Nondeterministic deciders of ordered queries

A nondeterministic decider of an ordered query on encStructure inputs keeps its choice bit in register 0. Above the choice it validates the input tables and rejects cardinalities below two, then runs a nondeterministic block of counter code with a true exit, and accepts at that exit. nblockDecider assembles such a program around any block, as blockDecider does in the deterministic case. mem_NL_of_soundCompleteBlock reduces membership in NL to the correctness of the block on well-formed inputs of cardinality at least two. Every branch must reach the true exit only on members, or halt at the block's reject label. On members, some branch must reach the true exit. Every register stays at most (N + 1) ^ (d + k) for input length N and maximal input arity d.

FO(TC) model checking is the client.

Main definitions

• Cslib.Logic.FO.Ordered.nblockDecider: the shape check, the size guard, the block, accept and reject, above the choice bit.

Main results

• Cslib.Logic.FO.Ordered.mem_NL_of_soundCompleteBlock: a sound and complete block puts the query in NL.

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

The nondeterministic decider around a block C b T F of length c, placed at b with exits T (accept) and F (reject): the shape check and the guard rejecting cardinalities below two, shifted above the choice bit, then the block, accept, reject. Register 0 is the choice bit, registers 1 to 3 are the shape check's, followed by s scratch registers for the block.

theorem Cslib.Logic.FO.Ordered.mem_NL_of_soundCompleteBlock {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) (Post : Turing.CounterProgram.Config → Prop) (b T F : ℕ) (regs : List ℕ), P.CodeAt b (C b T F) → (P.instr F).halts = true → (∀ (x : Turing.CounterProgram.Config), x.1 = F → Post x) → regs.length = 3 + s → regs.getD 0 0 = a.1 → (∀ r ∈ regs, r ≤ ((encStructure a).length + 1) ^ (v.maxArity + k)) → (Turing.CounterProgram.Block.Sound P (encStructure a) (((encStructure a).length + 1) ^ (v.maxArity + k)) Post b regs T fun (regs' : List ℕ) => (∀ r ∈ regs', r ≤ ((encStructure a).length + 1) ^ (v.maxArity + k)) ∧ a ∈ S) ∧ (a ∈ S → Turing.CounterProgram.Block.Complete P (encStructure a) b regs T fun (x : List ℕ) => True)) : S ∈ Complexity.NL encStructure

A sound and complete block puts an ordered query in NL. 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 above the choice bit from the cardinality in register 0 and s registers after the shape check's, with every register at most (N + 1) ^ (d + k):

• is sound: every branch halts satisfying Post or reaches T only on members of S, keeping every register within the bound, whenever F is a halting label satisfying Post;
• is complete: on members of S, some branch reaches T.

Then nblockDecider v C c s decides S in nondeterministic logarithmic space.