Turing machines

The files PostTuringMachine.lean and TuringMachine.lean define a sequence of simple machine languages, starting with Turing machines and working up to more complex languages based on Wang B-machines.

PostTuringMachine.lean covers the TM0 model and TM1 model; TuringMachine.lean adds the TM2 model.

Naming conventions

Each model of computation in this file shares a naming convention for the elements of a model of computation. These are the parameters for the language:

• Γ is the alphabet on the tape.
• Λ is the set of labels, or internal machine states.
• σ is the type of internal memory, not on the tape. This does not exist in the TM0 model, and later models achieve this by mixing it into Λ.
• K is used in the TM2 model, which has multiple stacks, and denotes the number of such stacks.

All of these variables denote "essentially finite" types, but for technical reasons it is convenient to allow them to be infinite anyway. When using an infinite type, we will be interested to prove that only finitely many values of the type are ever interacted with.

Given these parameters, there are a few common structures for the model that arise:

• Stmt is the set of all actions that can be performed in one step. For the TM0 model this set is finite, and for later models it is an infinite inductive type representing "possible program texts".
• Cfg is the set of instantaneous configurations, that is, the state of the machine together with its environment.
• Machine is the set of all machines in the model. Usually this is approximately a function Λ → Stmt, although different models have different ways of halting and other actions.
• step : Cfg → Option Cfg is the function that describes how the state evolves over one step. If step c = none, then c is a terminal state, and the result of the computation is read off from c. Because of the type of step, these models are all deterministic by construction.
• init : Input → Cfg sets up the initial state. The type Input depends on the model; in most cases it is List Γ.
• eval : Machine → Input → Part Output, given a machine M and input i, starts from init i, runs step until it reaches an output, and then applies a function Cfg → Output to the final state to obtain the result. The type Output depends on the model.
• Supports : Machine → Finset Λ → Prop asserts that a machine M starts in S : Finset Λ, and can only ever jump to other states inside S. This implies that the behavior of M on any input cannot depend on its values outside S. We use this to allow Λ to be an infinite set when convenient, and prove that only finitely many of these states are actually accessible. This formalizes "essentially finite" mentioned above.

The TM2 model

The TM2 model removes the tape entirely from the TM1 model, replacing it with an arbitrary (finite) collection of stacks, each with elements of different types (the alphabet of stack k : K is Γ k). The statements are:

• push k (f : σ → Γ k) q puts f a on the k-th stack, then does q.
• pop k (f : σ → Option (Γ k) → σ) q changes the state to f a (S k).head, where S k is the value of the k-th stack, and removes this element from the stack, then does q.
• peek k (f : σ → Option (Γ k) → σ) q changes the state to f a (S k).head, where S k is the value of the k-th stack, then does q.
• load (f : σ → σ) q reads nothing but applies f to the internal state, then does q.
• branch (f : σ → Bool) qtrue qfalse does qtrue or qfalse according to f a.
• goto (f : σ → Λ) jumps to label f a.
• halt halts on the next step.

The configuration is a tuple (l, var, stk) where l : Option Λ is the current label to run or none for the halting state, var : σ is the (finite) internal state, and stk : ∀ k, List (Γ k) is the collection of stacks. (Note that unlike the TM0 and TM1 models, these are not ListBlanks, they have definite ends that can be detected by the pop command.)

Given a designated stack k and a value L : List (Γ k), the initial configuration has all the stacks empty except the designated "input" stack; in eval this designated stack also functions as the output stack.

