Register-machine kernel of the closure loops

The counter code compiled from transitive-closure (FO(TC)) and deterministic-transitive-closure (FO(DTC)) formulas over the canonical ordered language shares one kernel. It evaluates a term whose free variables sit in registers, tests whether the current tuple of a closure loop differs from the target tuple, decodes a base-n code into a tuple of registers, and loads the source tuple of a closure.

Main definitions

• Cslib.Logic.FO.Ordered.ClosureKernel.termE: a term as an expression.
• Cslib.Logic.FO.Ordered.ClosureKernel.testExpr: positive exactly when the current tuple differs from the target tuple.
• Cslib.Logic.FO.Ordered.ClosureKernel.digitE: digit i of a base-n code.

Main results

• Cslib.Logic.FO.Ordered.ClosureKernel.reaches_digitsCode: decoding a code into a tuple.
• Cslib.Logic.FO.Ordered.ClosureKernel.reaches_loadCode: loading the source tuple of a closure.
• Cslib.Logic.FO.Ordered.ClosureKernel.eval_termE_of_atomic: a compiled term computes its value.

References

• N. Immerman, Languages That Capture Complexity Classes, Theorems 3.1 and 4.2

def Cslib.Logic.FO.Ordered.ClosureKernel.termE {L : FirstOrder.Language} [L.IsRelational] {α : Type u_1} (fv : α → ℕ) (t : (language L).Term α) : Turing.CounterProgram.Expr

A term with free variables in registers, as an expression.

