Interpreting machine descriptions

TMDesc.toTM turns a description into an actual single-work-tape machine: states are Fin (2^w + 1) (the extra state 2^w is the "never halts" sentinel produced when decoding a malformed halt field — it is unreachable, since every transition target is reduced mod 2^w), transitions look up the table, and head directions are sanitized to satisfy the ▷ ⇒ move right discipline.

descOfTM extracts a well-formed description from any single-work-tape machine: states are numbered by the canonical Fintype equivalence and the table lists every (state, symbols) combination densely.

Main results

• TMDesc.toTM — interpreter; the specification of the universal machine
• descOfTM / descOfTM_wf — every TM 1 has a well-formed description
• descOfTM_step_comm — step-exact correspondence between M and (descOfTM M).toTM
• descOfTM_decidesInTime — language and running time carry over exactly

def Complexity.TMDesc.toTM (d : TMDesc) : TM 1

Interpret a description as a single-work-tape machine. States are Fin (2^w + 1); state 2^w is the never-halting sentinel (reachable only as a malformed qhalt, never as a transition target). Directions are sanitized to satisfy the ▷ ⇒ right discipline.

Equations

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

noncomputable def Complexity.TM.descAct (M : TM 1) (q : Fin (Fintype.card M.Q)) (si sw so : Γ) : DescAct

The table action of M (with states numbered by stateEquiv) on the key (q, si, sw, so).

Equations

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

noncomputable def Complexity.TM.descEntry (M : TM 1) (q : Fin (Fintype.card M.Q)) (si sw so : Γ) : DescEntry

The dense table row for key (q, si, sw, so).

Equations

• M.descEntry q si sw so = { q := ↑q, si := si, sw := sw, so := so, act := M.descAct q si sw so }

noncomputable def Complexity.TM.descOfTM (M : TM 1) : TMDesc

Extract a description from a single-work-tape machine: states are numbered by the canonical equivalence, the state field width is the state count itself (k < 2^k), and the table densely lists every (state, symbols) combination.

Equations

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

theorem Complexity.TM.descOfTM_wf (M : TM 1) : M.descOfTM.WF

theorem Complexity.TM.descOfTM_lookup (M : TM 1) (q : Fin (Fintype.card M.Q)) (si sw so : Γ) : M.descOfTM.lookup (↑q) si sw so = M.descAct q si sw so

Looking up an in-range key in the extracted table returns the extracted action.

noncomputable def Complexity.TM.descCfg (M : TM 1) (c : Cfg 1 M.Q) : Cfg 1 M.descOfTM.toTM.Q

Configuration embedding into the interpreted description's state space: states are renumbered by stateEquiv (values below card Q < 2^card Q), tapes are unchanged.

Equations

• M.descCfg c = { state := ⟨↑(M.stateEquiv c.state), ⋯⟩, input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.descOfTM_halted (M : TM 1) (c : Cfg 1 M.Q) : M.descOfTM.toTM.halted (M.descCfg c) ↔ M.halted c

Halting is preserved by the embedding.

theorem Complexity.TM.descOfTM_initCfg (M : TM 1) (x : List Bool) : M.descCfg (M.initCfg x) = M.descOfTM.toTM.initCfg x

The initial configuration embeds correctly.

theorem Complexity.TM.descOfTM_step_comm (M : TM 1) (c : Cfg 1 M.Q) : M.descOfTM.toTM.step (M.descCfg c) = Option.map M.descCfg (M.step c)

Stepping the interpreted description commutes with the configuration embedding.

theorem Complexity.TM.descOfTM_reachesIn (M : TM 1) {t : ℕ} {c c' : Cfg 1 M.Q} (h : M.reachesIn t c c') : M.descOfTM.toTM.reachesIn t (M.descCfg c) (M.descCfg c')

Multi-step correspondence.

theorem Complexity.TM.descOfTM_decidesInTime (M : TM 1) {L : Language} {T : ℕ → ℕ} (h : M.DecidesInTime L T) : M.descOfTM.toTM.DecidesInTime L T

Extraction fidelity: the interpreted description of a machine decides the same language in exactly the same time.

theorem Complexity.TM.exists_wf_desc_decidesInTime {L : Language} {T : ℕ → ℕ} (M : TM 1) (h : M.DecidesInTime L T) : ∃ (d : TMDesc), d.WF ∧ d.toTM.DecidesInTime L T

Every language decidable by a single-work-tape machine is decidable by an interpreted well-formed description in the same time bound.