inductive Turing.TM2.Stmt {K : Type u_1} (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

The TM2 model removes the tape entirely from the TM1 model, replacing it with an arbitrary (finite) collection of stacks. The operation push puts an element on one of the stacks, and pop removes an element from a stack (and modifying the internal state based on the result). peek modifies the internal state but does not remove an element.

• push {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) : (σ → Γ k) → Stmt Γ Λ σ → Stmt Γ Λ σ
• peek {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) : (σ → Option (Γ k) → σ) → Stmt Γ Λ σ → Stmt Γ Λ σ
• pop {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) : (σ → Option (Γ k) → σ) → Stmt Γ Λ σ → Stmt Γ Λ σ
• load {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : (σ → σ) → Stmt Γ Λ σ → Stmt Γ Λ σ
• branch {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : (σ → Bool) → Stmt Γ Λ σ → Stmt Γ Λ σ → Stmt Γ Λ σ
• goto {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : (σ → Λ) → Stmt Γ Λ σ
• halt {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : Stmt Γ Λ σ

instance Turing.TM2.Stmt.inhabited {K : Type u_1} (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) : Inhabited (Stmt Γ Λ σ)

Equations

• Turing.TM2.Stmt.inhabited Γ Λ σ = { default := Turing.TM2.Stmt.halt }

structure Turing.TM2.Cfg {K : Type u_1} (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A configuration in the TM2 model is a label (or none for the halt state), the state of local variables, and the stacks. (Note that the stacks are not ListBlanks, they have a definite size.)

• l : Option Λ

  The current label to run (or none for the halting state)

• var : σ

  The internal state

• stk (k : K) : List (Γ k)

  The (finite) collection of internal stacks

instance Turing.TM2.Cfg.inhabited {K : Type u_1} (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) [Inhabited σ] : Inhabited (Cfg Γ Λ σ)

Equations

• Turing.TM2.Cfg.inhabited Γ Λ σ = { default := { l := default, var := default, stk := default } }

def Turing.TM2.stepAux {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] : Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Cfg Γ Λ σ

The step function for the TM2 model.

Equations

• Turing.TM2.stepAux (Turing.TM2.Stmt.push k f q) x✝¹ x✝ = Turing.TM2.stepAux q x✝¹ (Function.update x✝ k (f x✝¹ :: x✝ k))
• Turing.TM2.stepAux (Turing.TM2.Stmt.peek k f q) x✝¹ x✝ = Turing.TM2.stepAux q (f x✝¹ (x✝ k).head?) x✝
• Turing.TM2.stepAux (Turing.TM2.Stmt.pop k f q) x✝¹ x✝ = Turing.TM2.stepAux q (f x✝¹ (x✝ k).head?) (Function.update x✝ k (x✝ k).tail)
• Turing.TM2.stepAux (Turing.TM2.Stmt.load a q) x✝¹ x✝ = Turing.TM2.stepAux q (a x✝¹) x✝
• Turing.TM2.stepAux (Turing.TM2.Stmt.branch f q₁ q₂) x✝¹ x✝ = bif f x✝¹ then Turing.TM2.stepAux q₁ x✝¹ x✝ else Turing.TM2.stepAux q₂ x✝¹ x✝
• Turing.TM2.stepAux (Turing.TM2.Stmt.goto f) x✝¹ x✝ = { l := some (f x✝¹), var := x✝¹, stk := x✝ }
• Turing.TM2.stepAux Turing.TM2.Stmt.halt x✝¹ x✝ = { l := none, var := x✝¹, stk := x✝ }

def Turing.TM2.step {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Stmt Γ Λ σ) : Cfg Γ Λ σ → Option (Cfg Γ Λ σ)

The step function for the TM2 model.

Equations

• Turing.TM2.step M { l := none, var := var, stk := stk } = none
• Turing.TM2.step M { l := some l, var := v, stk := S } = some (Turing.TM2.stepAux (M l) v S)

def Turing.TM2.Reaches {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Stmt Γ Λ σ) : Cfg Γ Λ σ → Cfg Γ Λ σ → Prop

The (reflexive) reachability relation for the TM2 model.

Equations

• Turing.TM2.Reaches M = Relation.ReflTransGen fun (a b : Turing.TM2.Cfg Γ Λ σ) => b ∈ Turing.TM2.step M a

def Turing.TM2.SupportsStmt {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) : Stmt Γ Λ σ → Prop

Given a set S of states, SupportsStmt S q means that q only jumps to states in S.

Equations

• Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.push k a q) = Turing.TM2.SupportsStmt S q
• Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.peek k a q) = Turing.TM2.SupportsStmt S q
• Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.pop k a q) = Turing.TM2.SupportsStmt S q
• Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.load a q) = Turing.TM2.SupportsStmt S q
• Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.branch a q₁ q₂) = (Turing.TM2.SupportsStmt S q₁ ∧ Turing.TM2.SupportsStmt S q₂)
• Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.goto l) = ∀ (v : σ), l v ∈ S
• Turing.TM2.SupportsStmt S Turing.TM2.Stmt.halt = True

noncomputable def Turing.TM2.stmts₁ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : Stmt Γ Λ σ → Finset (Stmt Γ Λ σ)

