Running a machine inside the algebra — proof internals

Everything the completeness direction needs about a run, as opposed to a single step: a total step function that stands still once the machine has halted, the standing invariants of a run (the left-end marker where it belongs, every head inside the encoded window), and the iterated versions of Cobham.stepFn and Cobham.rewindFn.

Main results

• Complexity.TM.runCfg — the configuration after n steps, halting-idempotent
• Complexity.Cobham.iterate_stepFn — the encoded iteration tracks it
• Complexity.Cobham.iterate_rewindFn — the rewind iteration drives the head to cell 0

A total run

def Complexity.TM.runCfg {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) : ℕ → Cfg k tm.Q

The configuration after n steps, standing still once halted.

Equations

• tm.runCfg c 0 = c
• tm.runCfg c n.succ = (tm.step (tm.runCfg c n)).getD (tm.runCfg c n)

@[simp]

theorem Complexity.TM.runCfg_zero {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) : tm.runCfg c 0 = c

theorem Complexity.TM.runCfg_succ {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) (n : ℕ) : tm.runCfg c (n + 1) = (tm.step (tm.runCfg c n)).getD (tm.runCfg c n)

theorem Complexity.TM.runCfg_add {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) (a b : ℕ) : tm.runCfg c (a + b) = tm.runCfg (tm.runCfg c a) b

theorem Complexity.TM.runCfg_of_halted {k : ℕ} (tm : TM k) {c : Cfg k tm.Q} (h : c.state = tm.qhalt) (n : ℕ) : tm.runCfg c n = c

Once halted, the run stands still.

