Polynomial-time ordered queries run within one power of the universe size

The converse directions of the Immerman–Vardi and Grädel theorems simulate a native machine deciding an ordered query on the power universe Fin (n ^ k). This file supplies the machine and the tuple width k once: one finite-state machine decides the query by step n ^ k - 1 on every structure of size n, and n ^ k exceeds the encoding length and any fixed number of finite feature tags.

Main results

• Cslib.Logic.FO.Ordered.exists_tm_of_encodedLanguage_mem_P: a query whose encoded language is in P is decided by one machine within n ^ k - 1 steps, where n ^ k bounds the encoding length and a given number of tags.

theorem Cslib.Logic.FO.Ordered.exists_tm_of_encodedLanguage_mem_P {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {K : Query L} (hK : K.encodedLanguage v ∈ Complexity.P encStructure) : ∃ (m : ℕ) (State : Type) (x : Fintype State) (tm : Turing.MultiTapeTM m Bool State), ∀ (tags : ℕ), ∃ (k : ℕ), 1 ≤ k ∧ (∀ (i : Fin v.count), v.arity i ≤ k) ∧ (∀ (a : EncodedStructure), v.WellFormed a → 2 ≤ a.1 → (encStructure a).length + 1 < a.1 ^ k ∧ tags ≤ a.1 ^ k) ∧ ∀ (M : Structure L), M ∈ K ↔ (Turing.MultiTapeTM.runFrom (tm.initCfg (encStructure (encode v M))) (M.size ^ k - 1)).Halted ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (encStructure (encode v M))) (M.size ^ k - 1)).output = [true]

The machine of a polynomial-time ordered query. If the encoded language of K is in P, one finite-state machine tm decides K: for every number tags there is a tuple width k ≥ 1 bounding all arities of v such that n ^ k exceeds the encoding length plus one and is at least tags on every well-formed input of size n ≥ 2, and tm has halted with output [true] by step M.size ^ k - 1 exactly on the structures M ∈ K.