Equivalence of Unrestricted Grammars and Turing Machines

This file defines the grammar construction for simulating TM0 machines, and states the equivalence between unrestricted (Type-0) grammars and Turing machines.

The correctness proofs and the main equivalence theorem are in TMtoGrammarHelpers.lean.

Main definitions

• is_TM: A language is TM-recognizable if there exists a finite-state Turing machine (using Mathlib's Turing.TM0 model) that halts on input w iff w ∈ L.
• TMtoGrammarNT: Nonterminal symbols for the grammar simulating a TM.
• tmToGrammar: The grammar that simulates a TM0 machine.

Construction

We construct an unrestricted grammar that simulates a TM0 machine using "two-track" nonterminals.

inductive TMtoGrammarNT (T Λ : Type) : Type

Nonterminals for the grammar simulating a TM0 machine.

• start: Initial symbol
• genMore: Generation-phase marker for adding more input cells
• cell orig cur: Tape cell with original input orig and current content cur
• headCell q orig cur: Head position in state q, original input orig, current cur
• leftBound / rightBound: Tape boundary markers
• haltCell orig: Cell in cleanup phase, remembering original input orig

• start {T Λ : Type} : TMtoGrammarNT T Λ
• genMore {T Λ : Type} : TMtoGrammarNT T Λ
• cell {T Λ : Type} : Option T → Option T → TMtoGrammarNT T Λ
• headCell {T Λ : Type} : Λ → Option T → Option T → TMtoGrammarNT T Λ
• leftBound {T Λ : Type} : TMtoGrammarNT T Λ
• rightBound {T Λ : Type} : TMtoGrammarNT T Λ
• haltCell {T Λ : Type} : Option T → TMtoGrammarNT T Λ

noncomputable def allOptT (T : Type) [Fintype T] : List (Option T)

All values of Option T.

Equations

• allOptT T = none :: List.map some Finset.univ.val.toList

noncomputable def allΛ (Λ : Type) [Fintype Λ] : List Λ

All values of Λ.

Equations

• allΛ Λ = Finset.univ.val.toList

noncomputable def generationRules (T : Type) [Fintype T] (Λ : Type) [Inhabited Λ] : Turing.TM0.Machine (Option T) Λ → List (grule T (TMtoGrammarNT T Λ))

Generation rules: nondeterministically create an initial TM configuration for an arbitrary input word.

The grammar builds the initial configuration from right to left:

1. S → leftBound · genMore · rightBound
2. Repeatedly: genMore → genMore · cell(some t, some t) (adds cells to the RIGHT)
3. Finally: genMore → headCell(q₀, some t, some t) or genMore → headCell(q₀, none, none) (replaces genMore with the TM head, placing it at the leftmost position)

For input [t₁, t₂, ..., tₙ], the derivation is: S → LB · genMore · RB → LB · genMore · cell(tₙ) · RB → ... → LB · genMore · cell(t₂) · ... · cell(tₙ) · RB → LB · headCell(q₀, t₁) · cell(t₂) · ... · cell(tₙ) · RB

Equations

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

noncomputable def simulationRules (T : Type) [Fintype T] (Λ : Type) [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) : List (grule T (TMtoGrammarNT T Λ))

Simulation rules: encode TM transitions as grammar rules.

For each (q, γ) with M q γ = some (q', action):

• Write γ': headCell(q, orig, γ) → headCell(q', orig, γ')
• Move right: headCell(q, orig, γ) cell(orig', γ') → cell(orig, γ) headCell(q', orig', γ') (with boundary extension when at the right edge)
• Move left: cell(o'', γ'') headCell(q, orig, γ) → headCell(q', o'', γ'') cell(orig, γ) (with boundary extension when at the left edge)

Equations

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

noncomputable def cleanupRules (T : Type) [Fintype T] (Λ : Type) [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) : List (grule T (TMtoGrammarNT T Λ))

Cleanup rules: when TM halts, extract original input as terminals.

1. Convert halted head cell to halt marker
2. Propagate halt to all remaining cells
3. Replace halt markers with original terminal symbols (or ε for blanks)
4. Remove boundary markers

Equations

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

noncomputable def tmToGrammar (T : Type) [Fintype T] (Λ : Type) [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) : grammar T

The grammar simulating TM0 machine M.

Equations

• tmToGrammar T Λ M = { nt := TMtoGrammarNT T Λ, initial := TMtoGrammarNT.start, rules := generationRules T Λ M ++ simulationRules T Λ M ++ cleanupRules T Λ M }