theorem Complexity.TM.runCfg_of_reachesIn {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} {t : ℕ} (h : tm.reachesIn t c c') : tm.runCfg c t = c'

A run of exactly t steps is the t-th iterate.

The standing invariants of a run

theorem Complexity.TM.step_startInvariant {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} (h : tm.step c = some c') (hin : c.input.StartInvariant) (hwork : ∀ (i : Fin k), (c.work i).StartInvariant) (hout : c.output.StartInvariant) : c'.input.StartInvariant ∧ (∀ (i : Fin k), (c'.work i).StartInvariant) ∧ c'.output.StartInvariant

One step preserves the left-end marker's position on every tape.

theorem Complexity.TM.step_head_le {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} (h : tm.step c = some c') : c'.input.head ≤ c.input.head + 1 ∧ (∀ (i : Fin k), (c'.work i).head ≤ (c.work i).head + 1) ∧ c'.output.head ≤ c.output.head + 1

One step moves every head by at most one cell.

theorem Complexity.TM.runCfg_startInvariant {k : ℕ} (tm : TM k) (x : List Bool) (n : ℕ) : (tm.runCfg (tm.initCfg x) n).input.StartInvariant ∧ (∀ (i : Fin k), ((tm.runCfg (tm.initCfg x) n).work i).StartInvariant) ∧ (tm.runCfg (tm.initCfg x) n).output.StartInvariant

Every tape of a run keeps its left-end marker.

theorem Complexity.TM.runCfg_head_le {k : ℕ} (tm : TM k) (x : List Bool) (n : ℕ) : (tm.runCfg (tm.initCfg x) n).input.head ≤ n ∧ (∀ (i : Fin k), ((tm.runCfg (tm.initCfg x) n).work i).head ≤ n) ∧ (tm.runCfg (tm.initCfg x) n).output.head ≤ n

After n steps every head is within n cells of the start.

theorem Complexity.Cobham.cfgTapes_runCfg_inv {k : ℕ} (tm : TM k) (x : List Bool) (n W : ℕ) (hn : n ≤ W) : (∀ t ∈ cfgTapes (tm.runCfg (tm.initCfg x) n), t.StartInvariant) ∧ ∀ t ∈ cfgTapes (tm.runCfg (tm.initCfg x) n), t.head ≤ W

The invariants of a run, in the form the encoding lemmas want.

theorem Complexity.Cobham.iterate_stepFn {k : ℕ} (tm : TM k) (W : ℕ) (x : List Bool) (hq : Fintype.card tm.Q ≤ blockWidth W) (n : ℕ) : n ≤ W → (stepFn tm (blockRuler W))^[n] (cfgCode W (tm.initCfg x)) = cfgCode W (tm.runCfg (tm.initCfg x) n)

The encoded iteration tracks the run.

The rewind iteration

theorem Complexity.Cobham.iterate_rewindFn {W : ℕ} (t : Tape) (hinv : t.StartInvariant) (hW : t.head ≤ W) (n : ℕ) : (rewindFn (blockRuler W))^[n] (pairCode W t) = pairCode W ((fun (s : Tape) => s.move Dir3.left)^[n] t)

The rewind iteration walks the head left.

theorem Complexity.Cobham.rewound (t : Tape) {n : ℕ} (h : t.head ≤ n) : (fun (s : Tape) => s.move Dir3.left)^[n] t = { head := 0, cells := t.cells }

After enough rewinding the head is at cell 0.

Reading the output off the rewound tape

With the head at cell 0 the tape's right half-block is the whole window, in order and two bits per cell. The first bit of each cell says whether it holds data — symCode is arranged so that only 0 and 1 have it set — and the second is the bit itself. So the output is the second bits, truncated where the first bits stop: Complexity.cellBits twice and one Complexity.runTrue.

@[simp]

theorem Complexity.Cobham.cellsCode_one (t : Tape) (i : ℕ) : cellsCode t i 1 = symCode (t.cells i)

theorem Complexity.Cobham.bitOf_cellsCode (t : Tape) {w j : ℕ} (hj : j < w) {o : ℕ} (ho : o < 2) : bitOf (cellsCode t 0 w) (2 * j + o) = bitOf (symCode (t.cells j)) o

Reading one bit of an aligned window is reading one bit of a cell's code.

theorem Complexity.Cobham.drop_pairCode_rewound (W : ℕ) (t : Tape) : List.drop (blockRuler W).length (pairCode W { head := 0, cells := t.cells }) = cellsCode t 0 (W + 1)

The aligned window of a rewound tape is its right half-block.

theorem Complexity.Cobham.output_of_cellsCode {W : ℕ} (t : Tape) (y : List Bool) (hy : t.HasOutput y) (hyW : y.length + 1 ≤ W) : List.take (runTrue (cellBits 2 (cellsCode t 0 (W + 1)) W) W).length (cellBits 3 (cellsCode t 0 (W + 1)) W) = y

Reading the output off an aligned window.

The whole simulation

Everything above, wired together: a clock long enough to run the machine to a halt and to rewind the output head, a first iteration that runs the machine, a second that rewinds, and the extraction.

theorem Complexity.Cobham.initFn_length {k : ℕ} (tm : TM k) (R x : List Bool) : (initFn tm R x).length = (2 * (k + 2) + 1) * R.length

The three stages, as functions of the clock

The clock string u fixes the encoded window: the ruler is 2|u| bits wide, so the window is W = |u| - 1 cells and u.tail is a ruler of exactly W bits.

def Complexity.Cobham.clockRuler (u : List Bool) : List Bool

The block ruler belonging to a clock value.

Equations

• Complexity.Cobham.clockRuler u = List.replicate (u ++ u).length false

theorem Complexity.Cobham.clockRuler_eq {u : List Bool} (h : 1 ≤ u.length) : clockRuler u = blockRuler (u.length - 1)

theorem Complexity.Cobham.clockRulerFn {n : ℕ} {gu : (Fin n → List Bool) → List Bool} (hu : Cobham gu) : Cobham fun (w : Fin n → List Bool) => clockRuler (gu w)

noncomputable def Complexity.Cobham.runFn {k : ℕ} (tm : TM k) (u x : List Bool) : List Bool

Stage one: the encoding after running the machine to a halt.

Equations

• Complexity.Cobham.runFn tm u x = (Complexity.Cobham.stepFn tm (Complexity.Cobham.clockRuler u))^[u.tail.length] (Complexity.Cobham.initFn tm (Complexity.Cobham.clockRuler u) x)

noncomputable def Complexity.Cobham.outPairFn {k : ℕ} (tm : TM k) (u x : List Bool) : List Bool

Stage two: the output tape's two half-blocks, head rewound to cell 0.

Equations

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

noncomputable def Complexity.Cobham.simFn {k : ℕ} (tm : TM k) (u x : List Bool) : List Bool

Stage three: the string on the rewound output tape.

Equations

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

theorem Complexity.Cobham.iterate_stepFn_length_le {k : ℕ} (tm : TM k) (R x : List Bool) (n : ℕ) : ((stepFn tm R)^[n] (initFn tm R x)).length ≤ (2 * (k + 2) + 1) * R.length

The simulated run never leaves its blocks.

theorem Complexity.Cobham.iterate_rewindFn_length_le (R z : List Bool) (hz : z.length ≤ 2 * R.length) (n : ℕ) : ((rewindFn R)^[n] z).length ≤ 2 * R.length

The rewind never leaves its two blocks.

theorem Complexity.Cobham.simFn_mem {k : ℕ} (tm : TM k) {gu : (Fin 1 → List Bool) → List Bool} (hu : Cobham gu) : Cobham fun (v : Fin 1 → List Bool) => simFn tm (gu v) (v 0)

The whole simulation is in the algebra.

theorem Complexity.Cobham.simFn_eq {k : ℕ} (tm : TM k) {T : ℕ → ℕ} {f : List Bool → List Bool} (hcomp : tm.ComputesInTime f T) (u x : List Bool) (hlen : T x.length + x.length + Fintype.card tm.Q + 2 ≤ u.length) : simFn tm u x = f x

The simulation computes the machine's function. Provided the clock outlasts the run, covers the input and is wide enough for the state code, the three stages reproduce exactly the string the machine leaves on its output tape.

theorem Complexity.Cobham.computes_mem_CobhamFP {k : ℕ} (tm : TM k) {T : ℕ → ℕ} {S D : ℕ} (hSD : ∀ (n : ℕ), T n ≤ S * (n + 1) ^ D) {f : List Bool → List Bool} (hcomp : tm.ComputesInTime f T) : CobhamFP f

The completeness direction, for one machine.