Polynomial-time simulation of one Mathlib TM2 step

The simulator operates on Mathlib's configurations themselves. Finite functions in a source statement are finite case analyses; stack operations reuse the certified list and table calculus. Halting configurations remain fixed, so a clock may safely run beyond the source's halting time.

Main definitions

• Turing.TM2.stepTotal: a TM2 step that stays put after halting.
• Turing.TM2.pushBound: a syntactic upper bound on pushes along a statement path.

Main results

• Turing.TM2.cfg_label, Turing.TM2.cfg_var, Turing.TM2.cfg_stacks and Turing.TM2.cfg_mk: polynomial-time configuration projections and construction.
• Turing.TM2.stepAux_polyTime: executing one fixed statement is polynomial-time.
• Turing.TM2.stepTotal_polyTime: one fixed source transition is polynomial-time in the complete encoded configuration.
• Turing.TM2.stepTotal_stack_bound: a fixed source transition adds at most a constant number of symbols to any stack.

References

The statement semantics is Turing.TM2.stepAux in Mathlib.Computability.TuringMachine.StackTuringMachine.

theorem Turing.TM2.cfg_label {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] : MultiTapeTM.ComputableTidilyInPolyTime Cfg.l encCfg (MultiTapeTM.encFinite (Option Λ))

Reading the source label is efficient.

theorem Turing.TM2.cfg_var {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] : MultiTapeTM.ComputableTidilyInPolyTime Cfg.var encCfg (MultiTapeTM.encFinite σ)

Reading the finite register state is efficient.

theorem Turing.TM2.cfg_stacks {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] : MultiTapeTM.ComputableTidilyInPolyTime Cfg.stk encCfg (MultiTapeTM.encDPi fun (k : K) => MultiTapeTM.encList (MultiTapeTM.encFinite (Γ k)))

Reading the complete stack family is efficient.

theorem Turing.TM2.cfg_mk {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] {α : Type} {input : α ↪ List Bool} {label : α → Option Λ} {state : α → σ} {store : α → (k : K) → List (Γ k)} (hl : MultiTapeTM.ComputableTidilyInPolyTime label input (MultiTapeTM.encFinite (Option Λ))) (hv : MultiTapeTM.ComputableTidilyInPolyTime state input (MultiTapeTM.encFinite σ)) (hs : MultiTapeTM.ComputableTidilyInPolyTime store input (MultiTapeTM.encDPi fun (k : K) => MultiTapeTM.encList (MultiTapeTM.encFinite (Γ k)))) : MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => { l := label a, var := state a, stk := store a }) input encCfg

Construct a configuration while charging all retained storage.

theorem Turing.TM2.stepAux_polyTime {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] [DecidableEq K] (q : Stmt Γ Λ σ) : MultiTapeTM.ComputableTidilyInPolyTime (fun (cfg : Cfg Γ Λ σ) => stepAux q cfg.var cfg.stk) encCfg encCfg

Executing a fixed statement is efficient, including its straight-line continuations.

def Turing.TM2.stepTotal {K : Type} {Γ : K → Type} {Λ σ : Type} [DecidableEq K] (M : Λ → Stmt Γ Λ σ) (cfg : Cfg Γ Λ σ) : Cfg Γ Λ σ

Execute one source step, keeping the last configuration after halting.

theorem Turing.TM2.stepTotal_polyTime {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] [DecidableEq K] (M : Λ → Stmt Γ Λ σ) : MultiTapeTM.ComputableTidilyInPolyTime (stepTotal M) encCfg encCfg

The finite label chooses a fixed certified statement.

def Turing.TM2.pushBound {K : Type} {Γ : K → Type} {Λ σ : Type} : Stmt Γ Λ σ → ℕ

A syntactic bound on the number of pushes along any path through a statement.

theorem Turing.TM2.stepAux_stack_bound {K : Type} {Γ : K → Type} {Λ σ : Type} [DecidableEq K] (q : Stmt Γ Λ σ) (v : σ) (store : (k : K) → List (Γ k)) (bound : ℕ) (h : ∀ (k : K), (store k).length ≤ bound) (k : K) : ((stepAux q v store).stk k).length ≤ bound + pushBound q

Only pushes can increase stack lengths.

theorem Turing.TM2.stepTotal_stack_bound {K : Type} {Γ : K → Type} {Λ σ : Type} [Finite Λ] [DecidableEq K] (M : Λ → Stmt Γ Λ σ) : ∃ (C : ℕ), ∀ (cfg : Cfg Γ Λ σ) (bound : ℕ), (∀ (k : K), (cfg.stk k).length ≤ bound) → ∀ (k : K), ((stepTotal M cfg).stk k).length ≤ bound + C

A fixed finite program has a uniform per-transition stack-growth constant.