The circuit of a system of rules

A system of rules (DescriptiveComplexity.HornProgram) over an ordered structure is drawn as a monotone circuit whose gates evaluate its least fixed point: DescriptiveComplexity.CircNum.drawInterp.

• One disjunction gate per relation variable i and per tuple, canonically padded (DescriptiveComplexity.Padding): the atom i(x̄). Its inputs – all on the left wire, a disjunction of the circuit vocabulary being true as soon as some gate wired to its left is – are the rule instances deriving it: the rules whose head is that atom, at the valuations satisfying their guard. The guard is a formula of the input vocabulary, so it is evaluated by the wiring, not by the circuit.
• One conjunction chain per rule c and per valuation v̄ of its variables: the gate (c, j, v̄) is the conjunction of the j-th body atom, at v̄, and of the gate (c, j + 1, v̄); past the last body atom, the gate is the constant 1. So (c, 0, v̄) is “every body atom of c holds at v̄”.
• The outputs are the atoms of the relation variables bit τ, compared first by τ, then lexicographically.

Nothing is stratified by stages: the circuit may have cycles, and the evaluation of DescriptiveComplexity.GateVal, a least derivation, is the least fixed point of the rules as it stands.

This file holds the interpretation and reads its relations; the evaluation is DescriptiveComplexity.Problems.CircuitNumber.Hardness.

Tags

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.DrawTag {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : Type

The tags of the drawing: one per relation variable, for the atoms, and one per rule and position in its body, for the conjunction chains.

Equations

• DescriptiveComplexity.CircNum.DrawTag prog = (B.ι ⊕ (c : Fin (List.length prog)) × Fin ((DescriptiveComplexity.clauseAt prog c).body.length + 1))

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.atomTag {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {prog : HornProgram (L.sum FirstOrder.Language.order) B k} (i : B.ι) : DrawTag prog

The tag of the atoms of the relation variable i.

Equations

• DescriptiveComplexity.CircNum.atomTag i = Sum.inl i

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.stepTag {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {prog : HornProgram (L.sum FirstOrder.Language.order) B k} (c : Fin (List.length prog)) (j : Fin ((clauseAt prog c).body.length + 1)) : DrawTag prog

The tag of the j-th link of the conjunction chains of the rule c.

Equations

• DescriptiveComplexity.CircNum.stepTag c j = Sum.inr ⟨c, j⟩

The interpretation

noncomputable def DescriptiveComplexity.CircNum.drawInterp {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) {c : ℕ} (bit : Fin c → B.ι) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.numCircuit (DrawTag prog) (clauseDim B k)

The circuit of a system of rules, drawn inside an ordered structure, with the atoms of the relation variables bit τ as outputs.

Equations

• One or more equations did not get rendered due to their size.

Reading the relations