Helper Lemmas for TM → Grammar Construction

This file contains the detailed helper lemmas needed to prove the correctness of the tmToGrammar construction.

Encoding TM configurations as sentential forms

A TM0 configuration ⟨q, tape⟩ together with an "original input track" is encoded as a sentential form of the grammar. The encoding represents a finite window of the tape as a sequence of cell/headCell nonterminals flanked by boundary markers.

structure TwoTrackConfig {T Λ : Type} : Type

A "two-track tape segment" encodes a finite portion of the TM tape along with the original input at each position.

leftCells are the cells to the left of the head (in order from left to right). headState is the TM state at the head position. headOrig is the original input at the head position. headCur is the current tape content at the head position. rightCells are the cells to the right of the head (in order from left to right).

Each cell is a pair (original, current).

• leftCells : List (Option T × Option T)
• headState : Λ
• headOrig : Option T
• headCur : Option T
• rightCells : List (Option T × Option T)

def encodeTwoTrack {T Λ : Type} (cfg : TwoTrackConfig) : List (symbol T (TMtoGrammarNT T Λ))

Encode a TwoTrackConfig as a sentential form of the grammar.

Equations

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

def initTwoTrack {T Λ : Type} [Inhabited Λ] (w : List T) : TwoTrackConfig

The initial two-track configuration for input w. The head is at the leftmost position (or on blank for empty input).

Equations

• initTwoTrack [] = { leftCells := [], headState := default, headOrig := none, headCur := none, rightCells := [] }
• initTwoTrack (t :: ts) = { leftCells := [], headState := default, headOrig := some t, headCur := some t, rightCells := List.map (fun (t' : T) => (some t', some t')) ts }

Phase 1: Generation

The grammar derives the encoding of the initial configuration from [start]:

1. S → leftBound · genMore · rightBound
2. Repeatedly: genMore → genMore · cell(tᵢ) (adding cells right-to-left)
3. genMore → headCell(q₀, t₁) (or headCell(q₀, none, none) for empty input)

theorem generation_derives {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (w : List T) : grammar_derives (tmToGrammar T Λ M) [symbol.nonterminal TMtoGrammarNT.start] (encodeTwoTrack (initTwoTrack w))

Phase 3: Cleanup

After the TM halts, the grammar converts all nonterminals to terminals.

def encodeHalted {T Λ : Type} (originals : List (Option T)) : List (symbol T (TMtoGrammarNT T Λ))

Encode the "halted" configuration: all cells converted to haltCells.

Equations

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

def extractInput {T : Type} (originals : List (Option T)) : List T

Extract the original input from a list of originals (keep only some values).

Equations

• extractInput originals = List.filterMap id originals

theorem haltCells_to_terminals {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (originals : List (Option T)) : grammar_derives (tmToGrammar T Λ M) (List.map (fun (orig : Option T) => symbol.nonterminal (TMtoGrammarNT.haltCell orig)) originals) (List.map symbol.terminal (List.filterMap id originals))

theorem remove_boundaries {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (originals : List (Option T)) : grammar_derives (tmToGrammar T Λ M) (encodeHalted originals) (List.map (fun (orig : Option T) => symbol.nonterminal (TMtoGrammarNT.haltCell orig)) originals)

theorem cleanup_derives {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (originals : List (Option T)) : grammar_derives (tmToGrammar T Λ M) (encodeHalted originals) (List.map symbol.terminal (extractInput originals))

Rule membership helpers

theorem gen_rule_mem {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ generationRules T Λ M) : r ∈ (tmToGrammar T Λ M).rules

A rule from the generation rules is in the grammar.

theorem sim_rule_mem {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ simulationRules T Λ M) : r ∈ (tmToGrammar T Λ M).rules

A rule from the simulation rules is in the grammar.

theorem cleanup_rule_mem {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ cleanupRules T Λ M) : r ∈ (tmToGrammar T Λ M).rules

A rule from the cleanup rules is in the grammar.

def twoTrackOriginals {T Λ : Type} (cfg : TwoTrackConfig) : List (Option T)

Get the originals from a TwoTrackConfig.

Equations

• twoTrackOriginals cfg = List.map Prod.fst cfg.leftCells ++ [cfg.headOrig] ++ List.map Prod.fst cfg.rightCells

Phase 2: Simulation

The simulation phase shows that each TM0 step can be mirrored by a grammar derivation step on the encoded sentential form.

noncomputable def stepTwoTrack {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (cfg : TwoTrackConfig) : Option TwoTrackConfig

Compute the next TwoTrackConfig after one TM0 step. Returns none if the TM halts.

Equations

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

theorem stepTwoTrack_preserves_extractInput {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (cfg cfg' : TwoTrackConfig) (hstep : stepTwoTrack M cfg = some cfg') : extractInput (twoTrackOriginals cfg') = extractInput (twoTrackOriginals cfg)

theorem mem_allOptT {T : Type} [Fintype T] (x : Option T) : x ∈ allOptT T

theorem mem_allΛ {Λ : Type} [Fintype Λ] (q : Λ) : q ∈ allΛ Λ

theorem sim_write {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (q q' : Λ) (orig γ γ' : Option T) (hM : M q γ = some (q', Turing.TM0.Stmt.write γ')) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_transforms (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.headCell q orig γ)] ++ suffix_) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.headCell q' orig γ')] ++ suffix_)

theorem sim_move_right {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (q q' : Λ) (orig γ orig' γ' : Option T) (hM : M q γ = some (q', Turing.TM0.Stmt.move Turing.Dir.right)) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_transforms (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.headCell q orig γ), symbol.nonterminal (TMtoGrammarNT.cell orig' γ')] ++ suffix_) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.cell orig γ), symbol.nonterminal (TMtoGrammarNT.headCell q' orig' γ')] ++ suffix_)

theorem sim_move_right_boundary {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (q q' : Λ) (orig γ : Option T) (hM : M q γ = some (q', Turing.TM0.Stmt.move Turing.Dir.right)) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_transforms (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.headCell q orig γ), symbol.nonterminal TMtoGrammarNT.rightBound] ++ suffix_) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.cell orig γ), symbol.nonterminal (TMtoGrammarNT.headCell q' none none), symbol.nonterminal TMtoGrammarNT.rightBound] ++ suffix_)

theorem sim_move_left {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (q q' : Λ) (orig γ orig'' γ'' : Option T) (hM : M q γ = some (q', Turing.TM0.Stmt.move Turing.Dir.left)) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_transforms (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.cell orig'' γ''), symbol.nonterminal (TMtoGrammarNT.headCell q orig γ)] ++ suffix_) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.headCell q' orig'' γ''), symbol.nonterminal (TMtoGrammarNT.cell orig γ)] ++ suffix_)

