Reading a string out of an encoded tape — proof internals

The completeness direction ends by reading the simulated machine's output off its encoded output tape. Once the output head has been driven back to cell 0 (see Complexitylib.Classes.P.Cobham.Internal.StepAlgebra), that tape's right half-block is the whole tape in order, two bits per cell: the first bit of a cell says whether it holds data, the second is the data bit.

So the output is recovered by two short recursions on notation, both collected here:

• Complexity.cellBits — every second bit of a string, from a fixed offset; used twice, once for the "is data" bits and once for the data bits;
• Complexity.runTrue — the leading run of trues, as a ruler; its length is where the first blank cell is, hence the output's length.

Main results

• Complexity.Cobham.cellBitsFn, Complexity.Cobham.runTrueFn — both are in the algebra
• Complexity.runTrue_length — the run's length is where the first false is, clamped by the ruler

Reading a single bit

def Complexity.bitOf (z : List Bool) (p : ℕ) : Bool

The bit of z at position p, false past the end.

Equations

• Complexity.bitOf z p = (List.drop p z).headD false

theorem Complexity.bitOf_eq_getElem {z : List Bool} {p : ℕ} (h : p < z.length) : bitOf z p = z[p]

Within range, bitOf is the indexed bit.

theorem Complexity.bitOf_of_le {z : List Bool} {p : ℕ} (h : z.length ≤ p) : bitOf z p = false

Past the end there is no bit.

theorem Complexity.bitOf_append_left {a : List Bool} {p : ℕ} (h : p < a.length) (b : List Bool) : bitOf (a ++ b) p = bitOf a p

Reading inside the first part of a concatenation.

theorem Complexity.bitOf_append_right {a : List Bool} {p : ℕ} (h : a.length ≤ p) (b : List Bool) : bitOf (a ++ b) p = bitOf b (p - a.length)

Reading past the first part of a concatenation.

theorem Complexity.bitAt_eq (r z : List Bool) : bitAt r z = [bitOf z r.length]

Cobham.bitAt reads exactly one bit, and it is bitOf.

Every second bit

cellBits o z m lists the bits of z at positions o, o + 2, …, o + 2(m-1). With z a run of two-bit symbol codes, offset o picks out one bit of each symbol — which is how both halves of a coded cell are read.

def Complexity.cellBits (o : ℕ) (z : List Bool) : ℕ → List Bool

The bits of z at positions 2i + o for i < m.

Equations

• Complexity.cellBits o z 0 = []
• Complexity.cellBits o z m.succ = Complexity.cellBits o z m ++ [Complexity.bitOf z (2 * m + o)]

@[simp]

theorem Complexity.cellBits_length (o : ℕ) (z : List Bool) (m : ℕ) : (cellBits o z m).length = m

theorem Complexity.cellBits_getElem? (o : ℕ) (z : List Bool) (m i : ℕ) : i < m → (cellBits o z m)[i]? = some (bitOf z (2 * i + o))

The leading run of trues

The output tape's "is data" bits are true on the output and false at the first blank past it, so the output's length is the length of the leading run of trues. The recursion below computes it as a ruler, clamped at the width it is run to: the guard m ≤ |previous| is what stops the run at the first false rather than restarting after it.

def Complexity.runTrue (z : List Bool) : ℕ → List Bool

The leading run of trues of z, clamped to m bits, as a ruler.

Equations

• Complexity.runTrue z 0 = []
• Complexity.runTrue z m.succ = Complexity.runTrue z m ++ if m ≤ (Complexity.runTrue z m).length ∧ Complexity.bitOf z m = true then [true] else []

theorem Complexity.runTrue_length_le (z : List Bool) (m : ℕ) : (runTrue z m).length ≤ m

theorem Complexity.runTrue_length {z : List Bool} {n : ℕ} (htrue : ∀ i < n, bitOf z i = true) (hfalse : bitOf z n = false) (m : ℕ) : (runTrue z m).length = min m n

The run's length is where the first false is. The guard in runTrue stops the run at the first false rather than restarting after it, so the run's length is the position of the first false, clamped by the width.

Both recursions are in the algebra

theorem Complexity.Cobham.cellBitsFn {n : ℕ} (o : ℕ) {gr gz : (Fin n → List Bool) → List Bool} (hr : Cobham gr) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => cellBits o (gz v) (gr v).length

Every second bit is in the algebra. One limited recursion on notation: each peeled bit of the ruler appends one more bit of z, read at twice the remaining ruler's length plus the offset.

theorem Complexity.Cobham.runTrueFn {n : ℕ} {gr gz : (Fin n → List Bool) → List Bool} (hr : Cobham gr) (hz : Cobham gz) : Cobham fun (v : Fin n → List Bool) => runTrue (gz v) (gr v).length

The leading run of trues is in the algebra. One limited recursion on notation: the run grows by one only while it has kept pace with the ruler, which is the length comparison nonemptyFn/notFn performs.