Rational hitting lists: stack simulation

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/StackSimulation.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.RationalHitting.TMTime.StackToOne.go_time {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) {k : K} (o : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) {S : List (Γ k)} {L : Turing.ListBlank ((k : K) → Option (Γ k))} (hL : Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse) (n : ℕ) (H : n ≤ S.length) : exec (Turing.TM1.step (Turing.TM2to1.tr M)) n { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) } = some { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) }

theorem Complexity.RationalHitting.TMTime.StackToOne.return_time {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) {q : Turing.TM2.Stmt Γ Λ σ} {v : σ} {L : Turing.ListBlank ((k : K) → Option (Γ k))} (n : ℕ) : exec (Turing.TM1.step (Turing.TM2to1.tr M)) n { l := some (Turing.TM2to1.Λ'.ret q), var := v, Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) } = some { l := some (Turing.TM2to1.Λ'.ret q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }

def Complexity.RationalHitting.TMTime.StackToOne.stackWeight {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : Turing.TM2.Stmt Γ Λ σ → ℕ

Number of stack-access operations in a compiled statement.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.TMTime.StackToOne.stackWeight (Turing.TM2.Stmt.push k a q) = Complexity.RationalHitting.TMTime.StackToOne.stackWeight q + 1
• Complexity.RationalHitting.TMTime.StackToOne.stackWeight (Turing.TM2.Stmt.peek k a q) = Complexity.RationalHitting.TMTime.StackToOne.stackWeight q + 1
• Complexity.RationalHitting.TMTime.StackToOne.stackWeight (Turing.TM2.Stmt.pop k a q) = Complexity.RationalHitting.TMTime.StackToOne.stackWeight q + 1
• Complexity.RationalHitting.TMTime.StackToOne.stackWeight (Turing.TM2.Stmt.load a q) = Complexity.RationalHitting.TMTime.StackToOne.stackWeight q
• Complexity.RationalHitting.TMTime.StackToOne.stackWeight (Turing.TM2.Stmt.goto a) = 0
• Complexity.RationalHitting.TMTime.StackToOne.stackWeight Turing.TM2.Stmt.halt = 0

theorem Complexity.RationalHitting.TMTime.StackToOne.stackWeight_run {K : Type v_1} {Γ : K → Type v_2} {Λ : Type v_3} {σ : Type v_4} {k : K} (o : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ) : stackWeight (Turing.TM2to1.stRun o q) = stackWeight q + 1

theorem Complexity.RationalHitting.TMTime.StackToOne.stWrite_length {K : Type v_1} {Γ : K → Type v_2} {σ : Type v_4} {k : K} (o : Turing.TM2to1.StAct K Γ σ k) (v : σ) (l : List (Γ k)) : (Turing.TM2to1.stWrite v l o).length ≤ l.length + 1

theorem Complexity.RationalHitting.TMTime.StackToOne.updated_length {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} [DecidableEq K] {k : K} (o : Turing.TM2to1.StAct K Γ σ k) (v : σ) (S : (k : K) → List (Γ k)) (L : ℕ) (hS : ∀ (k : K), (S k).length ≤ L) (j : K) : (Function.update S k (Turing.TM2to1.stWrite v (S k) o) j).length ≤ L + 1

theorem Complexity.RationalHitting.TMTime.StackToOne.continuation_time {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k)) (T : Turing.ListBlank ((k : K) → Option (Γ k))) (L : ℕ) (hT : ∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) (hS : ∀ (k : K), (S k).length ≤ L) : ∃ (u : ℕ) (b : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ), u ≤ stackWeight q * (2 * (L + stackWeight q) + 3) ∧ Turing.TM2to1.TrCfg (Turing.TM2.stepAux q v S) b ∧ exec (Turing.TM1.step (Turing.TM2to1.tr M)) u (Turing.TM1.stepAux (Turing.TM2to1.trNormal q) v (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T))) = some b

Real TM1 transition count for the compiled continuation of a TM2 statement. The multipliers count sweeps to and from actual stack tops.

theorem Complexity.RationalHitting.TMTime.StackToOne.statement_length {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k)) (L : ℕ) (hS : ∀ (k : K), (S k).length ≤ L) (k : K) : ((Turing.TM2.stepAux q v S).stk k).length ≤ L + stackWeight q

theorem Complexity.RationalHitting.TMTime.StackToOne.step_time {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) (l : Λ) (v : σ) (S : (k : K) → List (Γ k)) (a : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) (L C : ℕ) (ha : Turing.TM2to1.TrCfg { l := some l, var := v, stk := S } a) (hS : ∀ (k : K), (S k).length ≤ L) (hC : stackWeight (M l) + 1 ≤ C) : ∃ (u : ℕ) (b : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ), u ≤ C * (2 * (L + C) + 4) ∧ Turing.TM2to1.TrCfg (Turing.TM2.stepAux (M l) v S) b ∧ exec (Turing.TM1.step (Turing.TM2to1.tr M)) u a = some b