theorem Cslib.Logic.FO.Ordered.ClosureKernel.eval_termE_of_atomic {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {w : List Bool} {α : Type} {fv : α → ℕ} {val : α → Fin a.1} (hC : (ModelChecker.atomicCompiler v fv 0).Correct w fv 0 val) {regs : List ℕ} (h0 : regs.getD 0 0 = a.1) (hv : ∀ (x : α), regs.getD (fv x) 0 = ↑(val x)) (t : (language L).Term α) : Turing.CounterProgram.Expr.eval regs (termE fv t) = ↑(FirstOrder.Language.Term.realize val t)

A term compiled by termE computes its value, given correct atomic handlers.

def Cslib.Logic.FO.Ordered.ClosureKernel.testExpr (base k : ℕ) (z : Fin k → Turing.CounterProgram.Expr) : Turing.CounterProgram.Expr

The test of the closure loop: positive exactly when the current tuple differs from the target tuple.

theorem Cslib.Logic.FO.Ordered.ClosureKernel.lt_eval_testExpr {base k n : ℕ} {z : Fin k → Turing.CounterProgram.Expr} {regs : List ℕ} {us zs : Fin k → Fin n} (hu : ∀ (i : Fin k), regs.getD (base + ↑i) 0 = ↑(us i)) (hz : ∀ (i : Fin k), Turing.CounterProgram.Expr.eval regs (z i) = ↑(zs i)) : Turing.CounterProgram.Expr.eval regs (Turing.CounterProgram.Expr.const 0) < Turing.CounterProgram.Expr.eval regs (testExpr base k z) ↔ us ≠ zs

theorem Cslib.Logic.FO.Ordered.ClosureKernel.eval_pow_reg0 {regs : List ℕ} {n k : ℕ} (h0 : regs.getD 0 0 = n) : Turing.CounterProgram.Expr.eval regs ((Turing.CounterProgram.Expr.reg 0).pow k) = n ^ k

With n in register 0, the expression n ^ k evaluates to n ^ k.

def Cslib.Logic.FO.Ordered.ClosureKernel.digitE (r i : ℕ) : Turing.CounterProgram.Expr

Digit i in base n (register 0) of register r: the decoding of a code into a tuple.

theorem Cslib.Logic.FO.Ordered.ClosureKernel.eval_digitE {regs : List ℕ} {r k n : ℕ} (h0 : regs.getD 0 0 = n) (g : Fin (n ^ k)) (hg : regs.getD r 0 = ↑g) (i : Fin k) : Turing.CounterProgram.Expr.eval regs (digitE r ↑i) = ↑(finFunctionFinEquiv.symm g i)

With n in register 0 and a code g < n ^ k in register r, digitE r i is digit i of the tuple finFunctionFinEquiv.symm g.

theorem Cslib.Logic.FO.Ordered.ClosureKernel.reaches_digitsCode {P : Turing.CounterProgram} {w : List Bool} {B b r d k n : ℕ} (hP : P.CodeAt b (Turing.CounterProgram.assignsCode b d k (digitE r))) (hrd : r < d ∨ d + k ≤ r) (hd : 0 < d) {regs : List ℕ} (hlen : d + k ≤ regs.length) (h0 : regs.getD 0 0 = n) (hnB : n ≤ B) (hB : ∀ x ∈ regs, x ≤ B) (g : Fin (n ^ k)) (hg : regs.getD r 0 = ↑g) : ∃ (regs' : List ℕ), P.Reaches w (P.Running B) (b, regs) (b + k, regs') ∧ regs'.length = regs.length ∧ (∀ (j : ℕ), j < d ∨ d + k ≤ j → regs'.getD j 0 = regs.getD j 0) ∧ (∀ (i : Fin k), regs'.getD (d + ↑i) 0 = ↑(finFunctionFinEquiv.symm g i)) ∧ ∀ x ∈ regs', x ≤ B

Decoding register r, holding g < n ^ k, into registers d + i writes the tuple finFunctionFinEquiv.symm g.

theorem Cslib.Logic.FO.Ordered.ClosureKernel.reaches_loadCode {P : Turing.CounterProgram} {w : List Bool} {B b base k n : ℕ} {src : Fin k → Turing.CounterProgram.Expr} (hP : P.CodeAt b (Turing.CounterProgram.assignsCode b base k fun (i : ℕ) => if h : i < k then src ⟨i, h⟩ else Turing.CounterProgram.Expr.const 0)) {regs₀ : List ℕ} (hlen : base + k ≤ regs₀.length) (hnB : n ≤ B) (hB : ∀ x ∈ regs₀, x ≤ B) {s₀ : Fin k → Fin n} (hsrc : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (i : Fin k), Turing.CounterProgram.Expr.eval regs (src i) = ↑(s₀ i)) : ∃ (regs' : List ℕ), P.Reaches w (P.Running B) (b, regs₀) (b + k, regs') ∧ regs'.length = regs₀.length ∧ (∀ (j : ℕ), j < base ∨ base + k ≤ j → regs'.getD j 0 = regs₀.getD j 0) ∧ (∀ (i : Fin k), regs'.getD (base + ↑i) 0 = ↑(s₀ i)) ∧ ∀ x ∈ regs', x ≤ B

Loading the source tuple s₀ of a closure, denoted by expressions src that read only registers below base, into registers base + i.

theorem Cslib.Logic.FO.Ordered.ClosureKernel.getD_pair {regs : List ℕ} {base k n : ℕ} {us vs : Fin k → Fin n} (hu : ∀ (i : Fin k), regs.getD (base + ↑i) 0 = ↑(us i)) (hv : ∀ (i : Fin k), regs.getD (base + k + ↑i) 0 = ↑(vs i)) (i : Fin (2 * k)) : regs.getD (base + ↑i) 0 = ↑(TC.pair us vs i)

The pair of a tuple in registers base + i and a tuple in registers base + k + i is in registers base + i, for i < 2 * k.

theorem Cslib.Logic.FO.Ordered.ClosureKernel.getD_elim_eq {α : Type} {fv : α → ℕ} {base : ℕ} {regs : List ℕ} {n : ℕ} {val : α → Fin n} (hv : ∀ (x : α), regs.getD (fv x) 0 = ↑(val x)) {c : Fin n} (hc : regs.getD base 0 = ↑c) (y : Option α) : regs.getD (y.elim base fv) 0 = ↑(y.elim c val)

The registers of the extended assignment of an existential body: the new variable in register base, the others in their registers.