The encoded machine step, inside the algebra — proof internals

Complexitylib.Classes.P.Cobham.Internal.Encoding shows that one machine step acts on an encoded configuration blockwise, via tapeStepBlocks. This module shows the other half: that tapeStepBlocks is in Cobham's algebra once the written symbol and the direction are fixed constants — which they are inside one branch of Cobham.tableFn, since the branch is selected by the (state, read-symbols) key.

Each half-block of the successor is a short composition of toolkit members: Cobham.takeFn and Cobham.dropFn at width two, Cobham.appendFn, Cobham.const, and one Cobham.padFn to restore the block width.

Main results

• Complexity.Cobham.tapeStepBlocksFst, Complexity.Cobham.tapeStepBlocksSnd — both half-blocks of a stepped tape are in the algebra

theorem Complexity.Cobham.tapeStepBlocksFst {n : ℕ} (s : Γ) (d : Dir3) {gR gL gRt : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hL : Cobham gL) (_hRt : Cobham gRt) : Cobham fun (v : Fin n → List Bool) => (tapeStepBlocks (gR v) s d (gL v) (gRt v)).1

The left half-block after a step is in the algebra. For a fixed direction and written symbol it is one of: the old left block unchanged (stay), the symbol prepended (right), or two bits dropped (left).

theorem Complexity.Cobham.tapeStepBlocksSnd {n : ℕ} (s : Γ) (d : Dir3) {gR gL gRt : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hL : Cobham gL) (hRt : Cobham gRt) : Cobham fun (v : Fin n → List Bool) => (tapeStepBlocks (gR v) s d (gL v) (gRt v)).2

The right half-block after a step is in the algebra. For a fixed direction and written symbol it is the old right block with its leading symbol replaced (stay), consumed (right), or pushed back together with the nearest left symbol (left).

