Deterministic deciders of ordered queries

A deterministic decider of an ordered query on encStructure inputs validates the input tables, rejects cardinalities below two, runs a block of counter code with a true exit and a false exit, and accepts or rejects at the exit the block takes. blockDecider assembles such a program around any block. mem_L_of_decidingBlock reduces membership in L to the correctness of the block on well-formed inputs of cardinality at least two, with every register bounded by (N + 1) ^ (d + k) for input length N and maximal input arity d. The extra exponent k lets the block hold k-tuples of universe elements in single registers.

Ordered first-order model checking and FO(DTC) model checking are the two clients. The nondeterministic analogue, used by FO(TC) model checking, is nblockDecider in Classes.LogSpace.FirstOrder.Ordered.NondeterministicDecider.

Main definitions

• Cslib.Logic.FO.Ordered.blockDecider: the shape check, the size guard, the block, accept and reject.

Main results

• Cslib.Logic.FO.Ordered.decider_bounds: the register bound dominates the cardinality, its k-th power, the input length and the table sizes.
• Cslib.Logic.FO.Ordered.decider_layout: where the shape check, the guard, the block, accept and reject sit in a decider's code.
• Cslib.Logic.FO.Ordered.mem_L_of_decidingBlock: a correct block puts the query in L.

theorem Cslib.Logic.FO.Ordered.decider_bounds {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (k : ℕ) : 1 ≤ ((encStructure a).length + 1) ^ (v.maxArity + k) ∧ a.1 ≤ ((encStructure a).length + 1) ^ (v.maxArity + k) ∧ a.1 ^ k ≤ ((encStructure a).length + 1) ^ (v.maxArity + k) ∧ (encStructure a).length ≤ ((encStructure a).length + 1) ^ (v.maxArity + k) ∧ ∀ (i : ℕ), a.1 ^ Vocabulary.ModelChecker.arityAt v i ≤ ((encStructure a).length + 1) ^ (v.maxArity + k)

The register bound (N + 1) ^ (d + k) of a decider, for input length N and maximal input arity d, dominates 1, the cardinality n, n ^ k, N and the size of every input table.

def Cslib.Logic.FO.Ordered.blockDecider {L : FirstOrder.Language} (v : Vocabulary L) (C : ℕ → ℕ → ℕ → List Turing.CounterProgram.Instr) (c s : ℕ) : Turing.CounterProgram

The deterministic decider around a block C b T F of length c, placed at b with exits T (accept) and F (reject): the shape check, the guard rejecting cardinalities below two, the block, accept, reject. Registers 0 to 2 are the shape check's, followed by s scratch registers for the block.

theorem Cslib.Logic.FO.Ordered.decider_layout {L : FirstOrder.Language} {v : Vocabulary L} {P : Turing.CounterProgram} {pre blk : List Turing.CounterProgram.Instr} {g : Turing.CounterProgram.Instr} {c : ℕ} (hcode : P.code = pre ++ [g] ++ blk ++ [Turing.CounterProgram.Instr.accept, Turing.CounterProgram.Instr.reject]) (hpre : pre.length = 4 + 6 * v.count) (hblk : blk.length = c) : P.CodeAt 0 pre ∧ P.instr (4 + 6 * v.count) = g ∧ P.CodeAt (5 + 6 * v.count) blk ∧ P.instr (5 + 6 * v.count + c) = Turing.CounterProgram.Instr.accept ∧ P.instr (6 + 6 * v.count + c) = Turing.CounterProgram.Instr.reject

The layout of a decider whose code is a prefix of length 4 + 6 * v.count (the shape check), a guard instruction, a block of length c, accept and reject: the guard at 4 + 6 * v.count, the block at 5 + 6 * v.count, accept and reject right after it.

theorem Cslib.Logic.FO.Ordered.mem_L_of_decidingBlock {L : FirstOrder.Language} (v : Vocabulary L) {S : Set EncodedStructure} {C : ℕ → ℕ → ℕ → List Turing.CounterProgram.Instr} {c s k : ℕ} (hC : ∀ (b T F : ℕ), (C b T F).length = c) (hS : ∀ a ∈ S, v.WellFormed a ∧ 2 ≤ a.1) (hblock : ∀ (a : EncodedStructure), v.WellFormed a → 2 ≤ a.1 → ∀ (P : Turing.CounterProgram) (b T F : ℕ) (regs : List ℕ), P.CodeAt b (C b T F) → regs.length = 3 + s → regs.getD 0 0 = a.1 → (∀ r ∈ regs, r ≤ ((encStructure a).length + 1) ^ (v.maxArity + k)) → ∃ (res : Bool) (regs' : List ℕ), (res = true ↔ a ∈ S) ∧ P.Reaches (encStructure a) (P.Running (((encStructure a).length + 1) ^ (v.maxArity + k))) (b, regs) (if res = true then T else F, regs') ∧ ∀ r ∈ regs', r ≤ ((encStructure a).length + 1) ^ (v.maxArity + k)) : S ∈ Complexity.L encStructure

A deciding block puts an ordered query in L. Let S contain only well-formed inputs of cardinality at least two. Suppose that on every such input, the block C b T F, run from the cardinality in register 0 and s registers after the shape check's, exits to T exactly on members of S and otherwise to F, with every register at most (N + 1) ^ (d + k). Then blockDecider v C c s decides S in logarithmic space.