Register operations

The hand-rolled core machines of the reduction emitter's register calculus (docs/A5-ReductionEmitter.md): skipTM (a one-step no-op, the fold identity), incRegTM (append one mark to a register), and clearRegTM (blank a register). All register arithmetic (addition, multiplication, polynomial evaluation) composes from these via the forRegTM loop combinator.

Specs are in the ghost-parametrized EmitPred style: registers are the canonical tapes regTape v, and posts are Function.update equations.

def Complexity.TM.skipTM {n : ℕ} : TM n

One idle step and halt: the identity for seqTM folds.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.skipTM_hoareTime {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) : skipTM.HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ work₀ ys) 1

skipTM changes nothing (parked tapes).

inductive Complexity.TM.IncPhase : Type

State set shared by incRegTM and clearRegTM: scan sweeps right over the marks, back rewinds to the sentinel, park steps onto cell 1, and done halts.

• scan : IncPhase
• back : IncPhase
• park : IncPhase
• done : IncPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqIncPhase : DecidableEq IncPhase

Equations

• Complexity.TM.instDecidableEqIncPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeIncPhase : Fintype IncPhase

IncPhase is finite (it has exactly four states).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.incRegTM {n : ℕ} (q : Fin n) : TM n

Increment register q: scan right over the marks, write a mark on the first blank, rewind to cell 1. From regTape d to regTape (d + 1) in 2d + 4 steps; every other tape untouched.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.incRegTM_hoareTime {n : ℕ} (q : Fin n) (d : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ q → Parked (work₀ i)) (hq : work₀ q = regTape d) : (incRegTM q).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ q (regTape (d + 1))) ys) (2 * d + 4)

incRegTM Hoare specification. From regTape d in register q, reach regTape (d + 1) in 2d + 4 steps; the input, output, and every other work tape are untouched.

def Complexity.TM.clearRegCells (d k : ℕ) : ℕ → Γ

Cells of a register holding d mid-clear: positions 1..k blanked, k+1..d still marked.

Equations

• Complexity.TM.clearRegCells d k j = if j = 0 then Complexity.Γ.start else if j ≤ k then Complexity.Γ.blank else if j ≤ d then Complexity.Γ.one else Complexity.Γ.blank

theorem Complexity.TM.clearCells_zero (d : ℕ) : clearRegCells d 0 = regCells d

Before any blanking (k = 0), a mid-clear register is exactly regCells d.

theorem Complexity.TM.clearCells_last (d : ℕ) : clearRegCells d d = regCells 0

After blanking all d marks (k = d), a mid-clear register is regCells 0.

theorem Complexity.TM.clearCells_ne_start {d k j : ℕ} (hj : 1 ≤ j) : clearRegCells d k j ≠ Γ.start

No mid-clear cell at position j ≥ 1 is the ▷ sentinel.

theorem Complexity.TM.clearCells_update_succ (d k : ℕ) : Function.update (clearRegCells d k) (k + 1) Γ.blank = clearRegCells d (k + 1)

Blanking cell k + 1 of clearRegCells d k advances the sweep to clearRegCells d (k + 1).

def Complexity.TM.clearRegTM {n : ℕ} (q : Fin n) : TM n

Clear register q: sweep right blanking the marks, rewind to cell 1. From regTape d to regTape 0 in 2d + 4 steps; every other tape untouched.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.clearRegTM_hoareTime {n : ℕ} (q : Fin n) (d : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ q → Parked (work₀ i)) (hq : work₀ q = regTape d) : (clearRegTM q).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ q (regTape 0)) ys) (2 * d + 4)

clearRegTM Hoare specification. From regTape d in register q, reach regTape 0 in 2d + 4 steps; everything else untouched.