Machine descriptions for the universal Turing machine

A TMDesc describes a single-work-tape deterministic Turing machine as finite data: a state bit-width w (states are numbers below 2^w), start and halt states, and a transition table (List DescEntry, first match wins).

Encoding

A description is laid out as a string over the writable alphabet Γw = {0, 1, □}, with □ acting as a field/entry separator:

qstart(w bits) □ qhalt(w bits) □ entry₀ □ entry₁ □ ⋯ □ entryₘ □ □

Each entry is 2w + 16 bit-symbols with no internal separators (field widths are determined by w): key q(w) si(2) sw(2) so(2), action q'(w) ww(2) wo(2) di(2) dw(2) dOut(2). The state width w is defined by the length of the leading qstart field. The table ends at the first empty segment (□□), so trailing junk is ignored — every description has infinitely many encodings (decodeDesc_encodeDesc_append), which the hierarchy-theorem diagonalization relies on.

The binary encoding encodeDesc : TMDesc → List Bool maps each Γw symbol to 2 bits via Γw.encode; decodeDesc : List Bool → TMDesc is total (unparseable segments are skipped, missing fields default), so every binary string denotes some machine.

Main definitions

• DescAct, DescEntry, TMDesc — machine descriptions
• TMDesc.lookup — first-match transition lookup with default action
• TMDesc.syms / encodeDesc — canonical encoding
• parseSyms / decodeDesc — total decoding
• TMDesc.WF — well-formedness (all state fields below 2^w)

Main results

• decodeDesc_encodeDesc — roundtrip on well-formed descriptions
• decodeDesc_encodeDesc_append — roundtrip ignores trailing junk

structure Complexity.DescAct : Type

The action part of a transition-table entry: next state, writes for the work and output tapes, and directions for the input, work, and output heads (matching the component order of TM.δ).

• q' : ℕ

  The next state (as a number below 2^w).

• ww : Γw

  The symbol written to the work tape.

• wo : Γw

  The symbol written to the output tape.

• di : Dir3

  The input-head direction.

• dw : Dir3

  The work-head direction.

• dOut : Dir3

  The output-head direction.

def Complexity.instDecidableEqDescAct.decEq (x✝ x✝¹ : DescAct) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.instDecidableEqDescAct : DecidableEq DescAct

Equations

• Complexity.instDecidableEqDescAct = Complexity.instDecidableEqDescAct.decEq

structure Complexity.DescEntry : Type

One transition-table row for a single-work-tape machine: the key (state and the three symbols under the input/work/output heads) together with the action to take.

• q : ℕ

  The state this row fires in.

• si : Γ

  The symbol under the input head.

• sw : Γ

  The symbol under the work head.

• so : Γ

  The symbol under the output head.

• act : DescAct

  The action to take when the key matches.

