Synthesizing a positive native computation tableau #
Fixed finite transition tables become fixed finite disjunctions. The three input-symbol formulas are ordinary first-order formulas; every recursive relation occurrence is certified positive by the shared synthesis calculus. A single resulting formula works for every input structure and every finite domain size.
Main results #
traceStep_polarityDefinable: syntactic positivity and uniform definability of the native tableau transformer.trace_lfp_definable: a single FO(LFP) formula for the native tableau fixed point.
theorem Cslib.Complexity.ImmermanVardi.Tableau.traceStep_polarityDefinable {L : FirstOrder.Language} {ι : Type} {size : ι → ℕ} [(i : ι) → L.Structure (Fin (size i))] [∀ (i : ι), Fact (2 ≤ size i)] {m : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : ι → List Bool) (inputFormula : Option Bool → (Logic.FO.Ordered.language L).Formula (Fin 1)) (hinput :
∀ (i : ι) (s : Option Bool) (a : Fin (size i)), (inputFormula s).Realize ![a] ↔ Turing.inputAt (input i) ↑a = s) {α : Type} (args : Fin 3 → α) :
Logic.FO.Operator.PolarityDefinable Logic.FO.LFP.policy (fun {k : ℕ} => Logic.FO.LFP.headMark) true
(fun (j : (i : ι) × Set (Fin 3 → Fin (size i))) => Fin (size j.fst))
(fun (x : (i : ι) × Set (Fin 3 → Fin (size i))) => Logic.FO.LFP.interpretation)
(fun (j : (i : ι) × Set (Fin 3 → Fin (size i))) {k : ℕ} =>
Logic.FO.Operator.RelEnv.cons j.snd fun {k : ℕ} => Logic.FO.Operator.RelEnv.empty)
fun (j : (i : ι) × Set (Fin 3 → Fin (size i))) (v : α → Fin (size j.fst)) =>
v ∘ args ∈ (traceStep tm (input j.fst)) j.snd
The native tableau transformer has one syntactically positive defining body, uniform over all input structures and candidate ternary relations.
theorem Cslib.Complexity.ImmermanVardi.Tableau.trace_lfp_definable {L : FirstOrder.Language} {ι : Type} {size : ι → ℕ} [(i : ι) → L.Structure (Fin (size i))] [∀ (i : ι), Fact (2 ≤ size i)] {m : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : ι → List Bool) (inputFormula : Option Bool → (Logic.FO.Ordered.language L).Formula (Fin 1)) (hinput :
∀ (i : ι) (s : Option Bool) (a : Fin (size i)), (inputFormula s).Realize ![a] ↔ Turing.inputAt (input i) ↑a = s) {α : Type} (args : Fin 3 → α) :
Logic.FO.Operator.Definable Logic.FO.LFP.policy (fun (i : ι) => Fin (size i))
(fun (x : ι) => Logic.FO.LFP.interpretation) (fun (x : ι) {k : ℕ} => Logic.FO.Operator.RelEnv.empty)
fun (i : ι) (v : α → Fin (size i)) => v ∘ args ∈ OrderHom.lfp (traceStep tm (input i))
The native tableau least fixed point is uniformly FO(LFP)-definable.