The counting machine's tape layout

⚠️ Unreviewed by Bolton

Placing the simulation with TM.placeWorkTM 0 m fixes where every tape sits: the simulated machine's k tapes come first, then its choice tape — which is the loop's counter — then the loop's own registers, and last the tape TM.retargetOutput sends the verdict to.

Six registers are needed: the two tallies, the horizon to compare the count against, a scratch cell for that comparison, a permanently blank tape to blank the verdict slot from, and the unary register that drives the wipe.

Main results

• NTM.bodyTapes — the tape count, and the named indices into it
• NTM.bodyIdx_distinct — the indices are pairwise distinct
• NTM.bodyRest — the resting contents of every tape the tally state does not name
• NTM.wipeTargets — the tapes the body blanks on its way out
• NTM.natTape_zero, NTM.regTape_zero — a register holding zero is the blank tape
• NTM.regTape_eq_natTape — a unary register of T ones is the binary numeral 2 ^ T - 1

@[reducible, inline]

abbrev Complexity.NTM.bodyTapes (k : ℕ) : ℕ

The counting machine's tape count: the simulation's k + 1, six registers, and the tape the verdict is written to.

Equations

• Complexity.NTM.bodyTapes k = 0 + (k + 1) + 6 + 1

def Complexity.NTM.cIdx (k : ℕ) : Fin (bodyTapes k)

The counter, which is also the simulation's choice tape.

Equations

• Complexity.NTM.cIdx k = ⟨k, ⋯⟩

def Complexity.NTM.aIdx (k : ℕ) : Fin (bodyTapes k)

The accepting tally.

Equations

• Complexity.NTM.aIdx k = ⟨k + 1, ⋯⟩

def Complexity.NTM.rIdx (k : ℕ) : Fin (bodyTapes k)

The rejecting tally.

Equations

• Complexity.NTM.rIdx k = ⟨k + 2, ⋯⟩

def Complexity.NTM.nIdx (k : ℕ) : Fin (bodyTapes k)

The horizon the counter is compared against.

Equations

• Complexity.NTM.nIdx k = ⟨k + 3, ⋯⟩

def Complexity.NTM.resIdx (k : ℕ) : Fin (bodyTapes k)

Scratch space for that comparison.

Equations

• Complexity.NTM.resIdx k = ⟨k + 4, ⋯⟩

def Complexity.NTM.zIdx (k : ℕ) : Fin (bodyTapes k)

A permanently blank tape, read whenever the verdict slot must be blanked.

Equations

• Complexity.NTM.zIdx k = ⟨k + 5, ⋯⟩

def Complexity.NTM.regIdx (k : ℕ) : Fin (bodyTapes k)

The unary register that drives the wipe.

Equations

• Complexity.NTM.regIdx k = ⟨k + 6, ⋯⟩

def Complexity.NTM.vIdx (k : ℕ) : Fin (bodyTapes k)

The tape the simulation's output is redirected to.

Equations

• Complexity.NTM.vIdx k = ⟨k + 7, ⋯⟩

theorem Complexity.NTM.vIdx_eq_last (k : ℕ) : vIdx k = Fin.last (0 + (k + 1) + 6)

def Complexity.NTM.simTapes (k : ℕ) : List (Fin (bodyTapes k))

The simulated machine's own work tapes: everything strictly left of the counter.

Equations

• Complexity.NTM.simTapes k = List.filter (fun (j : Fin (Complexity.NTM.bodyTapes k)) => decide (↑j < k)) (List.finRange (Complexity.NTM.bodyTapes k))

@[simp]

theorem Complexity.NTM.mem_simTapes_iff (k : ℕ) (j : Fin (bodyTapes k)) : j ∈ simTapes k ↔ ↑j < k

theorem Complexity.NTM.simTapes_nodup (k : ℕ) : (simTapes k).Nodup

theorem Complexity.NTM.simTapes_length_le (k : ℕ) : (simTapes k).length ≤ bodyTapes k

theorem Complexity.NTM.natTape_zero : natTape 0 = TM.blankTape

A counter tape holding zero is the blank tape, and so is a unary register holding zero. The machine's initial configuration therefore already carries both, which is what a prologue can start from.

theorem Complexity.NTM.regTape_zero : TM.regTape 0 = TM.blankTape

theorem Complexity.NTM.bits_two_pow_sub_one (T : ℕ) : (2 ^ T - 1).bits = List.replicate T true