def Complexity.instDecidableEqDescEntry.decEq (x✝ x✝¹ : DescEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.instDecidableEqDescEntry : DecidableEq DescEntry

Equations

• Complexity.instDecidableEqDescEntry = Complexity.instDecidableEqDescEntry.decEq

structure Complexity.TMDesc : Type

A description of a single-work-tape deterministic TM: state bit-width w (states are numbers below 2^w), start and halt states, and a transition table with first-match-wins semantics (TMDesc.lookup).

• w : ℕ

  The state bit-width: states are numbers below 2^w.

• qstart : ℕ

  The start state.

• qhalt : ℕ

  The halt state.

• entries : List DescEntry

  The transition table, first match wins.

def Complexity.instDecidableEqTMDesc.decEq (x✝ x✝¹ : TMDesc) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.instDecidableEqTMDesc : DecidableEq TMDesc

Equations

• Complexity.instDecidableEqTMDesc = Complexity.instDecidableEqTMDesc.decEq

def Complexity.TMDesc.readback : Γ → Γw

Identity write-back: the Γw symbol that leaves a read symbol unchanged when written. ▷ maps to □, which is harmless: ▷ occurs only at cell 0, where writes are structural no-ops.

Equations

• Complexity.TMDesc.readback Complexity.Γ.zero = Complexity.Γw.zero
• Complexity.TMDesc.readback Complexity.Γ.one = Complexity.Γw.one
• Complexity.TMDesc.readback Complexity.Γ.blank = Complexity.Γw.blank
• Complexity.TMDesc.readback Complexity.Γ.start = Complexity.Γw.blank

def Complexity.TMDesc.defaultAct (d : TMDesc) (sw so : Γ) : DescAct

The default action taken when no table entry matches: go to the halt state, write back what was read, and keep all heads in place.

Equations

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

def Complexity.TMDesc.lookup (d : TMDesc) (q : ℕ) (si sw so : Γ) : DescAct

First-match transition lookup; missing keys take the default action.

Equations

• d.lookup q si sw so = match List.find? (fun (e : Complexity.DescEntry) => e.q == q && e.si == si && e.sw == sw && e.so == so) d.entries with | some e => e.act | none => d.defaultAct sw so

structure Complexity.TMDesc.WF (d : TMDesc) : Prop

A description is well-formed when every state field is below 2^w, so the fixed-width binary encoding is faithful.

• qstart_lt : d.qstart < 2 ^ d.w
• qhalt_lt : d.qhalt < 2 ^ d.w
• entries_q_lt (e : DescEntry) : e ∈ d.entries → e.q < 2 ^ d.w
• entries_q'_lt (e : DescEntry) : e ∈ d.entries → e.act.q' < 2 ^ d.w

def Complexity.bitSym (b : Bool) : Γw

A bit as a desc-tape symbol.

Equations

• Complexity.bitSym b = if b = true then Complexity.Γw.one else Complexity.Γw.zero

def Complexity.bitsToSyms (l : List Bool) : List Γw

A bit string as desc-tape symbols.

Equations

• Complexity.bitsToSyms l = List.map Complexity.bitSym l

@[simp]

theorem Complexity.bitsToSyms_length (l : List Bool) : (bitsToSyms l).length = l.length

@[simp]

theorem Complexity.bitsToSyms_append (a b : List Bool) : bitsToSyms (a ++ b) = bitsToSyms a ++ bitsToSyms b

theorem Complexity.bitSym_ne_blank (b : Bool) : bitSym b ≠ Γw.blank

theorem Complexity.bitsToSyms_ne_blank {l : List Bool} {s : Γw} (h : s ∈ bitsToSyms l) : s ≠ Γw.blank

def Complexity.DescEntry.syms (w : ℕ) (e : DescEntry) : List Γw

The desc-tape symbols of one table entry (given state width w): q(w) si(2) sw(2) so(2) q'(w) ww(2) wo(2) di(2) dw(2) dOut(2), 2w + 16 symbols with no separators.

Equations

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

theorem Complexity.DescEntry.syms_length (w : ℕ) (e : DescEntry) : (syms w e).length = 2 * w + 16

theorem Complexity.DescEntry.syms_ne_blank {w : ℕ} {e : DescEntry} {s : Γw} (h : s ∈ syms w e) : s ≠ Γw.blank

def Complexity.TMDesc.syms (d : TMDesc) : List Γw

The desc-tape symbols of a description: qstart(w) □ qhalt(w) □ entry₀ □ ⋯ □ entryₘ □ □.

Equations

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

def Complexity.encodeDesc (d : TMDesc) : List Bool

The canonical binary encoding of a description: each desc-tape symbol becomes 2 bits via Γw.encode.

Equations

• Complexity.encodeDesc d = List.flatMap Complexity.Γw.encode d.syms

def Complexity.symOfPair : Bool → Bool → Γw

Total 2-bit-group decoding: 00 → 0, 01 → 1, and both remaining patterns (10, 11) map to the separator □. Left inverse of Γw.encode on the three encodable patterns.

Equations

• Complexity.symOfPair false false = Complexity.Γw.zero
• Complexity.symOfPair false true = Complexity.Γw.one
• Complexity.symOfPair x✝¹ x✝ = Complexity.Γw.blank

def Complexity.groupPairs : List Bool → List Γw

Group a bit string into consecutive pairs and decode each; a trailing odd bit is dropped.

Equations

• Complexity.groupPairs (b₀ :: b₁ :: rest) = Complexity.symOfPair b₀ b₁ :: Complexity.groupPairs rest
• Complexity.groupPairs x✝ = []

theorem Complexity.groupPairs_flatMap_encode (l : List Γw) : groupPairs (List.flatMap Γw.encode l) = l

Decoding pairs is a left inverse of symbol-wise binary encoding.

theorem Complexity.groupPairs_append_of_even {a : List Bool} : a.length % 2 = 0 → ∀ (b : List Bool), groupPairs (a ++ b) = groupPairs a ++ groupPairs b

groupPairs distributes over appending at an even boundary.

theorem Complexity.flatMap_encode_length_even (l : List Γw) : (List.flatMap Γw.encode l).length % 2 = 0

Every symbol-wise binary encoding has even length.

def Complexity.symBit? : Γw → Option Bool

The bit denoted by a desc-tape symbol, if any.

Equations

• Complexity.symBit? Complexity.Γw.zero = some false
• Complexity.symBit? Complexity.Γw.one = some true
• Complexity.symBit? Complexity.Γw.blank = none

@[simp]

theorem Complexity.symBit?_bitSym (b : Bool) : symBit? (bitSym b) = some b

def Complexity.takeField : List Γw → List Γw × List Γw

Split off the first field: the symbols before the first □, and the rest after it. An empty first field means the input started with a separator (or was empty).

Equations

• Complexity.takeField [] = ([], [])
• Complexity.takeField (Complexity.Γw.blank :: rest) = ([], rest)
• Complexity.takeField (s :: rest) = (s :: (Complexity.takeField rest).1, (Complexity.takeField rest).2)

theorem Complexity.takeField_rest_length (l : List Γw) : (takeField l).2.length ≤ l.length

theorem Complexity.takeField_cons_rest_length (s : Γw) (rest : List Γw) : (takeField (s :: rest)).2.length ≤ rest.length

On a nonempty input the remainder after the first field is strictly shorter — the parse loop terminates.

theorem Complexity.takeField_append {f : List Γw} (hf : ∀ s ∈ f, s ≠ Γw.blank) (r : List Γw) : takeField (f ++ Γw.blank :: r) = (f, r)

takeField recovers a blank-free field followed by a separator.

def Complexity.fieldNat (f : List Γw) : ℕ

The number denoted by a field (its bit symbols, read big-endian).

Equations

• Complexity.fieldNat f = Nat.fromBits (List.filterMap Complexity.symBit? f)

@[simp]

theorem Complexity.filterMap_symBit?_bitsToSyms (l : List Bool) : List.filterMap symBit? (bitsToSyms l) = l

theorem Complexity.fieldNat_bitsToSyms_toBits {w v : ℕ} (hv : v < 2 ^ w) : fieldNat (bitsToSyms (w.toBits v)) = v

def Complexity.decΓ (l : List Bool) : Γ

Total read-symbol decoder (left inverse of Γ.encode).

Equations

• Complexity.decΓ [false, false] = Complexity.Γ.zero
• Complexity.decΓ [false, true] = Complexity.Γ.one
• Complexity.decΓ [true, false] = Complexity.Γ.blank
• Complexity.decΓ [true, true] = Complexity.Γ.start
• Complexity.decΓ l = Complexity.Γ.blank

def Complexity.decΓw (l : List Bool) : Γw

Total write-symbol decoder; 11 decodes to □.

Equations

• Complexity.decΓw [false, false] = Complexity.Γw.zero
• Complexity.decΓw [false, true] = Complexity.Γw.one
• Complexity.decΓw l = Complexity.Γw.blank

def Complexity.decDir (l : List Bool) : Dir3

Total direction decoder; 11 decodes to stay.

Equations

• Complexity.decDir [false, false] = Complexity.Dir3.left
• Complexity.decDir [false, true] = Complexity.Dir3.right
• Complexity.decDir l = Complexity.Dir3.stay

@[simp]

theorem Complexity.decΓ_encode (s : Γ) : decΓ s.encode = s

@[simp]

theorem Complexity.decΓw_encode (s : Γw) : decΓw s.encode = s

@[simp]

theorem Complexity.decDir_encode (d : Dir3) : decDir d.encode = d

def Complexity.parseEntry (w : ℕ) (seg : List Γw) : Option DescEntry

Parse one table entry from a (blank-free) segment: reject if shorter than 2w + 16, otherwise decode the fixed-width fields sequentially from the prefix and ignore any excess.

Equations

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

@[irreducible]

def Complexity.parseEntries (w : ℕ) : List Γw → List DescEntry

Parse the table: segments are separated by □; parseable segments become entries, unparseable (too short) segments are skipped, and the first empty segment (a □□ or end of input) terminates the table.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.parseEntries w [] = []
• Complexity.parseEntries w (Complexity.Γw.blank :: rest) = []

def Complexity.parseSyms (l : List Γw) : TMDesc

Decode a desc-tape symbol string into a description. The state width is the length of the leading qstart field; a qhalt field of any other length denotes the out-of-range sentinel 2^w (a machine that never halts), matching the universal machine's symbol-wise comparison.

Equations

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

def Complexity.decodeDesc (α : List Bool) : TMDesc

Total decoding of a binary string into a machine description.

Equations

• Complexity.decodeDesc α = Complexity.parseSyms (Complexity.groupPairs α)

theorem Complexity.parseEntry_syms {w : ℕ} {e : DescEntry} (hq : e.q < 2 ^ w) (hq' : e.act.q' < 2 ^ w) : parseEntry w (DescEntry.syms w e) = some e

Parsing one encoded entry recovers it (when its state fields fit in width w).

theorem Complexity.parseEntries_blank (w : ℕ) (rest : List Γw) : parseEntries w (Γw.blank :: rest) = []

A leading separator (empty segment) terminates the table parse.

theorem Complexity.parseEntries_cons_of_ne_blank {s : Γw} (hs : s ≠ Γw.blank) (w : ℕ) (rest : List Γw) : parseEntries w (s :: rest) = match parseEntry w (takeField (s :: rest)).1 with | some e => e :: parseEntries w (takeField (s :: rest)).2 | none => parseEntries w (takeField (s :: rest)).2

One-step unfolding of the table parse on a segment-headed input.

theorem Complexity.parseEntries_syms {w : ℕ} {es : List DescEntry} (hq : ∀ e ∈ es, e.q < 2 ^ w) (hq' : ∀ e ∈ es, e.act.q' < 2 ^ w) (junk : List Γw) : parseEntries w (List.flatMap (fun (e : DescEntry) => DescEntry.syms w e ++ [Γw.blank]) es ++ Γw.blank :: junk) = es

Parsing the encoded table recovers it, ignoring anything after the terminating empty segment.

theorem Complexity.decodeDesc_encodeDesc_append {d : TMDesc} (hd : d.WF) (junk : List Bool) : decodeDesc (encodeDesc d ++ junk) = d

Roundtrip with padding: decoding an encoded well-formed description recovers it exactly, no matter what junk follows the encoding. This gives every description infinitely many encodings — the padding fact the hierarchy-theorem diagonalization relies on.

theorem Complexity.decodeDesc_encodeDesc {d : TMDesc} (hd : d.WF) : decodeDesc (encodeDesc d) = d

Roundtrip: decoding an encoded well-formed description recovers it.