The set of subtree statements in a statement.

Equations

• Turing.TM2.stmts₁ (Turing.TM2.Stmt.push k a q) = insert (Turing.TM2.Stmt.push k a q) (Turing.TM2.stmts₁ q)
• Turing.TM2.stmts₁ (Turing.TM2.Stmt.peek k a q) = insert (Turing.TM2.Stmt.peek k a q) (Turing.TM2.stmts₁ q)
• Turing.TM2.stmts₁ (Turing.TM2.Stmt.pop k a q) = insert (Turing.TM2.Stmt.pop k a q) (Turing.TM2.stmts₁ q)
• Turing.TM2.stmts₁ (Turing.TM2.Stmt.load a q) = insert (Turing.TM2.Stmt.load a q) (Turing.TM2.stmts₁ q)
• Turing.TM2.stmts₁ (Turing.TM2.Stmt.branch a q₁ q₂) = insert (Turing.TM2.Stmt.branch a q₁ q₂) (Turing.TM2.stmts₁ q₁ ∪ Turing.TM2.stmts₁ q₂)
• Turing.TM2.stmts₁ (Turing.TM2.Stmt.goto a) = {Turing.TM2.Stmt.goto a}
• Turing.TM2.stmts₁ Turing.TM2.Stmt.halt = {Turing.TM2.Stmt.halt}

theorem Turing.TM2.stmts₁_self {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q : Stmt Γ Λ σ} : q ∈ stmts₁ q

theorem Turing.TM2.stmts₁_trans {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q₁ q₂ : Stmt Γ Λ σ} : q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂

theorem Turing.TM2.stmts₁_supportsStmt_mono {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂) : SupportsStmt S q₁