A unary register of T ones is the binary numeral 2 ^ T - 1. The two encodings agree cell for cell: regCells writes 1 in cells 1 … T and blanks beyond, and so do the bits of 2 ^ T - 1. This is what lets the prologue produce the horizon 2 ^ T with a single increment, instead of a doubling loop.

theorem Complexity.NTM.regTape_eq_natTape (T : ℕ) : TM.regTape T = natTape (2 ^ T - 1)

theorem Complexity.NTM.cIdx_lt_aIdx (k : ℕ) : ↑(cIdx k) < ↑(aIdx k)

The registers are pairwise distinct, and none of them is one of the simulation's tapes.

theorem Complexity.NTM.bodyIdx_distinct (k : ℕ) : cIdx k ≠ aIdx k ∧ cIdx k ≠ rIdx k ∧ aIdx k ≠ rIdx k ∧ nIdx k ≠ cIdx k ∧ nIdx k ≠ aIdx k ∧ nIdx k ≠ rIdx k ∧ resIdx k ≠ cIdx k ∧ resIdx k ≠ aIdx k ∧ resIdx k ≠ rIdx k ∧ resIdx k ≠ nIdx k ∧ zIdx k ≠ cIdx k ∧ zIdx k ≠ aIdx k ∧ zIdx k ≠ rIdx k ∧ regIdx k ≠ cIdx k ∧ vIdx k ≠ cIdx k ∧ vIdx k ≠ aIdx k ∧ vIdx k ≠ rIdx k ∧ vIdx k ≠ zIdx k ∧ regIdx k ∉ simTapes k ∧ vIdx k ∉ simTapes k

def Complexity.NTM.bodyRest (k N H : ℕ) : Fin (bodyTapes k) → Tape

The resting contents of every tape the tally state does not name. The horizon sits on NTM.nIdx and the wipe's unary register on NTM.regIdx; everything else rests blank.

Equations

• Complexity.NTM.bodyRest k N H j = if j = Complexity.NTM.nIdx k then Complexity.natTape N else if j = Complexity.NTM.regIdx k then Complexity.TM.regTape H else Complexity.TM.blankTape

theorem Complexity.NTM.bodyRest_nIdx (k N H : ℕ) : bodyRest k N H (nIdx k) = natTape N

theorem Complexity.NTM.bodyRest_regIdx (k N H : ℕ) : bodyRest k N H (regIdx k) = TM.regTape H

theorem Complexity.NTM.bodyRest_other (k N H : ℕ) (j : Fin (bodyTapes k)) (hn : j ≠ nIdx k) (hr : j ≠ regIdx k) : bodyRest k N H j = TM.blankTape

theorem Complexity.NTM.bodyRest_parked (k N H : ℕ) (j : Fin (bodyTapes k)) : TM.Parked (bodyRest k N H j)

theorem Complexity.NTM.bodyRest_cells_zero (k N H : ℕ) (j : Fin (bodyTapes k)) : (bodyRest k N H j).cells 0 = Γ.start

theorem Complexity.NTM.bodyRest_head (k N H : ℕ) (j : Fin (bodyTapes k)) : (bodyRest k N H j).head = 1

theorem Complexity.NTM.bodyRest_startInvariant (k N H : ℕ) (j : Fin (bodyTapes k)) : (bodyRest k N H j).StartInvariant

theorem Complexity.NTM.bodyIdx_ne (k : ℕ) : ↑(cIdx k) = k ∧ ↑(aIdx k) = k + 1 ∧ ↑(rIdx k) = k + 2 ∧ ↑(nIdx k) = k + 3 ∧ ↑(resIdx k) = k + 4 ∧ ↑(zIdx k) = k + 5 ∧ ↑(regIdx k) = k + 6 ∧ ↑(vIdx k) = k + 7

The named registers are distinct from each other and from the simulation's tapes.

def Complexity.NTM.wipeTargets (k : ℕ) : List (Fin (bodyTapes k))

The tapes the body wipes on its way out: the simulated machine's own, and the tape its verdict was written to.

Equations

• Complexity.NTM.wipeTargets k = Complexity.NTM.simTapes k ++ [Complexity.NTM.vIdx k]

@[simp]

theorem Complexity.NTM.mem_wipeTargets_iff (k : ℕ) (j : Fin (bodyTapes k)) : j ∈ wipeTargets k ↔ ↑j < k ∨ j = vIdx k

theorem Complexity.NTM.wipeTargets_nodup (k : ℕ) : (wipeTargets k).Nodup

theorem Complexity.NTM.regIdx_not_mem_wipeTargets (k : ℕ) : regIdx k ∉ wipeTargets k