theorem Complexity.Cobham.blockAt_cfgCode_tape {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (j : ℕ) (hj : j < (cfgTapes c).length) : blockAt (blockRuler W) (cfgCode W c) (2 * j + 1) = padTo (blockRuler W) (leftCode (cfgTapes c)[j]) ∧ blockAt (blockRuler W) (cfgCode W c) (2 * j + 2) = padTo (blockRuler W) (rightCode (cfgTapes c)[j] W)

Tape j's two half-blocks, read out of an encoded configuration. Block 0 is the state, so tape j occupies blocks 2j+1 and 2j+2 — exactly the indices tapesStepFn addresses with Cobham.blockFn.

The transition key

The key is the state together with the symbol under every head. Reading it out of an encoding is one takeFn per field: the state block truncated to |Q| bits, then the first two bits of each tape's right half-block.

def Complexity.Cobham.readsFn (R : List Bool) (m j : ℕ) (z : List Bool) : List Bool

The read symbols of the tapes from index j on, m of them.

Equations

• Complexity.Cobham.readsFn R 0 j z = []
• Complexity.Cobham.readsFn R m_2.succ j z = List.take 2 (Complexity.blockAt R z (2 * j + 2)) ++ Complexity.Cobham.readsFn R m_2 (j + 1) z

def Complexity.Cobham.keyFn (R : List Bool) (q m : ℕ) (z : List Bool) : List Bool

The transition key, read out of an encoded configuration.

Equations

• Complexity.Cobham.keyFn R q m z = List.take q (Complexity.blockAt R z 0) ++ Complexity.Cobham.readsFn R m 0 z

theorem Complexity.Cobham.readsFn_mem {n : ℕ} (m j : ℕ) {gR gz : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => readsFn (gR v) m j (gz v)

Reading the head symbols is in the algebra.

theorem Complexity.Cobham.keyFn_mem {n : ℕ} (q m : ℕ) {gR gz : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => keyFn (gR v) q m (gz v)

Reading the transition key is in the algebra.

theorem Complexity.Cobham.readsFn_eq {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (hW : ∀ t ∈ cfgTapes c, t.head ≤ W) (m j : ℕ) : j + m = (cfgTapes c).length → readsFn (blockRuler W) m j (cfgCode W c) = List.flatMap (fun (t : Tape) => symCode t.read) (List.drop j (cfgTapes c))

The extracted key is the transition key.

theorem Complexity.Cobham.keyFn_eq {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (hq : Fintype.card Q ≤ blockWidth W) (hW : ∀ t ∈ cfgTapes c, t.head ≤ W) : keyFn (blockRuler W) (Fintype.card Q) (k + 2) (cfgCode W c) = keyCode c

The whole key, read out of an encoded configuration.

Lifting across all the tapes

A machine has a fixed number of tapes, so stepping all of them is a finite composition — the recursion below is at the meta level, over the list of per-tape actions, not inside the algebra. Tape j occupies blocks 2j+1 and 2j+2 (block 0 is the state), which Cobham.blockFn addresses.

def Complexity.Cobham.tapesStepFn (R : List Bool) (acts : List (Γ × Dir3)) (j : ℕ) (z : List Bool) : List Bool

The successor's tape blocks for one transition-table branch, as a function of the predecessor's encoding: tape j's two half-blocks, stepped, concatenated.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Cobham.tapesStepFn R [] j z = []

theorem Complexity.Cobham.tapesStepFn_mem {n : ℕ} (acts : List (Γ × Dir3)) (j : ℕ) {gR gz : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => tapesStepFn (gR v) acts j (gz v)

Stepping every tape is in the algebra.

theorem Complexity.Cobham.tapesStepFn_eq {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (acts : List (Γ × Dir3)) (j : ℕ) : j + acts.length ≤ (cfgTapes c).length → tapesStepFn (blockRuler W) acts j (cfgCode W c) = (List.zipWith (fun (a : Γ × Dir3) (t : Tape) => [(tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).1, (tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).2]) acts (List.drop j (cfgTapes c))).flatten.flatten

The algebra-side tape step computes the machine-side one. Reading the half-blocks out of the encoding (blockAt) gives exactly the tapes' own half-blocks, so tapesStepFn reproduces the blockwise map of tapesBlocks_tapesStep.

def Complexity.Cobham.branchFn (R q' : List Bool) (acts : List (Γ × Dir3)) (z : List Bool) : List Bool

One whole branch of the transition table: the new state block (a constant) followed by every tape stepped.

Equations

• Complexity.Cobham.branchFn R q' acts z = Complexity.padTo R q' ++ Complexity.Cobham.tapesStepFn R acts 0 z

theorem Complexity.Cobham.branchFn_mem {n : ℕ} (q' : List Bool) (acts : List (Γ × Dir3)) {gR gz : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => branchFn (gR v) q' acts (gz v)

A transition-table branch is in the algebra. With the branch fixed, the new state code and every tape's write and direction are constants, so the whole successor configuration is a finite composition of toolkit members.

theorem Complexity.Cobham.branchFn_eq {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} {W : ℕ} (h : tm.step c = some c') (hout : c.output.StartInvariant) (hwork : ∀ (i : Fin k), (c.work i).StartInvariant) (hgood : List.Forall₂ (fun (a : Γ × Dir3) (t : Tape) => (t.head = 0 → a.1 = t.cells t.head) ∧ (a.2 ≠ Dir3.right → t.head ≠ 0) ∧ t.head ≤ W) (stepActs tm c) (cfgTapes c)) : branchFn (blockRuler W) (stateCode c'.state) (stepActs tm c) (cfgCode W c) = cfgCode W c'

The join. For a fixed transition-table branch, the algebra-side successor branchFn — built purely from takeFn/dropFn/appendFn/padFn/const — is the encoding of the machine's successor configuration.

This is the point where the two halves of the development meet: the machine side (cfgBlocks_step, from the six write-and-move lemmas) and the algebra side (tapesStepFn, in the class by branchFn_mem).

The whole transition table

A machine has finitely many (state, read-symbols) keys, so the transition function is a finite table: one branchFn per key, selected by matching the key read out of the encoding against the key's constant pattern.

noncomputable def Complexity.Cobham.stepEntries {k : ℕ} (tm : TM k) : List (tm.Q × (Fin (k + 2) → Γ))

The transition table's index set: every (state, read-symbols) pair.

Equations

• Complexity.Cobham.stepEntries tm = Finset.univ.toList

theorem Complexity.Cobham.mem_stepEntries {k : ℕ} (tm : TM k) (p : tm.Q × (Fin (k + 2) → Γ)) : p ∈ stepEntries tm

Every key is in the table.

noncomputable def Complexity.Cobham.stepBranch {k : ℕ} (tm : TM k) (R : List Bool) (p : tm.Q × (Fin (k + 2) → Γ)) (z : List Bool) : List Bool

The branch a transition key selects. A halting key stands still: the machine has stopped, but the simulation runs for a fixed polynomial number of steps, so the encoding has to be a fixed point from then on.

Equations

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

theorem Complexity.Cobham.stepBranch_halt {k : ℕ} (tm : TM k) (R : List Bool) {p : tm.Q × (Fin (k + 2) → Γ)} (h : p.1 = tm.qhalt) (z : List Bool) : stepBranch tm R p z = z

theorem Complexity.Cobham.stepBranch_step {k : ℕ} (tm : TM k) (R : List Bool) {p : tm.Q × (Fin (k + 2) → Γ)} (h : p.1 ≠ tm.qhalt) (z : List Bool) : stepBranch tm R p z = branchFn R (stateCode (stepStateOf tm p.1 p.2)) (stepActsOf tm p.1 p.2) z

noncomputable def Complexity.Cobham.stepFn {k : ℕ} (tm : TM k) (R z : List Bool) : List Bool

One machine step, on encodings. The table dispatches on the key read out of the encoding and applies that key's branch.

Equations

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

theorem Complexity.Cobham.stepFn_mem {n k : ℕ} (tm : TM k) {gR gz : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => stepFn tm (gR v) (gz v)

The encoded step is in the algebra.

theorem Complexity.Cobham.stepFn_apply {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) {W : ℕ} (hq : Fintype.card tm.Q ≤ blockWidth W) (hW : ∀ t ∈ cfgTapes c, t.head ≤ W) : stepFn tm (blockRuler W) (cfgCode W c) = stepBranch tm (blockRuler W) (c.state, cfgReads c) (cfgCode W c)

The table selects the configuration's own branch. The key read out of the encoding is the configuration's key, and by keyPattern_injective no other entry's pattern matches it.

theorem Complexity.Cobham.stepFn_eq {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} {W : ℕ} (h : tm.step c = some c') (hq : Fintype.card tm.Q ≤ blockWidth W) (hW : ∀ t ∈ cfgTapes c, t.head ≤ W) (hout : c.output.StartInvariant) (hwork : ∀ (i : Fin k), (c.work i).StartInvariant) (hgood : List.Forall₂ (fun (a : Γ × Dir3) (t : Tape) => (t.head = 0 → a.1 = t.cells t.head) ∧ (a.2 ≠ Dir3.right → t.head ≠ 0) ∧ t.head ≤ W) (stepActs tm c) (cfgTapes c)) : stepFn tm (blockRuler W) (cfgCode W c) = cfgCode W c'

The encoded step computes the machine step.

theorem Complexity.Cobham.stepFn_halted {k : ℕ} (tm : TM k) {c : Cfg k tm.Q} {W : ℕ} (h : c.state = tm.qhalt) (hq : Fintype.card tm.Q ≤ blockWidth W) (hW : ∀ t ∈ cfgTapes c, t.head ≤ W) : stepFn tm (blockRuler W) (cfgCode W c) = cfgCode W c

A halted encoding is a fixed point.

Length bounds

Cobham.iterFn needs one polynomial bound covering every iterate, including the ones reached from junk inputs. Both simulated steps keep an encoding inside a fixed number of blocks, which is all the bound needs.

theorem Complexity.Cobham.tapesStepFn_length_le (R : List Bool) (acts : List (Γ × Dir3)) (j : ℕ) (z : List Bool) : (tapesStepFn R acts j z).length ≤ 2 * acts.length * R.length

theorem Complexity.Cobham.branchFn_length_le (R q' : List Bool) (acts : List (Γ × Dir3)) (z : List Bool) : (branchFn R q' acts z).length ≤ (2 * acts.length + 1) * R.length

@[simp]

theorem Complexity.Cobham.stepActsOf_length {k : ℕ} (tm : TM k) (q : tm.Q) (syms : Fin (k + 2) → Γ) : (stepActsOf tm q syms).length = k + 2

theorem Complexity.Cobham.stepFn_length_le {k : ℕ} (tm : TM k) (R z : List Bool) (hz : z.length ≤ (2 * (k + 2) + 1) * R.length) : (stepFn tm R z).length ≤ (2 * (k + 2) + 1) * R.length

An encoded configuration stays within its blocks.

Rewinding the output head

The encoding splits a tape at its head, so reading a tape off an encoding is easy only when the head sits at cell 0 — then the left half is empty and the right half is the whole tape, in order. Driving the head back to cell 0 is a separate iteration, of a step that moves one cell left and writes nothing.

It is stated on one tape's pair of half-blocks rather than on a whole configuration: after the simulation only the output tape matters, and a pair of blocks splits with one takeFn/dropFn.

def Complexity.Cobham.pairCode (W : ℕ) (t : Tape) : List Bool

One tape as its two padded half-blocks, concatenated.

Equations

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

theorem Complexity.Cobham.take_pairCode (W : ℕ) (t : Tape) : List.take (blockRuler W).length (pairCode W t) = padTo (blockRuler W) (leftCode t)

theorem Complexity.Cobham.drop_pairCode (W : ℕ) (t : Tape) : List.drop (blockRuler W).length (pairCode W t) = padTo (blockRuler W) (rightCode t W)

def Complexity.Cobham.rewindStep (R : List Bool) (s : Γ) (z : List Bool) : List Bool

One left move on a pair of half-blocks, writing back the symbol s.

Equations

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

def Complexity.Cobham.rewindFn (R z : List Bool) : List Bool

One rewind step. The head moves one cell left, except at cell 0 — where it reads ▷ and stays put, which is also what the machine model does. The symbol written back is the one just read, so nothing changes but the head.

Equations

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

theorem Complexity.Cobham.rewindFn_mem {n : ℕ} {gR gz : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => rewindFn (gR v) (gz v)

The rewind step is in the algebra.

theorem Complexity.Cobham.take_two_drop_pairCode {W : ℕ} (t : Tape) (hW : t.head ≤ W) : List.take 2 (List.drop (blockRuler W).length (pairCode W t)) = symCode t.read

The first two bits of a tape's padded right half-block code its read symbol.

theorem Complexity.Cobham.rewindFn_eq {W : ℕ} (t : Tape) (hinv : t.StartInvariant) (hW : t.head ≤ W) : rewindFn (blockRuler W) (pairCode W t) = pairCode W (t.move Dir3.left)

The rewind step computes a left move. Away from cell 0 the symbol written back is the one read, so tapeStepBlocks_eq applies with Tape.write_read_self; at cell 0 the head reads ▷ and both sides stand still.

theorem Complexity.Cobham.rewindFn_length_le (R z : List Bool) (hz : z.length ≤ 2 * R.length) : (rewindFn R z).length ≤ 2 * R.length

A rewound pair stays within its two blocks.

The initial encoding

At the start every tape but the input is blank and every head is at cell 0, so the encoding is a constant apart from the input tape's right half-block — which is the input string at two bits per cell. Zero padding is blank padding, which is why symCode Γ.blank = [0,0].

def Complexity.Cobham.encodeBits (x : List Bool) : List Bool

A bitstring as tape cells, two bits each.

Equations

• Complexity.Cobham.encodeBits x = List.flatMap (fun (b : Bool) => Complexity.Cobham.symCode (Complexity.Γ.ofBool b)) x

@[simp]

theorem Complexity.Cobham.encodeBits_nil : encodeBits [] = []

@[simp]

theorem Complexity.Cobham.encodeBits_cons (b : Bool) (x : List Bool) : encodeBits (b :: x) = symCode (Γ.ofBool b) ++ encodeBits x

@[simp]

theorem Complexity.Cobham.encodeBits_length (x : List Bool) : (encodeBits x).length = 2 * x.length

theorem Complexity.Cobham.encodeBitsFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) : Cobham fun (v : Fin n → List Bool) => encodeBits (g v)

Coding a string as tape cells is in the algebra.

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

The initial encoding. Everything but the input tape's right half-block is a constant of the machine.

Equations

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

theorem Complexity.Cobham.initFn_mem {n k : ℕ} (tm : TM k) {gR gx : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hx : Cobham gx) : Cobham fun (v : Fin n → List Bool) => initFn tm (gR v) (gx v)

The initial encoding is in the algebra.

The initial tapes

theorem Complexity.Cobham.cellsCode_add (t : Tape) (i a b : ℕ) : cellsCode t i (a + b) = cellsCode t i a ++ cellsCode t (i + a) b

Windows concatenate.

theorem Complexity.Cobham.initFn_eq {k : ℕ} (tm : TM k) (W : ℕ) (x : List Bool) (hx : x.length ≤ W) : initFn tm (blockRuler W) x = cfgCode W (tm.initCfg x)

The initial encoding is the initial configuration's.