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.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.

def Turing.dummyEntry : RawAction

A syntactically plausible one-input entry.

Equations

• Turing.dummyEntry = { inputMoves := #[Turing.Move.stay], workActions := #[], output := some false, nextState := none }

def Turing.badZeroStates : RawCode 1

Zero states (the empty table has the canonical size 0 · 3¹, so this parses and is rejected by the checker alone).

Equations

• Turing.badZeroStates = { workTapeCount := 0, alphabetSize := 2, stateCount := 0, startState := 0, table := #[] }

def Turing.badAlphabet : RawCode 1

Alphabet of size one (table of the canonical size 1 · 2¹).

Equations

• Turing.badAlphabet = { workTapeCount := 0, alphabetSize := 1, stateCount := 1, startState := 0, table := #[Turing.dummyEntry, Turing.dummyEntry] }

def Turing.badTableLength : RawCode 1

Wrong table length: the header demands 1 · 3¹ = 3 entries, only two are present, so parsing itself fails.

Equations

• Turing.badTableLength = { workTapeCount := 0, alphabetSize := 2, stateCount := 1, startState := 0, table := #[Turing.dummyEntry, Turing.dummyEntry] }

def Turing.badNextState : RawCode 1

Out-of-range successor state.

Equations

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

def Turing.badWorkSymbol : RawCode 1

Out-of-range work symbol (one work tape, so 1 · 3² = 9 entries).

Equations

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

Display demos