A finite stack program for deterministic multi-tape machines

The input uses a pair of binary stacks and a flag for the left boundary. Each two-sided work tape uses two stacks over Option Bool, with its current cell in finite control. Output is accumulated in reverse order. A separate cleanup phase empties all auxiliary stacks before reversing the output and resetting the control to Mathlib's canonical haltList convention.

Main definitions

• Turing.TM2.selectList, Turing.TM2.select: finite case analysis in a TM2 statement.
• Turing.MultiTapeTM.ToTM2.machine: the finite-alphabet stack machine.
• Turing.MultiTapeTM.ToTM2.program: its running, cleanup and output-reversal phases.

References

• C. Papadimitriou, Computational Complexity, Chapter 2

def Turing.TM2.selectList {K : Type} {Γ : K → Type} {Λ State : Type} [DecidableEq State] (values : List State) (table : State → Stmt Γ Λ State) : Stmt Γ Λ State

Finite case analysis compiles an arbitrary table on finite control to a fixed statement.

theorem Turing.TM2.stepAux_selectList {K : Type} {Γ : K → Type} {Λ State : Type} [DecidableEq State] [DecidableEq K] (values : List State) (table : State → Stmt Γ Λ State) (state : State) (store : (s : K) → List (Γ s)) (h : state ∈ values) : stepAux (selectList values table) state store = stepAux (table state) state store

noncomputable def Turing.TM2.select {K : Type} {Γ : K → Type} {Λ State : Type} [Fintype State] (table : State → Stmt Γ Λ State) : Stmt Γ Λ State

A table on a finite type uses only finitely many branches.

theorem Turing.TM2.stepAux_select {K : Type} {Γ : K → Type} {Λ State : Type} [Fintype State] [DecidableEq K] (table : State → Stmt Γ Λ State) (state : State) (store : (s : K) → List (Γ s)) : stepAux (select table) state store = stepAux (table state) state store

inductive Turing.MultiTapeTM.ToTM2.Stack (k : ℕ) : Type

The four binary stacks and the two stacks for every work tape.

• input {k : ℕ} : Stack k
• before {k : ℕ} : Stack k
• output {k : ℕ} : Stack k
• reversed {k : ℕ} : Stack k
• work {k : ℕ} (tape : Fin k) (right : Bool) : Stack k

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instDecidableEqStack {k✝ : ℕ} : DecidableEq (Stack k✝)

def Turing.MultiTapeTM.ToTM2.instDecidableEqStack.decEq {k✝ : ℕ} (x✝ x✝¹ : Stack k✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instFintypeStack {k✝ : ℕ} : Fintype (Stack k✝)

@[reducible, inline]

abbrev Turing.MultiTapeTM.ToTM2.Alphabet {k : ℕ} : Stack k → Type

Work stacks store blank cells explicitly; the input and output alphabets are binary.

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instFintypeAlphabet {k : ℕ} (s : Stack k) : Fintype (Alphabet s)

inductive Turing.MultiTapeTM.ToTM2.Label : Type

The three phases have no unbounded counters in their control.

• run : Label
• clean : Label
• reverse : Label

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instDecidableEqLabel : DecidableEq Label

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instFintypeLabel : Fintype Label

structure Turing.MultiTapeTM.ToTM2.Control (k : ℕ) (State : Type) : Type

All unbounded data live on stacks. symbol and busy are scratch registers.

• state : Option State

  The source state, or none when its final action has executed.

• atLeft : Bool

  Whether the bounded input head is at the blank before the word.

• head : Fin k → Option Bool

  The current cell on each work tape.

• symbol : Option Bool

  A scratch register for input movement and output reversal.

• busy : Bool

  Whether the current cleanup round found a nonempty auxiliary stack.

theorem Turing.MultiTapeTM.ToTM2.Control.ext {k : ℕ} {State : Type} {x y : Control k State} (state : x.state = y.state) (atLeft : x.atLeft = y.atLeft) (head : x.head = y.head) (symbol : x.symbol = y.symbol) (busy : x.busy = y.busy) : x = y

theorem Turing.MultiTapeTM.ToTM2.Control.ext_iff {k : ℕ} {State : Type} {x y : Control k State} : x = y ↔ x.state = y.state ∧ x.atLeft = y.atLeft ∧ x.head = y.head ∧ x.symbol = y.symbol ∧ x.busy = y.busy

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instFintypeControl {k✝ : ℕ} {State✝ : Type} [Fintype State✝] : Fintype (Control k✝ State✝)

def Turing.MultiTapeTM.ToTM2.initialControl {k : ℕ} {State : Type} (q : State) : Control k State

Initial finite control, also restored before halting.

@[reducible, inline]

abbrev Turing.MultiTapeTM.ToTM2.Statement (k : ℕ) (State : Type) : Type

A statement over the compiler's stack alphabets, phases and finite control.

def Turing.MultiTapeTM.ToTM2.writeWork {k : ℕ} {State : Type} (i : Fin k) (write : Option (Option Bool)) (next : Statement k State) : Statement k State

Write the current work cell, retaining the old value when no write is requested.

def Turing.MultiTapeTM.ToTM2.moveWork {k : ℕ} {State : Type} (i : Fin k) (direction : SignType) (next : Statement k State) : Statement k State

Moving a work head transfers its old current cell to the opposite stack.

def Turing.MultiTapeTM.ToTM2.workAction {k : ℕ} {State : Type} (i : Fin k) (action : Option (Option Bool) × SignType) (next : Statement k State) : Statement k State

A fixed native work-tape action is a bounded straight-line stack statement.

def Turing.MultiTapeTM.ToTM2.moveInput {k : ℕ} {State : Type} (direction : SignType) (next : Statement k State) : Statement k State

Move the bounded read-only input head. Empty stacks detect the two boundaries.

def Turing.MultiTapeTM.ToTM2.action {k : ℕ} {State : Type} (a : Action k Bool State) : Statement k State

A source step updates every work tape, the input head, output and control.

def Turing.MultiTapeTM.ToTM2.auxiliaries (k : ℕ) : List (Stack k)

Stacks discarded before output reversal.

def Turing.MultiTapeTM.ToTM2.discard {k : ℕ} {State : Type} (s : Stack k) (next : Statement k State) : Statement k State

Discard one cell from each auxiliary stack and remember whether any was nonempty.

def Turing.MultiTapeTM.ToTM2.clean {k : ℕ} {State : Type} : Statement k State

A cleanup round either reduces auxiliary storage or advances to output reversal.

noncomputable def Turing.MultiTapeTM.ToTM2.program {k : ℕ} {State : Type} [Fintype State] (q₀ : State) (transition : State → Option Bool → (Fin k → Option Bool) → Action k Bool State) : Label → Statement k State

The fixed program has finite control and a finite alphabet on every stack.

@[reducible, inline]

noncomputable abbrev Turing.MultiTapeTM.ToTM2.machine {k : ℕ} {State : Type} [Fintype State] (q₀ : State) (transition : State → Option Bool → (Fin k → Option Bool) → Action k Bool State) : FinTM2

The actual Mathlib FinTM2 produced by the reverse compiler.