noncomputable def Turing.TM2.stmts {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (M : Λ → Stmt Γ Λ σ) (S : Finset Λ) : Finset (Option (Stmt Γ Λ σ))

The set of statements accessible from initial set S of labels.

Equations

• Turing.TM2.stmts M S = Finset.insertNone (S.biUnion fun (q : Λ) => Turing.TM2.stmts₁ (M q))

theorem Turing.TM2.stmts_trans {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h₁ : q₁ ∈ stmts₁ q₂) : some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

def Turing.TM2.Supports {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [Inhabited Λ] (M : Λ → Stmt Γ Λ σ) (S : Finset Λ) : Prop

Given a TM2 machine M and a set S of states, Supports M S means that all states in S jump only to other states in S.

Equations

• Turing.TM2.Supports M S = (default ∈ S ∧ ∀ q ∈ S, Turing.TM2.SupportsStmt S (M q))

theorem Turing.TM2.stmts_supportsStmt {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [Inhabited Λ] {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q : Stmt Γ Λ σ} (ss : Supports M S) : some q ∈ stmts M S → SupportsStmt S q

theorem Turing.TM2.step_supports {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [Inhabited Λ] [DecidableEq K] (M : Λ → Stmt Γ Λ σ) {S : Finset Λ} (ss : Supports M S) {c c' : Cfg Γ Λ σ} : c' ∈ step M c → c.l ∈ Finset.insertNone S → c'.l ∈ Finset.insertNone S

def Turing.TM2.init {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [Inhabited Λ] [DecidableEq K] [Inhabited σ] (k : K) (L : List (Γ k)) : Cfg Γ Λ σ

The initial state of the TM2 model. The input is provided on a designated stack.

Equations

• Turing.TM2.init k L = { l := some default, var := default, stk := Function.update (fun (x : K) => []) k L }

def Turing.TM2.eval {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [Inhabited Λ] [DecidableEq K] [Inhabited σ] (M : Λ → Stmt Γ Λ σ) (k : K) (L : List (Γ k)) : Part (List (Γ k))

Evaluates a TM2 program to completion, with the output on the same stack as the input.

Equations

• Turing.TM2.eval M k L = Part.map (fun (c : Turing.TM2.Cfg Γ Λ σ) => c.stk k) (Turing.eval (Turing.TM2.step M) (Turing.TM2.init k L))

TM2 emulator in TM1

To prove that TM2 computable functions are TM1 computable, we need to reduce each TM2 program to a TM1 program. So suppose a TM2 program is given. This program has to maintain a whole collection of stacks, but we have only one tape, so we must "multiplex" them all together. Pictorially, if stack 1 contains [a, b] and stack 2 contains [c, d, e, f] then the tape looks like this:

 bottom:  ... | _ | T | _ | _ | _ | _ | ...
 stack 1: ... | _ | b | a | _ | _ | _ | ...
 stack 2: ... | _ | f | e | d | c | _ | ...

where a tape element is a vertical slice through the diagram. Here the alphabet is Γ' := Bool × ∀ k, Option (Γ k), where:

• bottom : Bool is marked only in one place, the initial position of the TM, and represents the tail of all stacks. It is never modified.
• stk k : Option (Γ k) is the value of the k-th stack, if in range, otherwise none (which is the blank value). Note that the head of the stack is at the far end; this is so that push and pop don't have to do any shifting.

In "resting" position, the TM is sitting at the position marked bottom. For non-stack actions, it operates in place, but for the stack actions push, peek, and pop, it must shuttle to the end of the appropriate stack, make its changes, and then return to the bottom. So the states are:

• normal (l : Λ): waiting at bottom to execute function l
• go k (s : StAct k) (q : Stmt₂): travelling to the right to get to the end of stack k in order to perform stack action s, and later continue with executing q
• ret (q : Stmt₂): travelling to the left after having performed a stack action, and executing q once we arrive

Because of the shuttling, emulation overhead is O(n), where n is the current maximum of the length of all stacks. Therefore a program that takes k steps to run in TM2 takes O((m+k)k) steps to run when emulated in TM1, where m is the length of the input.

theorem Turing.TM2to1.stk_nth_val {K : Type u_1} {Γ : K → Type u_2} {L : ListBlank ((k : K) → Option (Γ k))} {k : K} {S : List (Γ k)} (n : ℕ) (hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse) : L.nth n k = S.reverse[n]?

def Turing.TM2to1.Γ' (K : Type u_1) (Γ : K → Type u_2) : Type (max u_1 u_2)

The alphabet of the TM2 simulator on TM1 is a marker for the stack bottom, plus a vector of stack elements for each stack, or none if the stack does not extend this far.

Equations

• Turing.TM2to1.Γ' K Γ = (Bool × ((k : K) → Option (Γ k)))

instance Turing.TM2to1.Γ'.inhabited {K : Type u_1} {Γ : K → Type u_2} : Inhabited (Γ' K Γ)

Equations

• Turing.TM2to1.Γ'.inhabited = { default := (false, fun (x : K) => none) }

instance Turing.TM2to1.Γ'.fintype {K : Type u_1} {Γ : K → Type u_2} [DecidableEq K] [Fintype K] [(k : K) → Fintype (Γ k)] : Fintype (Γ' K Γ)

Equations

• Turing.TM2to1.Γ'.fintype = instFintypeProd Bool ((k : K) → Option (Γ k))

def Turing.TM2to1.addBottom {K : Type u_1} {Γ : K → Type u_2} (L : ListBlank ((k : K) → Option (Γ k))) : ListBlank (Γ' K Γ)

The bottom marker is fixed throughout the calculation, so we use the addBottom function to express the program state in terms of a tape with only the stacks themselves.

Equations

• Turing.TM2to1.addBottom L = Turing.ListBlank.cons (true, L.head) (Turing.ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)

theorem Turing.TM2to1.addBottom_map {K : Type u_1} {Γ : K → Type u_2} (L : ListBlank ((k : K) → Option (Γ k))) : ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (addBottom L) = L

theorem Turing.TM2to1.addBottom_modifyNth {K : Type u_1} {Γ : K → Type u_2} (f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)) (L : ListBlank ((k : K) → Option (Γ k))) (n : ℕ) : ListBlank.modifyNth (fun (a : Bool × ((k : K) → Option (Γ k))) => (a.1, f a.2)) n (addBottom L) = addBottom (ListBlank.modifyNth f n L)

theorem Turing.TM2to1.addBottom_nth_snd {K : Type u_1} {Γ : K → Type u_2} (L : ListBlank ((k : K) → Option (Γ k))) (n : ℕ) : ((addBottom L).nth n).2 = L.nth n

theorem Turing.TM2to1.addBottom_nth_succ_fst {K : Type u_1} {Γ : K → Type u_2} (L : ListBlank ((k : K) → Option (Γ k))) (n : ℕ) : ((addBottom L).nth (n + 1)).1 = false

theorem Turing.TM2to1.addBottom_head_fst {K : Type u_1} {Γ : K → Type u_2} (L : ListBlank ((k : K) → Option (Γ k))) : (addBottom L).head.1 = true

inductive Turing.TM2to1.StAct (K : Type u_1) (Γ : K → Type u_2) (σ : Type u_4) (k : K) : Type (max u_2 u_4)

A stack action is a command that interacts with the top of a stack. Our default position is at the bottom of all the stacks, so we have to hold on to this action while going to the end to modify the stack.

• push {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} : (σ → Γ k) → StAct K Γ σ k
• peek {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} : (σ → Option (Γ k) → σ) → StAct K Γ σ k
• pop {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} : (σ → Option (Γ k) → σ) → StAct K Γ σ k

instance Turing.TM2to1.StAct.inhabited {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} : Inhabited (StAct K Γ σ k)

Equations

• Turing.TM2to1.StAct.inhabited = { default := Turing.TM2to1.StAct.peek fun (s : σ) (x : Option (Γ k)) => s }

def Turing.TM2to1.stRun {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} : StAct K Γ σ k → TM2.Stmt Γ Λ σ → TM2.Stmt Γ Λ σ

The TM2 statement corresponding to a stack action.

Equations

• Turing.TM2to1.stRun (Turing.TM2to1.StAct.push f) = Turing.TM2.Stmt.push k f
• Turing.TM2to1.stRun (Turing.TM2to1.StAct.peek f) = Turing.TM2.Stmt.peek k f
• Turing.TM2to1.stRun (Turing.TM2to1.StAct.pop f) = Turing.TM2.Stmt.pop k f

def Turing.TM2to1.stVar {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) : StAct K Γ σ k → σ

The effect of a stack action on the local variables, given the value of the stack.

Equations

• Turing.TM2to1.stVar v l (Turing.TM2to1.StAct.push f) = v
• Turing.TM2to1.stVar v l (Turing.TM2to1.StAct.peek f) = f v l.head?
• Turing.TM2to1.stVar v l (Turing.TM2to1.StAct.pop f) = f v l.head?

def Turing.TM2to1.stWrite {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) : StAct K Γ σ k → List (Γ k)

The effect of a stack action on the stack.

Equations

• Turing.TM2to1.stWrite v l (Turing.TM2to1.StAct.push f) = f v :: l
• Turing.TM2to1.stWrite v l (Turing.TM2to1.StAct.peek f) = l
• Turing.TM2to1.stWrite v l (Turing.TM2to1.StAct.pop f) = l.tail

def Turing.TM2to1.stmtStRec {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {C : TM2.Stmt Γ Λ σ → Sort l} (H₁ : (k : K) → (s : StAct K Γ σ k) → (q : TM2.Stmt Γ Λ σ) → C q → C (stRun s q)) (H₂ : (a : σ → σ) → (q : TM2.Stmt Γ Λ σ) → C q → C (TM2.Stmt.load a q)) (H₃ : (p : σ → Bool) → (q₁ q₂ : TM2.Stmt Γ Λ σ) → C q₁ → C q₂ → C (TM2.Stmt.branch p q₁ q₂)) (H₄ : (l : σ → Λ) → C (TM2.Stmt.goto l)) (H₅ : C TM2.Stmt.halt) (n : TM2.Stmt Γ Λ σ) : C n

We have partitioned the TM2 statements into "stack actions", which require going to the end of the stack, and all other actions, which do not. This is a modified recursor which lumps the stack actions into one.

Equations

• Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ (Turing.TM2.Stmt.push k a q) = H₁ k (Turing.TM2to1.StAct.push a) q (Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ q)
• Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ (Turing.TM2.Stmt.peek k a q) = H₁ k (Turing.TM2to1.StAct.peek a) q (Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ q)
• Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ (Turing.TM2.Stmt.pop k a q) = H₁ k (Turing.TM2to1.StAct.pop a) q (Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ q)
• Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ (Turing.TM2.Stmt.load a q) = H₂ a q (Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ q)
• Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ (Turing.TM2.Stmt.branch a q₁ q₂) = H₃ a q₁ q₂ (Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ q₁) (Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ q₂)
• Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ (Turing.TM2.Stmt.goto l) = H₄ l
• Turing.TM2to1.stmtStRec H₁ H₂ H₃ H₄ H₅ Turing.TM2.Stmt.halt = H₅

theorem Turing.TM2to1.supports_run {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) {k : K} (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ) : TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q

inductive Turing.TM2to1.Λ' (K : Type u_1) (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

The machine states of the TM2 emulator. We can either be in a normal state when waiting for the next TM2 action, or we can be in the "go" and "return" states to go to the top of the stack and return to the bottom, respectively.

• normal {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : Λ → Λ' K Γ Λ σ
• go {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) : StAct K Γ σ k → TM2.Stmt Γ Λ σ → Λ' K Γ Λ σ
• ret {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : TM2.Stmt Γ Λ σ → Λ' K Γ Λ σ

instance Turing.TM2to1.Λ'.inhabited {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [Inhabited Λ] : Inhabited (Λ' K Γ Λ σ)

Equations

• Turing.TM2to1.Λ'.inhabited = { default := Turing.TM2to1.Λ'.normal default }

def Turing.TM2to1.trStAct {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] {k : K} (q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ) : StAct K Γ σ k → TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ

The program corresponding to state transitions at the end of a stack. Here we start out just after the top of the stack, and should end just after the new top of the stack.

Equations

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

def Turing.TM2to1.trInit {K : Type u_1} {Γ : K → Type u_2} [DecidableEq K] (k : K) (L : List (Γ k)) : List (Γ' K Γ)

The initial state for the TM2 emulator, given an initial TM2 state. All stacks start out empty except for the input stack, and the stack bottom mark is set at the head.

Equations

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

theorem Turing.TM2to1.step_run {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] {k : K} (q : TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k)) (s : StAct K Γ σ k) : TM2.stepAux (stRun s q) v S = TM2.stepAux q (stVar v (S k) s) (Function.update S k (stWrite v (S k) s))

def Turing.TM2to1.trNormal {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : TM2.Stmt Γ Λ σ → TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ

The translation of TM2 statements to TM1 statements. regular actions have direct equivalents, but stack actions are deferred by going to the corresponding go state, so that we can find the appropriate stack top.

Equations

• Turing.TM2to1.trNormal (Turing.TM2.Stmt.push k a q) = Turing.TM1.Stmt.goto fun (x : Turing.TM2to1.Γ' K Γ) (x : σ) => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.push a) q
• Turing.TM2to1.trNormal (Turing.TM2.Stmt.peek k a q) = Turing.TM1.Stmt.goto fun (x : Turing.TM2to1.Γ' K Γ) (x : σ) => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.peek a) q
• Turing.TM2to1.trNormal (Turing.TM2.Stmt.pop k a q) = Turing.TM1.Stmt.goto fun (x : Turing.TM2to1.Γ' K Γ) (x : σ) => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.pop a) q
• Turing.TM2to1.trNormal (Turing.TM2.Stmt.load a q) = Turing.TM1.Stmt.load (fun (x : Turing.TM2to1.Γ' K Γ) => a) (Turing.TM2to1.trNormal q)
• Turing.TM2to1.trNormal (Turing.TM2.Stmt.branch a q₁ q₂) = Turing.TM1.Stmt.branch (fun (x : Turing.TM2to1.Γ' K Γ) => a) (Turing.TM2to1.trNormal q₁) (Turing.TM2to1.trNormal q₂)
• Turing.TM2to1.trNormal (Turing.TM2.Stmt.goto l) = Turing.TM1.Stmt.goto fun (x : Turing.TM2to1.Γ' K Γ) (s : σ) => Turing.TM2to1.Λ'.normal (l s)
• Turing.TM2to1.trNormal Turing.TM2.Stmt.halt = Turing.TM1.Stmt.halt

theorem Turing.TM2to1.trNormal_run {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ) : trNormal (stRun s q) = TM1.Stmt.goto fun (x : Γ' K Γ) (x : σ) => Λ'.go k s q

noncomputable def Turing.TM2to1.trStmts₁ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : TM2.Stmt Γ Λ σ → Finset (Λ' K Γ Λ σ)

The set of machine states accessible from an initial TM2 statement.

Equations

• Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.push k f q) = {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.push f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
• Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.peek k f q) = {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.peek f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
• Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.pop k f q) = {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.pop f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
• Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.load a q) = Turing.TM2to1.trStmts₁ q
• Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.branch a q₁ q₂) = Turing.TM2to1.trStmts₁ q₁ ∪ Turing.TM2to1.trStmts₁ q₂
• Turing.TM2to1.trStmts₁ x✝ = ∅

theorem Turing.TM2to1.trStmts₁_run {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} {s : StAct K Γ σ k} {q : TM2.Stmt Γ Λ σ} : trStmts₁ (stRun s q) = {Λ'.go k s q, Λ'.ret q} ∪ trStmts₁ q

theorem Turing.TM2to1.tr_respects_aux₂ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] {k : K} {q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ} {v : σ} {S : (k : K) → List (Γ k)} {L : ListBlank ((k : K) → Option (Γ k))} (hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) (o : StAct K Γ σ k) : let v' := stVar v (S k) o; let Sk' := stWrite v (S k) o; let S' := Function.update S k Sk'; ∃ (L' : ListBlank ((k : K) → Option (Γ k))), (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S' k)).reverse) ∧ TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) = TM1.stepAux q v' ((Tape.move Dir.right)^[(S' k).length] (Tape.mk' ∅ (addBottom L')))

def Turing.TM2to1.tr {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → TM2.Stmt Γ Λ σ) : Λ' K Γ Λ σ → TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ

The TM2 emulator machine states written as a TM1 program. This handles the go and ret states, which shuttle to and from a stack top.

Equations

• One or more equations did not get rendered due to their size.
• Turing.TM2to1.tr M (Turing.TM2to1.Λ'.normal q) = Turing.TM2to1.trNormal (M q)

inductive Turing.TM2to1.TrCfg {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} : TM2.Cfg Γ Λ σ → TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ → Prop

The relation between TM2 configurations and TM1 configurations of the TM2 emulator.

• mk {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q : Option Λ} {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))) : (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) → TrCfg { l := q, var := v, stk := S } { l := Option.map Λ'.normal q, var := v, Tape := Tape.mk' ∅ (addBottom L) }

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

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

theorem Turing.TM2to1.tr_respects_aux {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → TM2.Stmt Γ Λ σ) {q : TM2.Stmt Γ Λ σ} {v : σ} {T : ListBlank ((i : K) → Option (Γ i))} {k : K} {S : (k : K) → List (Γ k)} (hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) (o : StAct K Γ σ k) (IH : ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))}, (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) → ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ), TrCfg (TM2.stepAux q v S) b ∧ Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b) : ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ), TrCfg (TM2.stepAux (stRun o q) v S) b ∧ Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b

theorem Turing.TM2to1.tr_respects {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → TM2.Stmt Γ Λ σ) : Respects (TM2.step M) (TM1.step (tr M)) TrCfg

theorem Turing.TM2to1.trCfg_init {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] [Inhabited Λ] [Inhabited σ] (k : K) (L : List (Γ k)) : TrCfg (TM2.init k L) (TM1.init (trInit k L))

theorem Turing.TM2to1.tr_eval_dom {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → TM2.Stmt Γ Λ σ) [Inhabited Λ] [Inhabited σ] (k : K) (L : List (Γ k)) : (TM1.eval (tr M) (trInit k L)).Dom ↔ (TM2.eval M k L).Dom

theorem Turing.TM2to1.tr_eval {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → TM2.Stmt Γ Λ σ) [Inhabited Λ] [Inhabited σ] (k : K) (L : List (Γ k)) {L₁ : ListBlank (Γ' K Γ)} {L₂ : List (Γ k)} (H₁ : L₁ ∈ TM1.eval (tr M) (trInit k L)) (H₂ : L₂ ∈ TM2.eval M k L) : ∃ (S : (k : K) → List (Γ k)) (L' : ListBlank ((k : K) → Option (Γ k))), addBottom L' = L₁ ∧ (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = L₂

noncomputable def Turing.TM2to1.trSupp {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (M : Λ → TM2.Stmt Γ Λ σ) (S : Finset Λ) : Finset (Λ' K Γ Λ σ)

The support of a set of TM2 states in the TM2 emulator.

Equations

• Turing.TM2to1.trSupp M S = S.biUnion fun (l : Λ) => insert (Turing.TM2to1.Λ'.normal l) (Turing.TM2to1.trStmts₁ (M l))

theorem Turing.TM2to1.tr_supports {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → TM2.Stmt Γ Λ σ) [Inhabited Λ] {S : Finset Λ} (ss : TM2.Supports M S) : TM1.Supports (tr M) (trSupp M S)