theorem sim_move_left_boundary {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (q q' : Λ) (orig γ : Option T) (hM : M q γ = some (q', Turing.TM0.Stmt.move Turing.Dir.left)) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_transforms (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal (TMtoGrammarNT.headCell q orig γ)] ++ suffix_) (prefix_ ++ [symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal (TMtoGrammarNT.headCell q' none none), symbol.nonterminal (TMtoGrammarNT.cell orig γ)] ++ suffix_)

theorem simulation_one_step {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (cfg cfg' : TwoTrackConfig) (hstep : stepTwoTrack M cfg = some cfg') : grammar_derives (tmToGrammar T Λ M) (encodeTwoTrack cfg) (encodeTwoTrack cfg')

theorem simulation_multi_step {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (cfg : TwoTrackConfig) (n : ℕ) (cfg' : TwoTrackConfig) (hsteps : (fun (c : Option TwoTrackConfig) => c >>= stepTwoTrack M)^[n] (some cfg) = some cfg') : grammar_derives (tmToGrammar T Λ M) (encodeTwoTrack cfg) (encodeTwoTrack cfg')

Phase 2.5: Halt conversion

When the TM halts, convert the two-track encoding to the halted encoding.

theorem halt_headCell_to_haltCell {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (q : Λ) (orig cur : Option T) (h_halts : M q cur = none) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_transforms (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.headCell q orig cur)] ++ suffix_) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.haltCell orig)] ++ suffix_)

theorem propagate_halt_right {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (cells : List (Option T × Option T)) (orig : Option T) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_derives (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.haltCell orig)] ++ List.map (fun (x : Option T × Option T) => match x with | (o, c) => symbol.nonterminal (TMtoGrammarNT.cell o c)) cells ++ suffix_) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.haltCell orig)] ++ List.map (fun (x : Option T × Option T) => match x with | (o, snd) => symbol.nonterminal (TMtoGrammarNT.haltCell o)) cells ++ suffix_)

