Shared output routines for first-order interpretation transducers

The order-free and canonical ordered transducers share coordinate extraction, framing, and malformed-output emission. Coordinates are written in increasing digit order; a client chooses its logical coordinate order through the formula's variable-to-register map.

Main definitions

• Cslib.Logic.Vocabulary.ModelChecker.Writer.tupleReg: a coordinate block register.
• Cslib.Logic.Vocabulary.ModelChecker.Writer.coordinatesCode: write the digits of an index.
• Cslib.Logic.Vocabulary.ModelChecker.Writer.rejectCode: emit a fixed malformed target.

Main results

• Cslib.Logic.Vocabulary.ModelChecker.Writer.reaches_coordinatesCode: exact digit semantics.
• Cslib.Logic.Vocabulary.ModelChecker.Writer.reachesOut_rejectCode: exact rejection output.

References

• N. Immerman, Descriptive Complexity. These routines are extracted from the existing order-free interpretation transducer, with its author and framing conventions retained.

def Cslib.Logic.Vocabulary.ModelChecker.Writer.tupleReg (d m i : ℕ) : ℕ

The register of the coordinate i of the tuple in block m, for tuples of d coordinates.

def Cslib.Logic.Vocabulary.ModelChecker.Writer.coordinatesCode (d m b : ℕ) : List Turing.CounterProgram.Instr

The code writing the coordinates of the tuple whose index is in register 4 into block m, placed at the label b; it continues at b + d.

theorem Cslib.Logic.Vocabulary.ModelChecker.Writer.length_coordinatesCode (d m b : ℕ) : (coordinatesCode d m b).length = d

The coordinate writer uses one instruction per digit.

theorem Cslib.Logic.Vocabulary.ModelChecker.Writer.reaches_coordinatesCode {P : Turing.CounterProgram} {w : List Bool} {B d m b n u : ℕ} (hP : P.CodeAt b (coordinatesCode d m b)) (hu : u < n ^ d) (hnB : n ≤ B) (regs : List ℕ) (h0 : regs.getD 0 0 = n) (h4 : regs.getD 4 0 = u) (hlen : tupleReg d m d ≤ regs.length) (hB : ∀ r ∈ regs, r ≤ B) : ∃ (regs' : List ℕ), P.Reaches w (P.Running B) (b, regs) (b + d, regs') ∧ regs'.length = regs.length ∧ (∀ i < d, regs'.getD (tupleReg d m i) 0 = u / n ^ i % n) ∧ (∀ (r : ℕ), (∀ i < d, r ≠ tupleReg d m i) → regs'.getD r 0 = regs.getD r 0) ∧ ∀ r ∈ regs', r ≤ B

Writing the coordinates of a tuple: from the code at b, with the index u < n ^ d of a tuple in register 4 and n in register 0, the program writes the coordinates u / n ^ i % n of the tuple into block m, changing no other register.

theorem Cslib.Logic.Vocabulary.ModelChecker.Writer.tupleReg_ne {d m m' i i' : ℕ} (h : m ≠ m') (hi : i < d) (hi' : i' < d) : tupleReg d m i ≠ tupleReg d m' i'

Distinct blocks have disjoint coordinate registers.

theorem Cslib.Logic.Vocabulary.ModelChecker.Writer.flatMap_range_pair_append_false (N : ℕ) (f : Fin N → Bool) : List.flatMap (fun (t : ℕ) => [true, if h : t < N then f ⟨t, h⟩ else false]) (List.range N) ++ [false] = Turing.MultiTapeTM.frame (List.ofFn f)

Emitting true and a bit for every number below N, then false, frames the bits.

def Cslib.Logic.Vocabulary.ModelChecker.Writer.rejectCode {L' : FirstOrder.Language} (v' : Vocabulary L') (b : ℕ) : List Turing.CounterProgram.Instr

The code emitting encStructure (0, [[], …, []]), a malformed input with one table too many, then halting; placed at b.

theorem Cslib.Logic.Vocabulary.ModelChecker.Writer.reachesOut_rejectCode {P : Turing.CounterProgram} {w : List Bool} {B : ℕ} {L' : FirstOrder.Language} {v' : Vocabulary L'} {b : ℕ} (hP : P.CodeAt b (rejectCode v' b)) (regs : List ℕ) (hB : ∀ r ∈ regs, r ≤ B) : P.ReachesOut w (P.Active B) (b, regs) (b + (v'.count + 2), regs) (List.replicate (v'.count + 2) false) ∧ P.instr (b + (v'.count + 2)) = Turing.CounterProgram.Instr.halt []

The rejection routine emits exactly the fixed malformed target and halts.

theorem Cslib.Logic.Vocabulary.ModelChecker.Writer.encStructure_reject {L' : FirstOrder.Language} {v' : Vocabulary L'} : encStructure (0, List.replicate (v'.count + 1) []) = List.replicate (v'.count + 2) false

The fixed malformed target has one empty table too many.