theorem Complexity.RationalHitting.TMTime.StackToOne.execution_time {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) [Inhabited Λ] (F : Finset Λ) (hF : Turing.TM2.Supports M F) (C : ℕ) (hC : ∀ l ∈ F, stackWeight (M l) + 1 ≤ C) (t : ℕ) (a b : Turing.TM2.Cfg Γ Λ σ) (a' : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) (L : ℕ) (ha : a.l ∈ Finset.insertNone F) (hS : ∀ (k : K), (a.stk k).length ≤ L) (htr : Turing.TM2to1.TrCfg a a') (hr : exec (Turing.TM2.step M) t a = some b) : ∃ (u : ℕ) (b' : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ), u ≤ C * t * (2 * (L + C * t) + 4) ∧ Turing.TM2to1.TrCfg b b' ∧ exec (Turing.TM1.step (Turing.TM2to1.tr M)) u a' = some b'

A bounded TM2 run on stacks of initial length <=L is simulated by Mathlib's single tape TM1 interpreter in at most Ct(2*(L+C*t)+4) macro-transitions. C is a fixed syntactic maximum over the finite program, not input advice.

theorem Complexity.RationalHitting.TMTime.StackToOne.halts {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) (a : Turing.TM2.Cfg Γ Λ σ) (a' : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) (htr : Turing.TM2to1.TrCfg a a') (ha : Turing.TM2.step M a = none) : Turing.TM1.step (Turing.TM2to1.tr M) a' = none

noncomputable def Complexity.RationalHitting.TMTime.FiniteStates.stateEncode {Λ : Type u_2} [Inhabited Λ] [DecidableEq Λ] (S : Finset Λ) (q : Λ) : Fin (Fintype.card ↥S + 1)

Number the supported states, reserving zero for the default state.

Equations

• Complexity.RationalHitting.TMTime.FiniteStates.stateEncode S q = if q = default then 0 else if h : q ∈ S then ((Fintype.equivFin ↥S) ⟨q, h⟩).succ else 0

noncomputable def Complexity.RationalHitting.TMTime.FiniteStates.stateDecode {Λ : Type u_2} [Inhabited Λ] (S : Finset Λ) : Fin (Fintype.card ↥S + 1) → Λ

Decode a numbered state, with zero denoting the default state.

Equations

• Complexity.RationalHitting.TMTime.FiniteStates.stateDecode S i = Fin.cases default (fun (i : Fin (Fintype.card ↥S)) => ↑((Fintype.equivFin ↥S).symm i)) i

@[simp]

theorem Complexity.RationalHitting.TMTime.FiniteStates.stateEncode_default {Λ : Type u_2} [Inhabited Λ] [DecidableEq Λ] (S : Finset Λ) : stateEncode S default = 0

theorem Complexity.RationalHitting.TMTime.FiniteStates.stateDecode_encode {Λ : Type u_2} [Inhabited Λ] [DecidableEq Λ] (S : Finset Λ) (q : Λ) (hq : q ∈ S) : stateDecode S (stateEncode S q) = q

noncomputable def Complexity.RationalHitting.TMTime.FiniteStates.machine {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) : Turing.TM0.Machine Γ (Fin (Fintype.card ↥S + 1))

Restrict a supported machine to an explicitly finite numbered state space.

Equations

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

noncomputable def Complexity.RationalHitting.TMTime.FiniteStates.cfg {Γ : Type u_1} {Λ : Type u_2} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (S : Finset Λ) (a : Turing.TM0.Cfg Γ Λ) : Turing.TM0.Cfg Γ (Fin (Fintype.card ↥S + 1))

Map a supported configuration to its numbered state representation.

Equations

• Complexity.RationalHitting.TMTime.FiniteStates.cfg S a = { q := Complexity.RationalHitting.TMTime.FiniteStates.stateEncode S a.q, Tape := a.Tape }

theorem Complexity.RationalHitting.TMTime.FiniteStates.step_cfg {Γ : Type u_1} {Λ : Type u_2} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (a : Turing.TM0.Cfg Γ Λ) (ha : a.q ∈ S) : Turing.TM0.step (machine M S) (cfg S a) = Option.map (cfg S) (Turing.TM0.step M a)

@[simp]

theorem Complexity.RationalHitting.TMTime.FiniteStates.cfg_init {Γ : Type u_1} {Λ : Type u_2} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (S : Finset Λ) (l : List Γ) : cfg S (Turing.TM0.init l) = Turing.TM0.init l

theorem Complexity.RationalHitting.TMTime.FiniteStates.execution {Γ : Type u_1} {Λ : Type u_2} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hs : Turing.TM0.Supports M ↑S) (t : ℕ) (a b : Turing.TM0.Cfg Γ Λ) (ha : a.q ∈ S) (hr : exec (Turing.TM0.step M) t a = some b) : exec (Turing.TM0.step (machine M S)) t (cfg S a) = some (cfg S b)

theorem Complexity.RationalHitting.TMTime.FiniteStates.run_support {Γ : Type v_1} {Λ : Type v_2} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hs : Turing.TM0.Supports M ↑S) (t : ℕ) (a b : Turing.TM0.Cfg Γ Λ) (ha : a.q ∈ S) (hr : exec (Turing.TM0.step M) t a = some b) : b.q ∈ S

theorem Complexity.RationalHitting.TMTime.FiniteStates.finite_machine {Γ : Type u_1} {Λ : Type u_2} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hs : Turing.TM0.Supports M ↑S) : ∃ (m : ℕ) (G : Turing.TM0.Machine Γ (Fin (m + 1))), ∀ (l : List Γ) (t : ℕ) (a : Turing.TM0.Cfg Γ Λ), exec (Turing.TM0.step M) t (Turing.TM0.init l) = some a → Turing.TM0.step M a = none → ∃ (b : Turing.TM0.Cfg Γ (Fin (m + 1))), exec (Turing.TM0.step G) t (Turing.TM0.init l) = some b ∧ Turing.TM0.step G b = none ∧ b.Tape = a.Tape

Finite-support compression has no transition or tape overhead.