FO(LFP) sentences for native machine acceptance #
One sentence expresses that a given deterministic native machine has halted with output
[true] by the maximum time in a finite ordered domain. The sentence is uniform in the
input structure and the domain size. Its input-symbol formulas are ordinary first-order
formulas, so no computational predicate is hidden in an added relation.
Main results #
exists_acceptance_sentence: native bounded machine acceptance has a single checked FO(LFP) sentence, given the first-order interpretation of its input tape.
theorem Cslib.Complexity.ImmermanVardi.Tableau.exists_acceptance_sentence {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) (hn : ∀ (i : ι), (input i).length + 1 < size i) (hB : ∀ (i : ι), Fintype.card (Tag m State) ≤ size i) :
∃ (φ : Logic.FO.LFP.Formula (Logic.FO.Ordered.language L) [] Empty),
∀ (i : ι),
(φ.Realize (fun {k : ℕ} => Logic.FO.Operator.RelEnv.empty) fun (e : Empty) => nomatch e) ↔ (Turing.MultiTapeTM.runFrom (tm.initCfg (input i)) (size i - 1)).Halted ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (input i)) (size i - 1)).output = [true]
A native deterministic machine's acceptance by the domain's final time is described by one checked FO(LFP) sentence. All input symbols are interpreted by ordinary first-order formulas.