Documentation

CslibFrontier.Computability.Complexity.Classes.LogSpace.FirstOrder.Ordered

Canonical ordered first-order model checking in logarithmic space #

For each fixed sentence over a finite relational input vocabulary expanded by canonical numeric symbols, its encoded query language belongs to L. Numeric 0, 1, max, order and BIT have the actual meanings on Fin n, for n ≥ 2, including inside quantified formulas. They are computed from cardinality and indices, with no extra numeric input tables.

The input uses encStructure: unary cardinality followed by the framed input relation tables in tupleIndex order. Malformed table shapes and cardinalities below two are rejected. The space bound is logarithmic in the full encoded input length; the sentence and vocabulary are fixed. This is a theorem at that encoding, with no assertion about raw words outside its image.

The decider is blockDecider (shape check, size guard, accept/reject) around the shared quantified control. Terms become native counter expressions; input relations read their actual table bits, order compares values, and BIT uses Christian Reitwiessner's binary digit algorithm, certified in linear work space in the binary value and index. The counter-program simulation charges intermediate expression storage.

This establishes ordered model checking. Ordered interpretations are computed in logarithmic space, and L and P are closed under ordered first-order reductions, in CslibFrontier.Computability.Complexity.Classes.LogSpace.FirstOrder.Ordered.Reduction; capture remains open.

Main definitions #

Main results #

References #

source
def Cslib.Logic.FO.Ordered.queryLanguage {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (φ : (language L).Sentence) :
Set EncodedStructure

Valid encodings of canonical ordered structures satisfying the fixed sentence. Cardinalities zero and one are excluded; the numeric vocabulary is computed rather than encoded.

Instances For
    source
    theorem Cslib.Logic.FO.Ordered.mem_queryLanguage {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {a : EncodedStructure} [Fact (2 ≤ a.1)] (φ : (language L).Sentence) :
    a ∈ queryLanguage v φ ↔ v.WellFormed a ∧ Fin a.1 ⊨ φ

    On an admissible cardinality, query membership is exactly shape validity and canonical ordered truth.

    source
    theorem Cslib.Logic.FO.Ordered.notMem_queryLanguage_of_lt_two {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {a : EncodedStructure} (hn : a.1 < 2) (φ : (language L).Sentence) :
    a ∉ queryLanguage v φ

    Universes smaller than the standard ordered convention are rejected.

    source
    def Cslib.Logic.FO.Ordered.ModelChecker.termExpr {L : FirstOrder.Language} [L.IsRelational] {α : Type u_1} (fv : α → ℕ) (base : ℕ) {k : ℕ} :
    (language L).Term (α ⊕ Fin k) → Turing.CounterProgram.Expr

    Compile a term to its natural index: variables use assignment registers, and the numeric constants are 0, 1, and the truncated predecessor of register 0 (the cardinality).

    Instances For
      source
      def Cslib.Logic.FO.Ordered.ModelChecker.atomicCompiler {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {α : Type u_1} (fv : α → ℕ) (base : ℕ) :
      Vocabulary.ModelChecker.AtomicCompiler (language L) α

      Actual native handlers for canonical ordered atoms. Input relations use their framed table; order and BIT use only the compiled numeric arguments.

      Instances For
        source
        theorem Cslib.Logic.FO.Ordered.ModelChecker.atomicCompiler_correct {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} (ha : v.WellFormed a) [Fact (2 ≤ a.1)] {α : Type u_1} (fv : α → ℕ) (base : ℕ) (val : α → Fin a.1) :
        (atomicCompiler v fv base).Correct (encStructure a) fv base val

        The ordered handlers compute their canonical semantics from the original encoded input.

        source
        def Cslib.Logic.FO.Ordered.ModelChecker.formulaCode {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {α : Type u_1} (fv : α → ℕ) (base : ℕ) {k : ℕ} (φ : (language L).BoundedFormula α k) (b T F : ℕ) :
        List Turing.CounterProgram.Instr

        Shared quantified control instantiated with the actual ordered handlers.

        Instances For
          source
          theorem Cslib.Logic.FO.Ordered.queryLanguage_mem_L {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (φ : (language L).Sentence) :
          queryLanguage v φ ∈ Complexity.L encStructure

          Every fixed canonical ordered first-order query is in L at the actual structure encoding. The decider is blockDecider around the compiled sentence: it rejects malformed table shapes and sizes zero/one; its numeric symbols are computed from the indices, including under quantifiers.