theorem propagate_halt_left_one_step {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (o c anchor_orig : Option T) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_transforms (tmToGrammar T Λ M) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.cell o c), symbol.nonterminal (TMtoGrammarNT.haltCell anchor_orig)] ++ suffix_) (prefix_ ++ [symbol.nonterminal (TMtoGrammarNT.haltCell o), symbol.nonterminal (TMtoGrammarNT.haltCell anchor_orig)] ++ suffix_)

theorem propagate_halt_left {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (cells : List (Option T × Option T)) (anchor_orig : Option T) (prefix_ suffix_ : List (symbol T (TMtoGrammarNT T Λ))) : grammar_derives (tmToGrammar T Λ M) (prefix_ ++ List.map (fun (x : Option T × Option T) => match x with | (o, c) => symbol.nonterminal (TMtoGrammarNT.cell o c)) cells ++ [symbol.nonterminal (TMtoGrammarNT.haltCell anchor_orig)] ++ suffix_) (prefix_ ++ List.map (fun (x : Option T × Option T) => match x with | (o, snd) => symbol.nonterminal (TMtoGrammarNT.haltCell o)) cells ++ [symbol.nonterminal (TMtoGrammarNT.haltCell anchor_orig)] ++ suffix_)

theorem halt_to_halted {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (cfg : TwoTrackConfig) (h_halts : M cfg.headState cfg.headCur = none) : grammar_derives (tmToGrammar T Λ M) (encodeTwoTrack cfg) (encodeHalted (twoTrackOriginals cfg))

Composing all phases

theorem extractInput_initTwoTrack {T Λ : Type} [Inhabited Λ] (w : List T) : extractInput (twoTrackOriginals (initTwoTrack w)) = w

Correspondence between TM0.Cfg and TwoTrackConfig

structure TMCorresponds {T Λ : Type} (tc : TwoTrackConfig) (tmCfg : Turing.TM0.Cfg (Option T) Λ) : Prop

A TwoTrackConfig corresponds to a TM0.Cfg if the head state, head symbol, and tape contents match (with the tape being blank beyond the TwoTrackConfig window).

• state_eq : tc.headState = tmCfg.q
• head_eq : tc.headCur = tmCfg.Tape.head
• left_match (i : ℕ) : (List.map Prod.snd tc.leftCells.reverse).getI i = tmCfg.Tape.left.nth i
• right_match (i : ℕ) : (List.map Prod.snd tc.rightCells).getI i = tmCfg.Tape.right.nth i

theorem initCorresponds {T Λ : Type} [Inhabited Λ] (w : List T) : TMCorresponds (initTwoTrack w) (Turing.TM0.init (List.map some w))

theorem corresponds_step_none {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (tmCfg : Turing.TM0.Cfg (Option T) Λ) (hcorr : TMCorresponds tc tmCfg) (hhalt : Turing.TM0.step M tmCfg = none) : stepTwoTrack M tc = none

theorem corresponds_step_some {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (tmCfg tmCfg' : Turing.TM0.Cfg (Option T) Λ) (hcorr : TMCorresponds tc tmCfg) (hstep : Turing.TM0.step M tmCfg = some tmCfg') : ∃ (tc' : TwoTrackConfig), stepTwoTrack M tc = some tc' ∧ TMCorresponds tc' tmCfg'

Main Correctness Theorems

theorem sim_reaches_halts {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (tmCfg : Turing.TM0.Cfg (Option T) Λ) (hcorr : TMCorresponds tc tmCfg) (tmCfg_halt : Turing.TM0.Cfg (Option T) Λ) (hreaches : Turing.Reaches (Turing.TM0.step M) tmCfg tmCfg_halt) (hhalt : Turing.TM0.step M tmCfg_halt = none) : ∃ (tc_final : TwoTrackConfig), grammar_derives (tmToGrammar T Λ M) (encodeTwoTrack tc) (encodeTwoTrack tc_final) ∧ M tc_final.headState tc_final.headCur = none ∧ extractInput (twoTrackOriginals tc_final) = extractInput (twoTrackOriginals tc)

theorem tmToGrammar_generates_of_halts {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (w : List T) (h : (Turing.TM0.eval M (List.map some w)).Dom) : grammar_generates (tmToGrammar T Λ M) w