Turing machines
This file defines a sequence of simple machine languages, starting with Turing machines and working up to more complex languages based on Wang B-machines.
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Λ.Kis 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:
stmtis 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".cfgis the set of instantaneous configurations, that is, the state of the machine together with its environment.machineis 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 cfgis the function that describes how the state evolves over one step. Ifstep c = none, thencis a terminal state, and the result of the computation is read off fromc. Because of the type ofstep, these models are all deterministic by construction.init : input → cfgsets up the initial state. The typeinputdepends on the model; in most cases it islist Γ.eval : machine → input → roption output, given a machineMand inputi, starts frominit i, runsstepuntil it reaches an output, and then applies a functioncfg → outputto the final state to obtain the result. The typeoutputdepends on the model.supports : machine → finset Λ → Propasserts that a machineMstarts inS : finset Λ, and can only ever jump to other states insideS. This implies that the behavior ofMon any input cannot depend on its values outsideS. 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 blank_extends partial order holds of l₁ and l₂ if l₂ is obtained by adding
blanks (default Γ) to the end of l₁.
Equations
- turing.blank_extends l₁ l₂ = ∃ (n : ℕ), l₂ = l₁ ++ list.repeat (inhabited.default Γ) n
Any two extensions by blank l₁,l₂ of l have a common join (which can be taken to be the
longer of l₁ and l₂).
blank_rel is the symmetric closure of blank_extends, turning it into an equivalence
relation. Two lists are related by blank_rel if one extends the other by blanks.
Equations
- turing.blank_rel l₁ l₂ = (turing.blank_extends l₁ l₂ ∨ turing.blank_extends l₂ l₁)
Given two blank_rel lists, there exists (constructively) a common join.
Given two blank_rel lists, there exists (constructively) a common meet.
Construct a setoid instance for blank_rel.
Equations
- turing.blank_rel.setoid Γ = {r := turing.blank_rel _inst_1, iseqv := _}
A list_blank Γ is a quotient of list Γ by extension by blanks at the end. This is used to
represent half-tapes of a Turing machine, so that we can pretend that the list continues
infinitely with blanks.
Equations
Equations
Equations
A modified version of quotient.lift_on' specialized for list_blank, with the stronger
precondition blank_extends instead of blank_rel.
Equations
- l.lift_on f H = quotient.lift_on' l f _
The quotient map turning a list into a list_blank.
Equations
The head of a list_blank is well defined.
The tail of a list_blank is well defined (up to the tail of blanks).
We can cons an element onto a list_blank.
Equations
- turing.list_blank.cons a l = l.lift_on (λ (l : list Γ), turing.list_blank.mk (a :: l)) _
The cons and head/tail functions are mutually inverse, unlike in the case of list where
this only holds for nonempty lists.
The cons and head/tail functions are mutually inverse, unlike in the case of list where
this only holds for nonempty lists.
Apply a function to a value stored at the nth position of the list.
Equations
- turing.list_blank.modify_nth f (n + 1) L = turing.list_blank.cons L.head (turing.list_blank.modify_nth f n L.tail)
- turing.list_blank.modify_nth f 0 L = turing.list_blank.cons (f L.head) L.tail
- f : Γ → Γ'
- map_pt' : c.f (inhabited.default Γ) = inhabited.default Γ'
A pointed map of inhabited types is a map that sends one default value to the other.
Equations
- turing.inhabited = {default := {f := λ (_x : Γ), inhabited.default Γ', map_pt' := _}}
Equations
- turing.has_coe_to_fun = {F := λ (x : turing.pointed_map Γ Γ'), Γ → Γ', coe := turing.pointed_map.f _inst_2}
The map function on lists is well defined on list_blanks provided that the map is
pointed.
Equations
- turing.list_blank.map f l = l.lift_on (λ (l : list Γ), turing.list_blank.mk (list.map ⇑f l)) _
The i-th projection as a pointed map.
Equations
- turing.proj i = {f := λ (a : Π (i : ι), Γ i), a i, map_pt' := _}
Append a list on the left side of a list_blank.
Equations
- turing.list_blank.append (a :: l) L = turing.list_blank.cons a (turing.list_blank.append l L)
- turing.list_blank.append list.nil L = L
The bind function on lists is well defined on list_blanks provided that the default element
is sent to a sequence of default elements.
- head : Γ
- left : turing.list_blank Γ
- right : turing.list_blank Γ
The tape of a Turing machine is composed of a head element (which we imagine to be the
current position of the head), together with two list_blanks denoting the portions of the tape
going off to the left and right. When the Turing machine moves right, an element is pulled from the
right side and becomes the new head, while the head element is consed onto the left side.
Equations
- turing.tape.inhabited = {default := {head := inhabited.default Γ _inst_1, left := inhabited.default (turing.list_blank Γ) turing.list_blank.inhabited, right := inhabited.default (turing.list_blank Γ) turing.list_blank.inhabited}}
- left : turing.dir
- right : turing.dir
A direction for the turing machine move command, either
left or right.
The "inclusive" left side of the tape, including both left and head.
Equations
- T.left₀ = turing.list_blank.cons T.head T.left
The "inclusive" right side of the tape, including both right and head.
Equations
- T.right₀ = turing.list_blank.cons T.head T.right
Move the tape in response to a motion of the Turing machine. Note that T.move dir.left makes
T.left smaller; the Turing machine is moving left and the tape is moving right.
Equations
- turing.tape.move turing.dir.right {head := a, left := L, right := R} = {head := R.head, left := turing.list_blank.cons a L, right := R.tail}
- turing.tape.move turing.dir.left {head := a, left := L, right := R} = {head := L.head, left := L.tail, right := turing.list_blank.cons a R}
Construct a tape from a left side and an inclusive right side.
Construct a tape from a left side and an inclusive right side.
Equations
Construct a tape from a list, with the head of the list at the TM head and the rest going to the right.
Equations
The nth function of a tape is integer-valued, with index 0 being the head, negative indexes
on the left and positive indexes on the right. (Picture a number line.)
Replace the current value of the head on the tape.
Apply a pointed map to a tape to change the alphabet.
Equations
- turing.tape.map f T = {head := ⇑f T.head, left := turing.list_blank.map f T.left, right := turing.list_blank.map f T.right}
Run a state transition function σ → option σ "to completion". The return value is the last
state returned before a none result. If the state transition function always returns some,
then the computation diverges, returning roption.none.
Equations
- turing.eval f = pfun.fix (λ (s : σ), roption.some ((f s).elim (sum.inl s) sum.inr))
The reflexive transitive closure of a state transition function. reaches f a b means
there is a finite sequence of steps f a = some a₁, f a₁ = some a₂, ... such that aₙ = b.
This relation permits zero steps of the state transition function.
Equations
- turing.reaches f = relation.refl_trans_gen (λ (a b : σ), b ∈ f a)
The transitive closure of a state transition function. reaches₁ f a b means there is a
nonempty finite sequence of steps f a = some a₁, f a₁ = some a₂, ... such that aₙ = b.
This relation does not permit zero steps of the state transition function.
Equations
- turing.reaches₁ f = relation.trans_gen (λ (a b : σ), b ∈ f a)
A variation on reaches. reaches₀ f a b holds if whenever reaches₁ f b c then
reaches₁ f a c. This is a weaker property than reaches and is useful for replacing states with
equivalent states without taking a step.
Equations
- turing.reaches₀ f a b = ∀ (c : σ), turing.reaches₁ f b c → turing.reaches₁ f a c
(co-)Induction principle for eval. If a property C holds of any point a evaluating to b
which is either terminal (meaning a = b) or where the next point also satisfies C, then it
holds of any point where eval f a evaluates to b. This formalizes the notion that if
eval f a evaluates to b then it reaches terminal state b in finitely many steps.
Equations
- turing.eval_induction h H = pfun.fix_induction h (λ (a' : σ) (ha' : b ∈ pfun.fix (λ (s : σ), roption.some ((f s).elim (sum.inl s) sum.inr)) a') (h' : Π (a'_1 : σ), b ∈ pfun.fix (λ (s : σ), roption.some ((f s).elim (sum.inl s) sum.inr)) a'_1 → sum.inr a'_1 ∈ roption.some ((f a').elim (sum.inl a') sum.inr) → C a'_1), H a' ha' (λ (b' : σ) (hb' : b ∈ turing.eval f b') (e : f a' = option.some b'), h' b' hb' _))
Given a relation tr : σ₁ → σ₂ → Prop between state spaces, and state transition functions
f₁ : σ₁ → option σ₁ and f₂ : σ₂ → option σ₂, respects f₁ f₂ tr means that if tr a₁ a₂ holds
initially and f₁ takes a step to a₂ then f₂ will take one or more steps before reaching a
state b₂ satisfying tr a₂ b₂, and if f₁ a₁ terminates then f₂ a₂ also terminates.
Such a relation tr is also known as a refinement.
Equations
- turing.respects f₁ f₂ tr = ∀ ⦃a₁ : σ₁⦄ ⦃a₂ : σ₂⦄, tr a₁ a₂ → turing.respects._match_1 f₂ tr (f₁ a₁)
- turing.respects._match_1 f₂ tr (option.some b₁) = ∃ (b₂ : σ₂), tr b₁ b₂ ∧ turing.reaches₁ f₂ a₂ b₂
- turing.respects._match_1 f₂ tr option.none = (f₂ a₂ = option.none)
A simpler version of respects when the state transition relation tr is a function.
Equations
- turing.frespects f₂ tr a₂ (option.some b₁) = turing.reaches₁ f₂ a₂ (tr b₁)
- turing.frespects f₂ tr a₂ option.none = (f₂ a₂ = option.none)
The TM0 model
A TM0 turing machine is essentially a Post-Turing machine, adapted for type theory.
A Post-Turing machine with symbol type Γ and label type Λ is a function
Λ → Γ → option (Λ × stmt), where a stmt can be either move left, move right or write a
for a : Γ. The machine works over a "tape", a doubly-infinite sequence of elements of Γ, and
an instantaneous configuration, cfg, is a label q : Λ indicating the current internal state of
the machine, and a tape Γ (which is essentially ℤ →₀ Γ). The evolution is described by the
step function:
- If
M q T.head = none, then the machine halts. - If
M q T.head = some (q', s), then the machine performs actions : stmtand then transitions to stateq'.
The initial state takes a list Γ and produces a tape Γ where the head of the list is the head
of the tape and the rest of the list extends to the right, with the left side all blank. The final
state takes the entire right side of the tape right or equal to the current position of the
machine. (This is actually a list_blank Γ, not a list Γ, because we don't know, at this level
of generality, where the output ends. If equality to default Γ is decidable we can trim the list
to remove the infinite tail of blanks.)
- move : Π (Γ : Type u_1) [_inst_1 : inhabited Γ], turing.dir → turing.TM0.stmt Γ
- write : Π (Γ : Type u_1) [_inst_1 : inhabited Γ], Γ → turing.TM0.stmt Γ
A Turing machine "statement" is just a command to either move left or right, or write a symbol on the tape.
Equations
A Post-Turing machine with symbol type Γ and label type Λ
is a function which, given the current state q : Λ and
the tape head a : Γ, either halts (returns none) or returns
a new state q' : Λ and a stmt describing what to do,
either a move left or right, or a write command.
Both Λ and Γ are required to be inhabited; the default value
for Γ is the "blank" tape value, and the default value of Λ is
the initial state.
Equations
- turing.TM0.machine Γ Λ = (Λ → Γ → option (Λ × turing.TM0.stmt Γ))
Equations
- turing.TM0.machine.inhabited Γ Λ = _.mpr (pi.inhabited Λ)
- q : Λ
- tape : turing.tape Γ
The configuration state of a Turing machine during operation
consists of a label (machine state), and a tape, represented in
the form (a, L, R) meaning the tape looks like L.rev ++ [a] ++ R
with the machine currently reading the a. The lists are
automatically extended with blanks as the machine moves around.
Equations
- turing.TM0.cfg.inhabited Γ Λ = {default := {q := inhabited.default Λ _inst_2, tape := inhabited.default (turing.tape Γ) turing.tape.inhabited}}
Execution semantics of the Turing machine.
Equations
- turing.TM0.step M {q := q, tape := T} = option.map (λ (_x : Λ × turing.TM0.stmt Γ), turing.TM0.step._match_2 T _x) (M q T.head)
- turing.TM0.step._match_2 T (q', a) = {q := q', tape := turing.TM0.step._match_1 T a}
- turing.TM0.step._match_1 T (turing.TM0.stmt.write a) = turing.tape.write a T
- turing.TM0.step._match_1 T (turing.TM0.stmt.move d) = turing.tape.move d T
The statement reaches M s₁ s₂ means that s₂ is obtained
starting from s₁ after a finite number of steps from s₂.
Equations
- turing.TM0.reaches M = relation.refl_trans_gen (λ (a b : turing.TM0.cfg Γ Λ), b ∈ turing.TM0.step M a)
The initial configuration.
Equations
- turing.TM0.init l = {q := inhabited.default Λ _inst_2, tape := turing.tape.mk₁ l}
Evaluate a Turing machine on initial input to a final state, if it terminates.
Equations
- turing.TM0.eval M l = roption.map (λ (c : turing.TM0.cfg Γ Λ), c.tape.right₀) (turing.eval (turing.TM0.step M) (turing.TM0.init l))
The raw definition of a Turing machine does not require that
Γ and Λ are finite, and in practice we will be interested
in the infinite Λ case. We recover instead a notion of
"effectively finite" Turing machines, which only make use of a
finite subset of their states. We say that a set S ⊆ Λ
supports a Turing machine M if S is closed under the
transition function and contains the initial state.
Equations
- turing.TM0.supports M S = (inhabited.default Λ ∈ S ∧ ∀ {q : Λ} {a : Γ} {q' : Λ} {s : turing.TM0.stmt Γ}, (q', s) ∈ M q a → q ∈ S → q' ∈ S)
Map a TM statement across a function. This does nothing to move statements and maps the write values.
Equations
Map a configuration across a function, given f : Γ → Γ' a map of the alphabets and
g : Λ → Λ' a map of the machine states.
Equations
- turing.TM0.cfg.map f g {q := q, tape := T} = {q := g q, tape := turing.tape.map f T}
Because the state transition function uses the alphabet and machine states in both the input
and output, to map a machine from one alphabet and machine state space to another we need functions
in both directions, essentially an equiv without the laws.
Equations
- M.map f₁ f₂ g₁ g₂ q l = option.map (prod.map g₁ (turing.TM0.stmt.map f₁)) (M (g₂ q) (⇑f₂ l))
The TM1 model
The TM1 model is a simplification and extension of TM0 (Post-Turing model) in the direction of
Wang B-machines. The machine's internal state is extended with a (finite) store σ of variables
that may be accessed and updated at any time.
A machine is given by a Λ indexed set of procedures or functions. Each function has a body which
is a stmt. Most of the regular commands are allowed to use the current value a of the local
variables and the value T.head on the tape to calculate what to write or how to change local
state, but the statements themselves have a fixed structure. The stmts can be as follows:
move d q: move left or right, and then doqwrite (f : Γ → σ → Γ) q: writef a T.headto the tape, then doqload (f : Γ → σ → σ) q: change the internal state tof a T.headbranch (f : Γ → σ → bool) qtrue qfalse: Iff a T.headis true, doqtrue, elseqfalsegoto (f : Γ → σ → Λ): Go to labelf a T.headhalt: Transition to the halting state, which halts on the following step
Note that here most statements do not have labels; goto commands can only go to a new function.
Only the goto and halt statements actually take a step; the rest is done by recursion on
statements and so take 0 steps. (There is a uniform bound on many statements can be executed before
the next goto, so this is an O(1) speedup with the constant depending on the machine.)
The halt command has a one step stutter before actually halting so that any changes made before
the halt have a chance to be "committed", since the eval relation uses the final configuration
before the halt as the output, and move and write etc. take 0 steps in this model.
- move : Π (Γ : Type u_1) [_inst_1 : inhabited Γ] (Λ : Type u_2) (σ : Type u_3), turing.dir → turing.TM1.stmt Γ Λ σ → turing.TM1.stmt Γ Λ σ
- write : Π (Γ : Type u_1) [_inst_1 : inhabited Γ] (Λ : Type u_2) (σ : Type u_3), (Γ → σ → Γ) → turing.TM1.stmt Γ Λ σ → turing.TM1.stmt Γ Λ σ
- load : Π (Γ : Type u_1) [_inst_1 : inhabited Γ] (Λ : Type u_2) (σ : Type u_3), (Γ → σ → σ) → turing.TM1.stmt Γ Λ σ → turing.TM1.stmt Γ Λ σ
- branch : Π (Γ : Type u_1) [_inst_1 : inhabited Γ] (Λ : Type u_2) (σ : Type u_3), (Γ → σ → bool) → turing.TM1.stmt Γ Λ σ → turing.TM1.stmt Γ Λ σ → turing.TM1.stmt Γ Λ σ
- goto : Π (Γ : Type u_1) [_inst_1 : inhabited Γ] (Λ : Type u_2) (σ : Type u_3), (Γ → σ → Λ) → turing.TM1.stmt Γ Λ σ
- halt : Π (Γ : Type u_1) [_inst_1 : inhabited Γ] (Λ : Type u_2) (σ : Type u_3), turing.TM1.stmt Γ Λ σ
The TM1 model is a simplification and extension of TM0
(Post-Turing model) in the direction of Wang B-machines. The machine's
internal state is extended with a (finite) store σ of variables
that may be accessed and updated at any time.
A machine is given by a Λ indexed set of procedures or functions.
Each function has a body which is a stmt, which can either be a
move or write command, a branch (if statement based on the
current tape value), a load (set the variable value),
a goto (call another function), or halt. Note that here
most statements do not have labels; goto commands can only
go to a new function. All commands have access to the variable value
and current tape value.
Equations
- turing.TM1.stmt.inhabited Γ Λ σ = {default := turing.TM1.stmt.halt σ}
- l : option Λ
- var : σ
- tape : turing.tape Γ
The configuration of a TM1 machine is given by the currently evaluating statement, the variable store value, and the tape.
Equations
- turing.TM1.cfg.inhabited Γ Λ σ = {default := {l := inhabited.default (option Λ) (option.inhabited Λ), var := inhabited.default σ _inst_2, tape := inhabited.default (turing.tape Γ) turing.tape.inhabited}}
The semantics of TM1 evaluation.
Equations
- turing.TM1.step_aux turing.TM1.stmt.halt v T = {l := option.none Λ, var := v, tape := T}
- turing.TM1.step_aux (turing.TM1.stmt.goto l) v T = {l := option.some (l T.head v), var := v, tape := T}
- turing.TM1.step_aux (turing.TM1.stmt.branch p q₁ q₂) v T = cond (p T.head v) (turing.TM1.step_aux q₁ v T) (turing.TM1.step_aux q₂ v T)
- turing.TM1.step_aux (turing.TM1.stmt.load s q) v T = turing.TM1.step_aux q (s T.head v) T
- turing.TM1.step_aux (turing.TM1.stmt.write a q) v T = turing.TM1.step_aux q v (turing.tape.write (a T.head v) T)
- turing.TM1.step_aux (turing.TM1.stmt.move d q) v T = turing.TM1.step_aux q v (turing.tape.move d T)
The state transition function.
Equations
- turing.TM1.step M {l := option.some l, var := v, tape := T} = option.some (turing.TM1.step_aux (M l) v T)
- turing.TM1.step M {l := option.none Λ, var := v, tape := T} = option.none
A set S of labels supports the statement q if all the goto
statements in q refer only to other functions in S.
Equations
- turing.TM1.supports_stmt S turing.TM1.stmt.halt = true
- turing.TM1.supports_stmt S (turing.TM1.stmt.goto l) = ∀ (a : Γ) (v : σ), l a v ∈ S
- turing.TM1.supports_stmt S (turing.TM1.stmt.branch p q₁ q₂) = (turing.TM1.supports_stmt S q₁ ∧ turing.TM1.supports_stmt S q₂)
- turing.TM1.supports_stmt S (turing.TM1.stmt.load s q) = turing.TM1.supports_stmt S q
- turing.TM1.supports_stmt S (turing.TM1.stmt.write a q) = turing.TM1.supports_stmt S q
- turing.TM1.supports_stmt S (turing.TM1.stmt.move d q) = turing.TM1.supports_stmt S q
The subterm closure of a statement.
Equations
- turing.TM1.stmts₁ turing.TM1.stmt.halt = {turing.TM1.stmt.halt}
- turing.TM1.stmts₁ (turing.TM1.stmt.goto a) = {turing.TM1.stmt.goto a}
- turing.TM1.stmts₁ (turing.TM1.stmt.branch p q₁ q₂) = has_insert.insert (turing.TM1.stmt.branch p q₁ q₂) (turing.TM1.stmts₁ q₁ ∪ turing.TM1.stmts₁ q₂)
- turing.TM1.stmts₁ (turing.TM1.stmt.load s q) = has_insert.insert (turing.TM1.stmt.load s q) (turing.TM1.stmts₁ q)
- turing.TM1.stmts₁ (turing.TM1.stmt.write a q) = has_insert.insert (turing.TM1.stmt.write a q) (turing.TM1.stmts₁ q)
- turing.TM1.stmts₁ (turing.TM1.stmt.move d q) = has_insert.insert (turing.TM1.stmt.move d q) (turing.TM1.stmts₁ q)
The set of all statements in a turing machine, plus one extra value none representing the
halt state. This is used in the TM1 to TM0 reduction.
Equations
- turing.TM1.stmts M S = (S.bind (λ (q : Λ), turing.TM1.stmts₁ (M q))).insert_none
A set S of labels supports machine M if all the goto
statements in the functions in S refer only to other functions
in S.
Equations
- turing.TM1.supports M S = (inhabited.default Λ ∈ S ∧ ∀ (q : Λ), q ∈ S → turing.TM1.supports_stmt S (M q))
The initial state, given a finite input that is placed on the tape starting at the TM head and going to the right.
Equations
- turing.TM1.init l = {l := option.some (inhabited.default Λ), var := inhabited.default σ _inst_3, tape := turing.tape.mk₁ l}
Evaluate a TM to completion, resulting in an output list on the tape (with an indeterminate number of blanks on the end).
Equations
- turing.TM1.eval M l = roption.map (λ (c : turing.TM1.cfg Γ Λ σ), c.tape.right₀) (turing.eval (turing.TM1.step M) (turing.TM1.init l))
TM1 emulator in TM0
To prove that TM1 computable functions are TM0 computable, we need to reduce each TM1 program to a TM0 program. So suppose a TM1 program is given. We take the following:
- The alphabet
Γis the same for both TM1 and TM0 - The set of states
Λ'is defined to beoption stmt₁ × σ, that is, a TM1 statement ornonerepresenting halt, and the possible settings of the internal variables. Note that this is an infinite set, becausestmt₁is infinite. This is okay because we assume that from the initial TM1 state, only finitely many other labels are reachable, and there are only finitely many statements that appear in all of these functions.
Even though stmt₁ contains a statement called halt, we must separate it from none
(some halt steps to none and none actually halts) because there is a one step stutter in the
TM1 semantics.
The base machine state space is a pair of an option stmt₁ representing the current program
to be executed, or none for the halt state, and a σ which is the local state (stored in the TM,
not the tape). Because there are an infinite number of programs, this state space is infinite, but
for a finitely supported TM1 machine and a finite type σ, only finitely many of these states are
reachable.
Equations
- turing.TM1to0.Λ' M = (option (turing.TM1.stmt Γ Λ σ) × σ)
Equations
- turing.TM1to0.inhabited M = {default := (option.some (M (inhabited.default Λ)), inhabited.default σ _inst_3)}
The core TM1 → TM0 translation function. Here s is the current value on the tape, and the
stmt₁ is the TM1 statement to translate, with local state v : σ. We evaluate all regular
instructions recursively until we reach either a move or write command, or a goto; in the
latter case we emit a dummy write s step and transition to the new target location.
Equations
- turing.TM1to0.tr_aux M s turing.TM1.stmt.halt v = ((option.none (turing.TM1.stmt Γ Λ σ), v), turing.TM0.stmt.write s)
- turing.TM1to0.tr_aux M s (turing.TM1.stmt.goto l) v = ((option.some (M (l s v)), v), turing.TM0.stmt.write s)
- turing.TM1to0.tr_aux M s (turing.TM1.stmt.branch p q₁ q₂) v = cond (p s v) (turing.TM1to0.tr_aux M s q₁ v) (turing.TM1to0.tr_aux M s q₂ v)
- turing.TM1to0.tr_aux M s (turing.TM1.stmt.load a q) v = turing.TM1to0.tr_aux M s q (a s v)
- turing.TM1to0.tr_aux M s (turing.TM1.stmt.write a q) v = ((option.some q, v), turing.TM0.stmt.write (a s v))
- turing.TM1to0.tr_aux M s (turing.TM1.stmt.move d q) v = ((option.some q, v), turing.TM0.stmt.move d)
The translated TM0 machine (given the TM1 machine input).
Equations
- turing.TM1to0.tr M (option.some q, v) s = option.some (turing.TM1to0.tr_aux M s q v)
- turing.TM1to0.tr M (option.none (turing.TM1.stmt Γ Λ σ), v) s = option.none
Translate configurations from TM1 to TM0.
Equations
- turing.TM1to0.tr_cfg M {l := l, var := v, tape := T} = {q := (option.map M l, v), tape := T}
Given a finite set of accessible Λ machine states, there is a finite set of accessible
machine states in the target (even though the type Λ' is infinite).
Equations
TM1(Γ) emulator in TM1(bool)
The most parsimonious Turing machine model that is still Turing complete is TM0 with Γ = bool.
Because our construction in the previous section reducing TM1 to TM0 doesn't change the
alphabet, we can do the alphabet reduction on TM1 instead of TM0 directly.
The basic idea is to use a bijection between Γ and a subset of vector bool n, where n is a
fixed constant. Each tape element is represented as a block of n bools. Whenever the machine
wants to read a symbol from the tape, it traverses over the block, performing n branch
instructions to each any of the 2^n results.
For the write instruction, we have to use a goto because we need to follow a different code
path depending on the local state, which is not available in the TM1 model, so instead we jump to
a label computed using the read value and the local state, which performs the writing and returns
to normal execution.
Emulation overhead is O(1). If not for the above write behavior it would be 1-1 because we are
exploiting the 0-step behavior of regular commands to avoid taking steps, but there are
nevertheless a bounded number of write calls between goto statements because TM1 statements are
finitely long.
- normal : Π {Γ : Type u_1} [_inst_1 : inhabited Γ] {Λ : Type u_2} [_inst_2 : inhabited Λ] {σ : Type u_3} [_inst_3 : inhabited σ], Λ → turing.TM1to1.Λ'
- write : Π {Γ : Type u_1} [_inst_1 : inhabited Γ] {Λ : Type u_2} [_inst_2 : inhabited Λ] {σ : Type u_3} [_inst_3 : inhabited σ], Γ → turing.TM1.stmt Γ Λ σ → turing.TM1to1.Λ'
The configuration state of the TM.
Equations
Read a vector of length n from the tape.
Equations
- turing.TM1to1.read_aux (i + 1) f = turing.TM1.stmt.branch (λ (a : bool) (s : σ), a) (turing.TM1.stmt.move turing.dir.right (turing.TM1to1.read_aux i (λ (v : vector bool i), f (bool.tt :: v)))) (turing.TM1.stmt.move turing.dir.right (turing.TM1to1.read_aux i (λ (v : vector bool i), f (bool.ff :: v))))
- turing.TM1to1.read_aux 0 f = f vector.nil
A move left or right corresponds to n moves across the super-cell.
Equations
- turing.TM1to1.move d q = turing.TM1.stmt.move d^[n] q
To read a symbol from the tape, we use read_aux to traverse the symbol,
then return to the original position with n moves to the left.
Equations
- turing.TM1to1.read dec f = turing.TM1to1.read_aux n (λ (v : vector bool n), turing.TM1to1.move turing.dir.left (f (dec v)))
Write a list of bools on the tape.
Equations
- turing.TM1to1.write (a :: l) q = turing.TM1.stmt.write (λ (_x : bool) (_x : σ), a) (turing.TM1.stmt.move turing.dir.right (turing.TM1to1.write l q))
- turing.TM1to1.write list.nil q = q
Translate a normal instruction. For the write command, we use a goto indirection so that
we can access the current value of the tape.
Equations
- turing.TM1to1.tr_normal dec turing.TM1.stmt.halt = turing.TM1.stmt.halt
- turing.TM1to1.tr_normal dec (turing.TM1.stmt.goto l) = turing.TM1to1.read dec (λ (a : Γ), turing.TM1.stmt.goto (λ (_x : bool) (s : σ), turing.TM1to1.Λ'.normal (l a s)))
- turing.TM1to1.tr_normal dec (turing.TM1.stmt.branch p q₁ q₂) = turing.TM1to1.read dec (λ (a : Γ), turing.TM1.stmt.branch (λ (_x : bool) (s : σ), p a s) (turing.TM1to1.tr_normal dec q₁) (turing.TM1to1.tr_normal dec q₂))
- turing.TM1to1.tr_normal dec (turing.TM1.stmt.load f q) = turing.TM1to1.read dec (λ (a : Γ), turing.TM1.stmt.load (λ (_x : bool) (s : σ), f a s) (turing.TM1to1.tr_normal dec q))
- turing.TM1to1.tr_normal dec (turing.TM1.stmt.write f q) = turing.TM1to1.read dec (λ (a : Γ), turing.TM1.stmt.goto (λ (_x : bool) (s : σ), turing.TM1to1.Λ'.write (f a s) q))
- turing.TM1to1.tr_normal dec (turing.TM1.stmt.move d q) = turing.TM1to1.move d (turing.TM1to1.tr_normal dec q)
The low level tape corresponding to the given tape over alphabet Γ.
Equations
- turing.TM1to1.tr_tape' enc0 L R = turing.tape.mk' (L.bind (λ (x : Γ), (enc x).to_list.reverse) _) (R.bind (λ (x : Γ), (enc x).to_list) _)
The low level tape corresponding to the given tape over alphabet Γ.
Equations
- turing.TM1to1.tr_tape enc0 T = turing.TM1to1.tr_tape' enc0 T.left T.right₀
The top level program.
Equations
- turing.TM1to1.tr enc dec M (turing.TM1to1.Λ'.write a q) = turing.TM1to1.write (enc a).to_list (turing.TM1to1.move turing.dir.left (turing.TM1to1.tr_normal dec q))
- turing.TM1to1.tr enc dec M (turing.TM1to1.Λ'.normal l) = turing.TM1to1.tr_normal dec (M l)
The machine configuration translation.
Equations
- turing.TM1to1.tr_cfg enc0 {l := l, var := v, tape := T} = {l := option.map turing.TM1to1.Λ'.normal l, var := v, tape := turing.TM1to1.tr_tape enc0 T}
The set of accessible Λ'.write machine states.
Equations
- turing.TM1to1.writes turing.TM1.stmt.halt = ∅
- turing.TM1to1.writes (turing.TM1.stmt.goto l) = ∅
- turing.TM1to1.writes (turing.TM1.stmt.branch p q₁ q₂) = turing.TM1to1.writes q₁ ∪ turing.TM1to1.writes q₂
- turing.TM1to1.writes (turing.TM1.stmt.load f q) = turing.TM1to1.writes q
- turing.TM1to1.writes (turing.TM1.stmt.write f q) = finset.image (λ (a : Γ), turing.TM1to1.Λ'.write a q) finset.univ ∪ turing.TM1to1.writes q
- turing.TM1to1.writes (turing.TM1.stmt.move d q) = turing.TM1to1.writes q
The set of accessible machine states, assuming that the input machine is supported on S,
are the normal states embedded from S, plus all write states accessible from these states.
Equations
- turing.TM1to1.tr_supp M S = S.bind (λ (l : Λ), has_insert.insert (turing.TM1to1.Λ'.normal l) (turing.TM1to1.writes (M l)))
TM0 emulator in TM1
To establish that TM0 and TM1 are equivalent computational models, we must also have a TM0 emulator
in TM1. The main complication here is that TM0 allows an action to depend on the value at the head
and local state, while TM1 doesn't (in order to have more programming language-like semantics).
So we use a computed goto to go to a state that performes the desired action and then returns to
normal execution.
One issue with this is that the halt instruction is supposed to halt immediately, not take a step
to a halting state. To resolve this we do a check for halt first, then goto (with an
unreachable branch).
- normal : Π {Γ : Type u_1} [_inst_1 : inhabited Γ] {Λ : Type u_2} [_inst_2 : inhabited Λ], Λ → turing.TM0to1.Λ'
- act : Π {Γ : Type u_1} [_inst_1 : inhabited Γ] {Λ : Type u_2} [_inst_2 : inhabited Λ], turing.TM0.stmt Γ → Λ → turing.TM0to1.Λ'
The machine states for a TM1 emulating a TM0 machine. States of the TM0 machine are embedded
as normal q states, but the actual operation is split into two parts, a jump to act s q
followed by the action and a jump to the next normal state.
Equations
The program.
Equations
- turing.TM0to1.tr M (turing.TM0to1.Λ'.act (turing.TM0.stmt.write a) q) = turing.TM1.stmt.write (λ (_x : Γ) (_x : unit), a) (turing.TM1.stmt.goto (λ (_x : Γ) (_x : unit), turing.TM0to1.Λ'.normal q))
- turing.TM0to1.tr M (turing.TM0to1.Λ'.act (turing.TM0.stmt.move d) q) = turing.TM1.stmt.move d (turing.TM1.stmt.goto (λ (_x : Γ) (_x : unit), turing.TM0to1.Λ'.normal q))
- turing.TM0to1.tr M (turing.TM0to1.Λ'.normal q) = turing.TM1.stmt.branch (λ (a : Γ) (_x : unit), (M q a).is_none) turing.TM1.stmt.halt (turing.TM1.stmt.goto (λ (a : Γ) (_x : unit), turing.TM0to1.tr._match_1 (M q a)))
- turing.TM0to1.tr._match_1 (option.some (q', s)) = turing.TM0to1.Λ'.act s q'
- turing.TM0to1.tr._match_1 option.none = inhabited.default turing.TM0to1.Λ'
The configuration translation.
Equations
- turing.TM0to1.tr_cfg M {q := q, tape := T} = {l := cond (M q T.head).is_some (option.some (turing.TM0to1.Λ'.normal q)) option.none, var := (), tape := T}
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) qputsf aon thek-th stack, then doesq.pop k (f : σ → option (Γ k) → σ) qchanges the state tof a (S k).head, whereS kis the value of thek-th stack, and removes this element from the stack, then doesq.peek k (f : σ → option (Γ k) → σ) qchanges the state tof a (S k).head, whereS kis the value of thek-th stack, then doesq.load (f : σ → σ) qreads nothing but appliesfto the internal state, then doesq.branch (f : σ → bool) qtrue qfalsedoesqtrueorqfalseaccording tof a.goto (f : σ → Λ)jumps to labelf a.halthalts 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
list_blanks, 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.
- push : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) (k : K), (σ → Γ k) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
- peek : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) (k : K), (σ → option (Γ k) → σ) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
- pop : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) (k : K), (σ → option (Γ k) → σ) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
- load : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4), (σ → σ) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
- branch : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4), (σ → bool) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
- goto : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4), (σ → Λ) → turing.TM2.stmt Γ Λ σ
- halt : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4), turing.TM2.stmt Γ Λ σ
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.
Equations
- turing.TM2.stmt.inhabited Γ Λ σ = {default := turing.TM2.stmt.halt σ}
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 list_blanks, they have a definite
size.)
Equations
- turing.TM2.cfg.inhabited Γ Λ σ = {default := {l := inhabited.default (option Λ) (option.inhabited Λ), var := inhabited.default σ _inst_2, stk := inhabited.default (Π (k : K), list (Γ k)) (pi.inhabited K)}}
The step function for the TM2 model.
Equations
- turing.TM2.step_aux turing.TM2.stmt.halt v S = {l := option.none Λ, var := v, stk := S}
- turing.TM2.step_aux (turing.TM2.stmt.goto f) v S = {l := option.some (f v), var := v, stk := S}
- turing.TM2.step_aux (turing.TM2.stmt.branch f q₁ q₂) v S = cond (f v) (turing.TM2.step_aux q₁ v S) (turing.TM2.step_aux q₂ v S)
- turing.TM2.step_aux (turing.TM2.stmt.load a q) v S = turing.TM2.step_aux q (a v) S
- turing.TM2.step_aux (turing.TM2.stmt.pop k f q) v S = turing.TM2.step_aux q (f v (S k).head') (function.update S k (S k).tail)
- turing.TM2.step_aux (turing.TM2.stmt.peek k f q) v S = turing.TM2.step_aux q (f v (S k).head') S
- turing.TM2.step_aux (turing.TM2.stmt.push k f q) v S = turing.TM2.step_aux q v (function.update S k (f v :: S k))
The step function for the TM2 model.
Equations
- turing.TM2.step M {l := option.some l, var := v, stk := S} = option.some (turing.TM2.step_aux (M l) v S)
- turing.TM2.step M {l := option.none Λ, var := v, stk := S} = option.none
The (reflexive) reachability relation for the TM2 model.
Equations
- turing.TM2.reaches M = relation.refl_trans_gen (λ (a b : turing.TM2.cfg Γ Λ σ), b ∈ turing.TM2.step M a)
Given a set S of states, support_stmt S q means that q only jumps to states in S.
Equations
- turing.TM2.supports_stmt S turing.TM2.stmt.halt = true
- turing.TM2.supports_stmt S (turing.TM2.stmt.goto l) = ∀ (v : σ), l v ∈ S
- turing.TM2.supports_stmt S (turing.TM2.stmt.branch f q₁ q₂) = (turing.TM2.supports_stmt S q₁ ∧ turing.TM2.supports_stmt S q₂)
- turing.TM2.supports_stmt S (turing.TM2.stmt.load a q) = turing.TM2.supports_stmt S q
- turing.TM2.supports_stmt S (turing.TM2.stmt.pop k f q) = turing.TM2.supports_stmt S q
- turing.TM2.supports_stmt S (turing.TM2.stmt.peek k f q) = turing.TM2.supports_stmt S q
- turing.TM2.supports_stmt S (turing.TM2.stmt.push k f q) = turing.TM2.supports_stmt S q
The set of subtree statements in a statement.
Equations
- turing.TM2.stmts₁ turing.TM2.stmt.halt = {turing.TM2.stmt.halt}
- turing.TM2.stmts₁ (turing.TM2.stmt.goto l) = {turing.TM2.stmt.goto l}
- turing.TM2.stmts₁ (turing.TM2.stmt.branch f q₁ q₂) = has_insert.insert (turing.TM2.stmt.branch f q₁ q₂) (turing.TM2.stmts₁ q₁ ∪ turing.TM2.stmts₁ q₂)
- turing.TM2.stmts₁ (turing.TM2.stmt.load a q) = has_insert.insert (turing.TM2.stmt.load a q) (turing.TM2.stmts₁ q)
- turing.TM2.stmts₁ (turing.TM2.stmt.pop k f q) = has_insert.insert (turing.TM2.stmt.pop k f q) (turing.TM2.stmts₁ q)
- turing.TM2.stmts₁ (turing.TM2.stmt.peek k f q) = has_insert.insert (turing.TM2.stmt.peek k f q) (turing.TM2.stmts₁ q)
- turing.TM2.stmts₁ (turing.TM2.stmt.push k f q) = has_insert.insert (turing.TM2.stmt.push k f q) (turing.TM2.stmts₁ q)
The set of statements accessible from initial set S of labels.
Equations
- turing.TM2.stmts M S = (S.bind (λ (q : Λ), turing.TM2.stmts₁ (M q))).insert_none
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 = (inhabited.default Λ ∈ S ∧ ∀ (q : Λ), q ∈ S → turing.TM2.supports_stmt S (M q))
The initial state of the TM2 model. The input is provided on a designated stack.
Equations
- turing.TM2.init k L = {l := option.some (inhabited.default Λ), var := inhabited.default σ _inst_3, stk := function.update (λ (_x : K), list.nil) k L}
Evaluates a TM2 program to completion, with the output on the same stack as the input.
Equations
- turing.TM2.eval M k L = roption.map (λ (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 : boolis 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 thek-th stack, if in range, otherwisenone(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 atbottomto execute functionlgo k (s : st_act k) (q : stmt₂): travelling to the right to get to the end of stackkin order to perform stack actions, and later continue with executingqret (q : stmt₂): travelling to the left after having performed a stack action, and executingqonce 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.
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.Γ' = (bool × Π (k : K), option (Γ k))
Equations
- turing.TM2to1.Γ'.inhabited = {default := (bool.ff, λ (_x : K), option.none)}
Equations
- turing.TM2to1.Γ'.fintype = prod.fintype bool (Π (k : K), option (Γ k))
The bottom marker is fixed throughout the calculation, so we use the add_bottom function
to express the program state in terms of a tape with only the stacks themselves.
Equations
- turing.TM2to1.add_bottom L = turing.list_blank.cons (bool.tt, L.head) (turing.list_blank.map {f := prod.mk bool.ff, map_pt' := _} L.tail)
- push : Π {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {σ : Type u_4} [_inst_3 : inhabited σ] (k : K), (σ → Γ k) → turing.TM2to1.st_act k
- peek : Π {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {σ : Type u_4} [_inst_3 : inhabited σ] (k : K), (σ → option (Γ k) → σ) → turing.TM2to1.st_act k
- pop : Π {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {σ : Type u_4} [_inst_3 : inhabited σ] (k : K), (σ → option (Γ k) → σ) → turing.TM2to1.st_act k
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.
Equations
- turing.TM2to1.st_act.inhabited = {default := turing.TM2to1.st_act.peek (λ (s : σ) (_x : option (Γ k)), s)}
The TM2 statement corresponding to a stack action.
The effect of a stack action on the local variables, given the value of the stack.
Equations
- turing.TM2to1.st_var v l (turing.TM2to1.st_act.pop f) = f v l.head'
- turing.TM2to1.st_var v l (turing.TM2to1.st_act.peek f) = f v l.head'
- turing.TM2to1.st_var v l (turing.TM2to1.st_act.push f) = v
The effect of a stack action on the stack.
Equations
- turing.TM2to1.st_write v l (turing.TM2to1.st_act.pop f) = l.tail
- turing.TM2to1.st_write v l (turing.TM2to1.st_act.peek f) = l
- turing.TM2to1.st_write v l (turing.TM2to1.st_act.push f) = f v :: l
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.stmt_st_rec H₁ H₂ H₃ H₄ H₅ turing.TM2.stmt.halt = H₅
- turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ (turing.TM2.stmt.goto l) = H₄ l
- turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ (turing.TM2.stmt.branch a q₁ q₂) = H₃ a q₁ q₂ (turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ q₁) (turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ q₂)
- turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ (turing.TM2.stmt.load a q) = H₂ a q (turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ q)
- turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ (turing.TM2.stmt.pop k f q) = H₁ k (turing.TM2to1.st_act.pop f) q (turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ q)
- turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ (turing.TM2.stmt.peek k f q) = H₁ k (turing.TM2to1.st_act.peek f) q (turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ q)
- turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ (turing.TM2.stmt.push k f q) = H₁ k (turing.TM2to1.st_act.push f) q (turing.TM2to1.stmt_st_rec H₁ H₂ H₃ H₄ H₅ q)
- normal : Π {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [_inst_2 : inhabited Λ] {σ : Type u_4} [_inst_3 : inhabited σ], Λ → turing.TM2to1.Λ'
- go : Π {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [_inst_2 : inhabited Λ] {σ : Type u_4} [_inst_3 : inhabited σ] (k : K), turing.TM2to1.st_act k → turing.TM2.stmt Γ Λ σ → turing.TM2to1.Λ'
- ret : Π {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [_inst_2 : inhabited Λ] {σ : Type u_4} [_inst_3 : inhabited σ], turing.TM2.stmt Γ Λ σ → turing.TM2to1.Λ'
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.
Equations
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
- turing.TM2to1.tr_st_act q (turing.TM2to1.st_act.pop f) = turing.TM1.stmt.branch (λ (a : turing.TM2to1.Γ') (_x : σ), a.fst) (turing.TM1.stmt.load (λ (a : turing.TM2to1.Γ') (s : σ), f s option.none) q) (turing.TM1.stmt.move turing.dir.left (turing.TM1.stmt.load (λ (a : turing.TM2to1.Γ') (s : σ), f s (a.snd k)) (turing.TM1.stmt.write (λ (a : turing.TM2to1.Γ') (s : σ), (a.fst, function.update a.snd k option.none)) q)))
- turing.TM2to1.tr_st_act q (turing.TM2to1.st_act.peek f) = turing.TM1.stmt.move turing.dir.left (turing.TM1.stmt.load (λ (a : turing.TM2to1.Γ') (s : σ), f s (a.snd k)) (turing.TM1.stmt.move turing.dir.right q))
- turing.TM2to1.tr_st_act q (turing.TM2to1.st_act.push f) = turing.TM1.stmt.write (λ (a : turing.TM2to1.Γ') (s : σ), (a.fst, function.update a.snd k (option.some (f s)))) (turing.TM1.stmt.move turing.dir.right q)
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
- turing.TM2to1.tr_init k L = let L' : list turing.TM2to1.Γ' := list.map (λ (a : Γ k), (bool.ff, function.update (λ (_x : K), option.none) k ↑a)) L.reverse in (bool.tt, L'.head.snd) :: L'.tail
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.tr_normal turing.TM2.stmt.halt = turing.TM1.stmt.halt
- turing.TM2to1.tr_normal (turing.TM2.stmt.goto l) = turing.TM1.stmt.goto (λ (a : turing.TM2to1.Γ') (s : σ), turing.TM2to1.Λ'.normal (l s))
- turing.TM2to1.tr_normal (turing.TM2.stmt.branch f q₁ q₂) = turing.TM1.stmt.branch (λ (a : turing.TM2to1.Γ'), f) (turing.TM2to1.tr_normal q₁) (turing.TM2to1.tr_normal q₂)
- turing.TM2to1.tr_normal (turing.TM2.stmt.load a q) = turing.TM1.stmt.load (λ (_x : turing.TM2to1.Γ'), a) (turing.TM2to1.tr_normal q)
- turing.TM2to1.tr_normal (turing.TM2.stmt.pop k f q) = turing.TM1.stmt.goto (λ (_x : turing.TM2to1.Γ') (_x : σ), turing.TM2to1.Λ'.go k (turing.TM2to1.st_act.pop f) q)
- turing.TM2to1.tr_normal (turing.TM2.stmt.peek k f q) = turing.TM1.stmt.goto (λ (_x : turing.TM2to1.Γ') (_x : σ), turing.TM2to1.Λ'.go k (turing.TM2to1.st_act.peek f) q)
- turing.TM2to1.tr_normal (turing.TM2.stmt.push k f q) = turing.TM1.stmt.goto (λ (_x : turing.TM2to1.Γ') (_x : σ), turing.TM2to1.Λ'.go k (turing.TM2to1.st_act.push f) q)
The set of machine states accessible from an initial TM2 statement.
Equations
- turing.TM2to1.tr_stmts₁ turing.TM2.stmt.halt = ∅
- turing.TM2to1.tr_stmts₁ (turing.TM2.stmt.goto a) = ∅
- turing.TM2to1.tr_stmts₁ (turing.TM2.stmt.branch f q₁ q₂) = turing.TM2to1.tr_stmts₁ q₁ ∪ turing.TM2to1.tr_stmts₁ q₂
- turing.TM2to1.tr_stmts₁ (turing.TM2.stmt.load a q) = turing.TM2to1.tr_stmts₁ q
- turing.TM2to1.tr_stmts₁ (turing.TM2.stmt.pop k f q) = {turing.TM2to1.Λ'.go k (turing.TM2to1.st_act.pop f) q, turing.TM2to1.Λ'.ret q} ∪ turing.TM2to1.tr_stmts₁ q
- turing.TM2to1.tr_stmts₁ (turing.TM2.stmt.peek k f q) = {turing.TM2to1.Λ'.go k (turing.TM2to1.st_act.peek f) q, turing.TM2to1.Λ'.ret q} ∪ turing.TM2to1.tr_stmts₁ q
- turing.TM2to1.tr_stmts₁ (turing.TM2.stmt.push k f q) = {turing.TM2to1.Λ'.go k (turing.TM2to1.st_act.push f) q, turing.TM2to1.Λ'.ret q} ∪ turing.TM2to1.tr_stmts₁ q
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
- turing.TM2to1.tr M (turing.TM2to1.Λ'.ret q) = turing.TM1.stmt.branch (λ (a : turing.TM2to1.Γ') (s : σ), a.fst) (turing.TM2to1.tr_normal q) (turing.TM1.stmt.move turing.dir.left (turing.TM1.stmt.goto (λ (_x : turing.TM2to1.Γ') (_x : σ), turing.TM2to1.Λ'.ret q)))
- turing.TM2to1.tr M (turing.TM2to1.Λ'.go k s q) = turing.TM1.stmt.branch (λ (a : turing.TM2to1.Γ') (s : σ), (a.snd k).is_none) (turing.TM2to1.tr_st_act (turing.TM1.stmt.goto (λ (_x : turing.TM2to1.Γ') (_x : σ), turing.TM2to1.Λ'.ret q)) s) (turing.TM1.stmt.move turing.dir.right (turing.TM1.stmt.goto (λ (_x : turing.TM2to1.Γ') (_x : σ), turing.TM2to1.Λ'.go k s q)))
- turing.TM2to1.tr M (turing.TM2to1.Λ'.normal q) = turing.TM2to1.tr_normal (M q)
- mk : ∀ {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [_inst_2 : inhabited Λ] {σ : Type u_4} [_inst_3 : inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) {q : option Λ} {v : σ} {S : Π (k : K), list (Γ k)} (L : turing.list_blank (Π (k : K), option (Γ k))), (∀ (k : K), turing.list_blank.map (turing.proj k) L = turing.list_blank.mk (list.map option.some (S k)).reverse) → turing.TM2to1.tr_cfg M {l := q, var := v, stk := S} {l := option.map turing.TM2to1.Λ'.normal q, var := v, tape := turing.tape.mk' ∅ (turing.TM2to1.add_bottom L)}
The relation between TM2 configurations and TM1 configurations of the TM2 emulator.
The support of a set of TM2 states in the TM2 emulator.
Equations
- turing.TM2to1.tr_supp M S = S.bind (λ (l : Λ), has_insert.insert (turing.TM2to1.Λ'.normal l) (turing.TM2to1.tr_stmts₁ (M l)))