TM State Normalization and Binary Encoding

This file provides two pieces of general infrastructure for working with Turing machines:

1. State normalization: Convert any TM n with finite state type Q to an equivalent machine using states Fin (Fintype.card Q). This is needed whenever states must be represented as binary numbers (e.g., for encoding a TM description).

2. Binary encoding primitives: Fixed-width encodings for tape symbols, write symbols, directions, and natural numbers, with roundtrip correctness proofs.

Main definitions

State normalization

• TM.stateEquiv — canonical equivalence Q ≃ Fin (Fintype.card Q)
• TM.normalize — normalize state type to Fin (Fintype.card Q)
• TM.normalizeCfg — embed a config into the normalized state space
• TM.normalize_decidesInTime — behavioral equivalence

Binary encoding

• Γ.encode / Γ.decode — tape symbol ↔ 2 bits
• Γw.encode — write symbol → 2 bits
• Dir3.encode — direction → 2 bits
• Nat.toBits / Nat.fromBits — fixed-width big-endian binary

Enumeration

• allΓ — all 4 tape symbols in canonical order
• allΓFuncs — enumerate all Fin n → Γ functions

noncomputable def Complexity.TM.stateEquiv {n : ℕ} (tm : TM n) : tm.Q ≃ Fin (Fintype.card tm.Q)

The canonical equivalence between a TM's states and Fin (Fintype.card Q).

Equations

• tm.stateEquiv = Fintype.equivFin tm.Q

noncomputable def Complexity.TM.stateEquivOfCardEq {n k : ℕ} (tm : TM n) (hk : k = Fintype.card tm.Q) : tm.Q ≃ Fin k

The canonical equivalence cast to Fin k given k = Fintype.card Q.

Equations

• tm.stateEquivOfCardEq hk = ⋯ ▸ tm.stateEquiv

theorem Complexity.TM.stateEquivOfCardEq_val {n k : ℕ} (tm : TM n) (hk : k = Fintype.card tm.Q) (q : tm.Q) : ↑((tm.stateEquivOfCardEq hk) q) = ↑(tm.stateEquiv q)

stateEquivOfCardEq agrees with stateEquiv on values.

noncomputable def Complexity.TM.normalize {n : ℕ} (tm : TM n) : TM n

Normalize a TM's state type to Fin (Fintype.card Q) via the canonical equivalence. This preserves all computational behavior. Noncomputable because Fintype.equivFin uses choice.

Equations

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

noncomputable def Complexity.TM.normalizeCfg {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : Cfg n tm.normalize.Q

Configuration embedding: map a config with original states to normalized states.

Equations

• tm.normalizeCfg c = { state := tm.stateEquiv c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.normalize_step_comm {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : tm.normalize.step (tm.normalizeCfg c) = Option.map tm.normalizeCfg (tm.step c)

Stepping the normalized TM commutes with the state equivalence.

theorem Complexity.TM.normalize_reachesIn {n : ℕ} (tm : TM n) {t : ℕ} {c c' : Cfg n tm.Q} (h : tm.reachesIn t c c') : tm.normalize.reachesIn t (tm.normalizeCfg c) (tm.normalizeCfg c')

Multi-step simulation: normalized TM mirrors original TM.

theorem Complexity.TM.normalize_halted {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : tm.normalize.halted (tm.normalizeCfg c) ↔ tm.halted c

Halting is preserved by normalization.

theorem Complexity.TM.normalize_output {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : (tm.normalizeCfg c).output = c.output

Output is preserved by normalization.

theorem Complexity.TM.normalize_initCfg {n : ℕ} (tm : TM n) (x : List Bool) : tm.normalizeCfg (tm.initCfg x) = tm.normalize.initCfg x

The initial config normalizes correctly.

theorem Complexity.TM.normalize_decidesInTime {n : ℕ} (tm : TM n) {L : Language} {T : ℕ → ℕ} (h : tm.DecidesInTime L T) : tm.normalize.DecidesInTime L T

Normalized TM decides the same language in the same time.

def Complexity.Γ.encode : Γ → List Bool

Encode a tape symbol as 2 bits: 0→00, 1→01, □→10, ▷→11.

Equations

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

def Complexity.Γ.decode : List Bool → Option Γ

Decode 2 bits back to a tape symbol.

Equations

• Complexity.Γ.decode [false, false] = some Complexity.Γ.zero
• Complexity.Γ.decode [false, true] = some Complexity.Γ.one
• Complexity.Γ.decode [true, false] = some Complexity.Γ.blank
• Complexity.Γ.decode [true, true] = some Complexity.Γ.start
• Complexity.Γ.decode x✝ = none

def Complexity.Γw.encode : Γw → List Bool

Encode a write symbol as 2 bits: 0→00, 1→01, □→10.

Equations

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

def Complexity.Dir3.encode : Dir3 → List Bool

Encode a direction as 2 bits: L→00, R→01, S→10.

Equations

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

theorem Complexity.Γ.length_encode (g : Γ) : g.encode.length = 2

theorem Complexity.Γw.length_encode (g : Γw) : g.encode.length = 2

theorem Complexity.Dir3.length_encode (d : Dir3) : d.encode.length = 2

theorem Complexity.Γ.decode_encode (g : Γ) : decode g.encode = some g

Roundtrip: decode ∘ encode = some.

theorem Complexity.Γ.encode_injective : Function.Injective encode

Γ encoding is injective.

def Complexity.allΓ : List Γ

All 4 tape symbols in canonical order.

Equations

• Complexity.allΓ = [Complexity.Γ.zero, Complexity.Γ.one, Complexity.Γ.blank, Complexity.Γ.start]

theorem Complexity.mem_allΓ (g : Γ) : g ∈ allΓ

Every tape symbol appears in allΓ.

theorem Complexity.nodup_allΓ : allΓ.Nodup

allΓ contains no duplicates.

theorem Complexity.length_allΓ : allΓ.length = 4

allΓ has exactly 4 elements (one per Γ constructor).

def Complexity.allΓFuncs (n : ℕ) : List (Fin n → Γ)

Enumerate all functions Fin n → Γ in canonical (lexicographic) order.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.allΓFuncs 0 = [Fin.elim0]

theorem Complexity.mem_allΓFuncs (n : ℕ) (f : Fin n → Γ) : f ∈ allΓFuncs n

Every function Fin n → Γ appears in allΓFuncs n.