Polynomial-time evaluation of ordered FO(LFP)

For each fixed formula, the finite evaluator is computed by a native multi-tape Turing machine in polynomial time. The proof uses the library's certified closure rules for Boolean operations, bounded quantification, table construction and iteration. A fixed point's working table has exactly n ^ k bits after each step, so the loop calculus accounts for the size of intermediate states as well as the number of iterations.

The input vocabulary and formula are fixed. Polynomial degrees may depend on the formula's quantifier nesting and relation arities; no polynomial combined-complexity claim is made when the formula itself is part of the input.

Main results

• Cslib.Logic.FO.LFP.ModelChecker.computableInPolyTime_eval: the raw bounded evaluator has a native polynomial-time certificate, uniformly in polynomial-time input assignments.
• Cslib.Logic.FO.LFP.ModelChecker.computableInPolyTime_modelChecker: the sentence decider, including shape and universe-size checks, is polynomial time.
• Cslib.Logic.FO.Ordered.LFPDefinable.encodedLanguage_mem_P: every ordered FO(LFP)-definable query belongs to the existing native machine class P under encStructure.

References

• N. Immerman, Relational queries computable in polynomial time, Section 2.

theorem Cslib.Logic.FO.LFP.ModelChecker.computableInPolyTime_eval {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {Γ : List ℕ} {α : Type w} (φ : RawFormula (Ordered.language L) Γ α) {γ : Type} {enc : γ ↪ List Bool} {a : γ → EncodedStructure} {tables : γ → List (List Bool)} {σ : γ → α → ℕ} (ha : Turing.MultiTapeTM.ComputableInPolyTime a enc encStructure) (ht : Turing.MultiTapeTM.ComputableInPolyTime tables enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hσ : ∀ (x : α), Turing.MultiTapeTM.ComputableInPolyTime (fun (y : γ) => σ y x) enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (y : γ) => eval v φ (a y) (tables y) (σ y)) enc Turing.MultiTapeTM.encBool

Every fixed raw formula's bounded evaluator has a native polynomial-time implementation. The free variables may be any fixed family of polynomial-time numerical inputs. Formation is needed for semantic correctness, and is not needed for the cost bound.

def Cslib.Logic.FO.LFP.ModelChecker.modelChecker {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (φ : RawFormula (Ordered.language L) [] Empty) (a : EncodedStructure) : Bool

Decide a fixed sentence, rejecting malformed relation tables and universes smaller than two.

theorem Cslib.Logic.FO.LFP.ModelChecker.computableInPolyTime_modelChecker {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (φ : RawFormula (Ordered.language L) [] Empty) : Turing.MultiTapeTM.ComputableInPolyTime (modelChecker v φ) encStructure Turing.MultiTapeTM.encBool

The complete decision procedure, including its input checks, is native polynomial time.

theorem Cslib.Logic.FO.Ordered.LFPDefinable.encodedLanguage_mem_P {L : FirstOrder.Language} [L.IsRelational] {K : Query L} (hK : LFPDefinable K) (v : Vocabulary L) : K.encodedLanguage v ∈ Complexity.P encStructure

Every ordered FO(LFP)-definable query is in the native class P, using the existing source-only structure encoding. The formula is uniform over all canonical finite structures.