Total decoding, description size, and the Milestone C test battery

Turing.decodeCode interprets every bit string as a machine: malformed descriptions (and non-canonical ones — anything decodeCodeExact rejects) decode to the default reject machine Code.defaultRejectCode i, giving the paper's total notation [α]_i.

Turing.codeSize is the description length |α|; codeSize_le bounds it explicitly in the header data — the arithmetic later consumed by λ-boundedness bookkeeping.

The examples at the end are the Milestone C acceptance battery (planning/tm-infrastructure.md, WP9), all kernel-evaluated by decide: encode/decode round trips for the Milestone B machines, and one malformed description per failure mode — zero states, alphabet of size one, wrong table length, out-of-range successor state, out-of-range work symbol, trailing garbage, and the empty string — each pinned to decodeCodeExact = none and decodeCode = defaultRejectCode.

Total decoding

def Turing.decodeCode (i : ℕ) (s : List Bool) : Code i

Total decoding: the machine described by an arbitrary bit string — the paper's [α]_i. Strings rejected by decodeCodeExact denote the default reject machine.

Equations

• Turing.decodeCode i s = (Turing.decodeCodeExact i s).getD (Turing.Code.defaultRejectCode i)

@[simp]

theorem Turing.decodeCode_encodeCode {i : ℕ} (c : Code i) : decodeCode i (encodeCode c) = c

Description size

def Turing.codeSize {i : ℕ} (c : Code i) : ℕ

The description size |α| of a machine code.

Equations

• Turing.codeSize c = (Turing.encodeCode c).length

theorem Turing.codeSize_eq {i : ℕ} (c : Code i) : codeSize c = (encodeCode c).length

theorem Turing.encodeMove_length_le (m : Move) : (encodeMove m).length ≤ 2

theorem Turing.encodeOutput_length_le (o : Option Bool) : (encodeOutput o).length ≤ 2

theorem Turing.encodeListWith_length_le {α : Type u_1} {enc : α → List Bool} {B : ℕ} {l : List α} : (∀ a ∈ l, (enc a).length ≤ B) → (encodeListWith enc l).length ≤ l.length * B

Elementwise length bound for concatenated encodings.

theorem Turing.encodeAction_length_le {i : ℕ} (c : Code i) {a : RawAction} (ha : a ∈ c.raw.table) : (encodeAction a).length ≤ 2 * i + c.raw.workTapeCount * (4 + (encodeNat c.raw.alphabetSize).length) + 3 + (encodeNat c.raw.stateCount).length

Length bound for one well-formed table entry.

theorem Turing.codeSize_le {i : ℕ} (c : Code i) : codeSize c ≤ 1 + (encodeNat c.raw.workTapeCount).length + (encodeNat c.raw.alphabetSize).length + 2 * (encodeNat c.raw.stateCount).length + c.raw.stateCount * (c.raw.alphabetSize + 1) ^ (i + c.raw.workTapeCount) * (2 * i + c.raw.workTapeCount * (4 + (encodeNat c.raw.alphabetSize).length) + 3 + (encodeNat c.raw.stateCount).length)

Explicit size bound: header plus table-count times the per-entry bound. This is the |α| arithmetic that λ-boundedness bookkeeping consumes.

Round trips (Milestone B machines)

The malformed battery

One raw description per failure mode; each must be rejected by decodeCodeExact and decode totally to the default reject machine.

Display demos