mathlib3 documentation

computability.turing_machine

Turing machines #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 Λ.
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.

def turing.blank_extends {Γ : Type u_1} [inhabited Γ] (l₁ l₂ : list Γ) :

Prop

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.replicate n inhabited.default

@[refl]

theorem turing.blank_extends.refl {Γ : Type u_1} [inhabited Γ] (l : list Γ) :

turing.blank_extends l l

@[trans]

theorem turing.blank_extends.trans {Γ : Type u_1} [inhabited Γ] {l₁ l₂ l₃ : list Γ} :

turing.blank_extends l₁ l₂ → turing.blank_extends l₂ l₃ → turing.blank_extends l₁ l₃

theorem turing.blank_extends.below_of_le {Γ : Type u_1} [inhabited Γ] {l l₁ l₂ : list Γ} :

turing.blank_extends l l₁ → turing.blank_extends l l₂ → l₁.length ≤ l₂.length → turing.blank_extends l₁ l₂

def turing.blank_extends.above {Γ : Type u_1} [inhabited Γ] {l l₁ l₂ : list Γ} (h₁ : turing.blank_extends l l₁) (h₂ : turing.blank_extends l l₂) :

{l' // turing.blank_extends l₁ l' ∧ turing.blank_extends l₂ l'}

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₂).

Equations

h₁.above h₂ = dite (l₁.length ≤ l₂.length) (λ (h : l₁.length ≤ l₂.length), ⟨l₂, _⟩) (λ (h : ¬l₁.length ≤ l₂.length), ⟨l₁, _⟩)

theorem turing.blank_extends.above_of_le {Γ : Type u_1} [inhabited Γ] {l l₁ l₂ : list Γ} :

turing.blank_extends l₁ l → turing.blank_extends l₂ l → l₁.length ≤ l₂.length → turing.blank_extends l₁ l₂

def turing.blank_rel {Γ : Type u_1} [inhabited Γ] (l₁ l₂ : list Γ) :

Prop

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₁)

@[refl]

theorem turing.blank_rel.refl {Γ : Type u_1} [inhabited Γ] (l : list Γ) :

turing.blank_rel l l

@[symm]

theorem turing.blank_rel.symm {Γ : Type u_1} [inhabited Γ] {l₁ l₂ : list Γ} :

turing.blank_rel l₁ l₂ → turing.blank_rel l₂ l₁

@[trans]

theorem turing.blank_rel.trans {Γ : Type u_1} [inhabited Γ] {l₁ l₂ l₃ : list Γ} :

turing.blank_rel l₁ l₂ → turing.blank_rel l₂ l₃ → turing.blank_rel l₁ l₃

def turing.blank_rel.above {Γ : Type u_1} [inhabited Γ] {l₁ l₂ : list Γ} (h : turing.blank_rel l₁ l₂) :

{l // turing.blank_extends l₁ l ∧ turing.blank_extends l₂ l}

Given two blank_rel lists, there exists (constructively) a common join.

Equations

h.above = dite (l₁.length ≤ l₂.length) (λ (hl : l₁.length ≤ l₂.length), ⟨l₂, _⟩) (λ (hl : ¬l₁.length ≤ l₂.length), ⟨l₁, _⟩)

def turing.blank_rel.below {Γ : Type u_1} [inhabited Γ] {l₁ l₂ : list Γ} (h : turing.blank_rel l₁ l₂) :

{l // turing.blank_extends l l₁ ∧ turing.blank_extends l l₂}

Given two blank_rel lists, there exists (constructively) a common meet.

Equations

h.below = dite (l₁.length ≤ l₂.length) (λ (hl : l₁.length ≤ l₂.length), ⟨l₁, _⟩) (λ (hl : ¬l₁.length ≤ l₂.length), ⟨l₂, _⟩)

theorem turing.blank_rel.equivalence (Γ : Type u_1) [inhabited Γ] :

equivalence turing.blank_rel

def turing.blank_rel.setoid (Γ : Type u_1) [inhabited Γ] :

setoid (list Γ)

Construct a setoid instance for blank_rel.

Equations

turing.blank_rel.setoid Γ = {r := turing.blank_rel _inst_1, iseqv := _}

def turing.list_blank (Γ : Type u_1) [inhabited Γ] :

Type u_1

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

turing.list_blank Γ = quotient (turing.blank_rel.setoid Γ)

Instances for turing.list_blank

@[protected, instance]

def turing.list_blank.inhabited {Γ : Type u_1} [inhabited Γ] :

inhabited (turing.list_blank Γ)

Equations

turing.list_blank.inhabited = {default := quotient.mk' list.nil}

@[protected, instance]

def turing.list_blank.has_emptyc {Γ : Type u_1} [inhabited Γ] :

has_emptyc (turing.list_blank Γ)

Equations

turing.list_blank.has_emptyc = {emptyc := quotient.mk' list.nil}

@[protected, reducible]

def turing.list_blank.lift_on {Γ : Type u_1} [inhabited Γ] {α : Sort u_2} (l : turing.list_blank Γ) (f : list Γ → α) (H : ∀ (a b : list Γ), turing.blank_extends a b → f a = f b) :

α

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 _

def turing.list_blank.mk {Γ : Type u_1} [inhabited Γ] :

list Γ → turing.list_blank Γ

The quotient map turning a list into a list_blank.

Equations

turing.list_blank.mk = quotient.mk'

@[protected]

theorem turing.list_blank.induction_on {Γ : Type u_1} [inhabited Γ] {p : turing.list_blank Γ → Prop} (q : turing.list_blank Γ) (h : ∀ (a : list Γ), p (turing.list_blank.mk a)) :

p q

def turing.list_blank.head {Γ : Type u_1} [inhabited Γ] (l : turing.list_blank Γ) :

Γ

The head of a list_blank is well defined.

Equations

l.head = l.lift_on list.head turing.list_blank.head._proof_1

@[simp]

theorem turing.list_blank.head_mk {Γ : Type u_1} [inhabited Γ] (l : list Γ) :

(turing.list_blank.mk l).head = l.head

def turing.list_blank.tail {Γ : Type u_1} [inhabited Γ] (l : turing.list_blank Γ) :

turing.list_blank Γ

The tail of a list_blank is well defined (up to the tail of blanks).

Equations

l.tail = l.lift_on (λ (l : list Γ), turing.list_blank.mk l.tail) turing.list_blank.tail._proof_1

@[simp]

theorem turing.list_blank.tail_mk {Γ : Type u_1} [inhabited Γ] (l : list Γ) :

(turing.list_blank.mk l).tail = turing.list_blank.mk l.tail

def turing.list_blank.cons {Γ : Type u_1} [inhabited Γ] (a : Γ) (l : turing.list_blank Γ) :

turing.list_blank Γ

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)) _

@[simp]

theorem turing.list_blank.cons_mk {Γ : Type u_1} [inhabited Γ] (a : Γ) (l : list Γ) :

turing.list_blank.cons a (turing.list_blank.mk l) = turing.list_blank.mk (a :: l)

@[simp]

theorem turing.list_blank.head_cons {Γ : Type u_1} [inhabited Γ] (a : Γ) (l : turing.list_blank Γ) :

(turing.list_blank.cons a l).head = a

@[simp]

theorem turing.list_blank.tail_cons {Γ : Type u_1} [inhabited Γ] (a : Γ) (l : turing.list_blank Γ) :

(turing.list_blank.cons a l).tail = l

@[simp]

theorem turing.list_blank.cons_head_tail {Γ : Type u_1} [inhabited Γ] (l : turing.list_blank Γ) :

turing.list_blank.cons l.head l.tail = l

The cons and head/tail functions are mutually inverse, unlike in the case of list where this only holds for nonempty lists.

theorem turing.list_blank.exists_cons {Γ : Type u_1} [inhabited Γ] (l : turing.list_blank Γ) :

∃ (a : Γ) (l' : turing.list_blank Γ), l = turing.list_blank.cons a l'

The cons and head/tail functions are mutually inverse, unlike in the case of list where this only holds for nonempty lists.

def turing.list_blank.nth {Γ : Type u_1} [inhabited Γ] (l : turing.list_blank Γ) (n : ℕ) :

Γ

The n-th element of a list_blank is well defined for all n : ℕ, unlike in a list.

Equations

l.nth n = l.lift_on (λ (l : list Γ), l.inth n) _

@[simp]

theorem turing.list_blank.nth_mk {Γ : Type u_1} [inhabited Γ] (l : list Γ) (n : ℕ) :

(turing.list_blank.mk l).nth n = l.inth n

@[simp]

theorem turing.list_blank.nth_zero {Γ : Type u_1} [inhabited Γ] (l : turing.list_blank Γ) :

l.nth 0 = l.head

@[simp]

theorem turing.list_blank.nth_succ {Γ : Type u_1} [inhabited Γ] (l : turing.list_blank Γ) (n : ℕ) :

l.nth (n + 1) = l.tail.nth n

@[ext]

theorem turing.list_blank.ext {Γ : Type u_1} [inhabited Γ] {L₁ L₂ : turing.list_blank Γ} :

(∀ (i : ℕ), L₁.nth i = L₂.nth i) → L₁ = L₂

@[simp]

def turing.list_blank.modify_nth {Γ : Type u_1} [inhabited Γ] (f : Γ → Γ) :

ℕ → turing.list_blank Γ → turing.list_blank Γ

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

theorem turing.list_blank.nth_modify_nth {Γ : Type u_1} [inhabited Γ] (f : Γ → Γ) (n i : ℕ) (L : turing.list_blank Γ) :

(turing.list_blank.modify_nth f n L).nth i = ite (i = n) (f (L.nth i)) (L.nth i)

structure turing.pointed_map (Γ : Type u) (Γ' : Type v) [inhabited Γ] [inhabited Γ'] :

Type (max u v)

f : Γ → Γ'
map_pt' : self.f inhabited.default = inhabited.default

A pointed map of inhabited types is a map that sends one default value to the other.

Instances for turing.pointed_map

@[protected, instance]

def turing.pointed_map.inhabited {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] :

inhabited (turing.pointed_map Γ Γ')

Equations

turing.pointed_map.inhabited = {default := {f := inhabited.default (pi.inhabited Γ), map_pt' := _}}

@[protected, instance]

def turing.pointed_map.has_coe_to_fun {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] :

has_coe_to_fun (turing.pointed_map Γ Γ') (λ (_x : turing.pointed_map Γ Γ'), Γ → Γ')

Equations

turing.pointed_map.has_coe_to_fun = {coe := turing.pointed_map.f _inst_2}

@[simp]

theorem turing.pointed_map.mk_val {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : Γ → Γ') (pt : f inhabited.default = inhabited.default) :

⇑{f := f, map_pt' := pt} = f

@[simp]

theorem turing.pointed_map.map_pt {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') :

⇑f inhabited.default = inhabited.default

@[simp]

theorem turing.pointed_map.head_map {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : list Γ) :

(list.map ⇑f l).head = ⇑f l.head

def turing.list_blank.map {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : turing.list_blank Γ) :

turing.list_blank Γ'

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)) _

@[simp]

theorem turing.list_blank.map_mk {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : list Γ) :

turing.list_blank.map f (turing.list_blank.mk l) = turing.list_blank.mk (list.map ⇑f l)

@[simp]

theorem turing.list_blank.head_map {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : turing.list_blank Γ) :

(turing.list_blank.map f l).head = ⇑f l.head

@[simp]

theorem turing.list_blank.tail_map {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : turing.list_blank Γ) :

(turing.list_blank.map f l).tail = turing.list_blank.map f l.tail

@[simp]

theorem turing.list_blank.map_cons {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : turing.list_blank Γ) (a : Γ) :

turing.list_blank.map f (turing.list_blank.cons a l) = turing.list_blank.cons (⇑f a) (turing.list_blank.map f l)

@[simp]

theorem turing.list_blank.nth_map {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : turing.list_blank Γ) (n : ℕ) :

(turing.list_blank.map f l).nth n = ⇑f (l.nth n)

def turing.proj {ι : Type u_1} {Γ : ι → Type u_2} [Π (i : ι), inhabited (Γ i)] (i : ι) :

turing.pointed_map (Π (i : ι), Γ i) (Γ i)

The i-th projection as a pointed map.

Equations

turing.proj i = {f := λ (a : Π (i : ι), Γ i), a i, map_pt' := _}

theorem turing.proj_map_nth {ι : Type u_1} {Γ : ι → Type u_2} [Π (i : ι), inhabited (Γ i)] (i : ι) (L : turing.list_blank (Π (i : ι), Γ i)) (n : ℕ) :

(turing.list_blank.map (turing.proj i) L).nth n = L.nth n i

theorem turing.list_blank.map_modify_nth {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (F : turing.pointed_map Γ Γ') (f : Γ → Γ) (f' : Γ' → Γ') (H : ∀ (x : Γ), ⇑F (f x) = f' (⇑F x)) (n : ℕ) (L : turing.list_blank Γ) :

turing.list_blank.map F (turing.list_blank.modify_nth f n L) = turing.list_blank.modify_nth f' n (turing.list_blank.map F L)

@[simp]

def turing.list_blank.append {Γ : Type u_1} [inhabited Γ] :

list Γ → turing.list_blank Γ → turing.list_blank Γ

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

@[simp]

theorem turing.list_blank.append_mk {Γ : Type u_1} [inhabited Γ] (l₁ l₂ : list Γ) :

turing.list_blank.append l₁ (turing.list_blank.mk l₂) = turing.list_blank.mk (l₁ ++ l₂)

theorem turing.list_blank.append_assoc {Γ : Type u_1} [inhabited Γ] (l₁ l₂ : list Γ) (l₃ : turing.list_blank Γ) :

turing.list_blank.append (l₁ ++ l₂) l₃ = turing.list_blank.append l₁ (turing.list_blank.append l₂ l₃)

def turing.list_blank.bind {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (l : turing.list_blank Γ) (f : Γ → list Γ') (hf : ∃ (n : ℕ), f inhabited.default = list.replicate n inhabited.default) :

turing.list_blank Γ'

The bind function on lists is well defined on list_blanks provided that the default element is sent to a sequence of default elements.

Equations

l.bind f hf = l.lift_on (λ (l : list Γ), turing.list_blank.mk (l.bind f)) _

@[simp]

theorem turing.list_blank.bind_mk {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (l : list Γ) (f : Γ → list Γ') (hf : ∃ (n : ℕ), f inhabited.default = list.replicate n inhabited.default) :

(turing.list_blank.mk l).bind f hf = turing.list_blank.mk (l.bind f)

@[simp]

theorem turing.list_blank.cons_bind {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (a : Γ) (l : turing.list_blank Γ) (f : Γ → list Γ') (hf : ∃ (n : ℕ), f inhabited.default = list.replicate n inhabited.default) :

(turing.list_blank.cons a l).bind f hf = turing.list_blank.append (f a) (l.bind f hf)

structure turing.tape (Γ : Type u_1) [inhabited Γ] :

Type u_1

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.

Instances for turing.tape

turing.tape.has_sizeof_inst
turing.tape.inhabited

@[protected, instance]

def turing.tape.inhabited {Γ : Type u_1} [inhabited Γ] :

inhabited (turing.tape Γ)

Equations

turing.tape.inhabited = {default := {head := inhabited.default _inst_1, left := inhabited.default turing.list_blank.inhabited, right := inhabited.default turing.list_blank.inhabited}}

@[protected, instance]

def turing.dir.inhabited :

inhabited turing.dir

@[protected, instance]

def turing.dir.decidable_eq :

decidable_eq turing.dir

inductive turing.dir :

left : turing.dir
right : turing.dir

A direction for the turing machine move command, either left or right.

Instances for turing.dir

turing.dir.has_sizeof_inst
turing.dir.inhabited

def turing.tape.left₀ {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

turing.list_blank Γ

The "inclusive" left side of the tape, including both left and head.

Equations

T.left₀ = turing.list_blank.cons T.head T.left

def turing.tape.right₀ {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

turing.list_blank Γ

The "inclusive" right side of the tape, including both right and head.

Equations

T.right₀ = turing.list_blank.cons T.head T.right

def turing.tape.move {Γ : Type u_1} [inhabited Γ] :

turing.dir → turing.tape Γ → turing.tape Γ

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}

@[simp]

theorem turing.tape.move_left_right {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

turing.tape.move turing.dir.right (turing.tape.move turing.dir.left T) = T

@[simp]

theorem turing.tape.move_right_left {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

turing.tape.move turing.dir.left (turing.tape.move turing.dir.right T) = T

def turing.tape.mk' {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) :

Construct a tape from a left side and an inclusive right side.

Equations

turing.tape.mk' L R = {head := R.head, left := L, right := R.tail}

@[simp]

theorem turing.tape.mk'_left {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) :

(turing.tape.mk' L R).left = L

@[simp]

theorem turing.tape.mk'_head {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) :

(turing.tape.mk' L R).head = R.head

@[simp]

theorem turing.tape.mk'_right {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) :

(turing.tape.mk' L R).right = R.tail

@[simp]

theorem turing.tape.mk'_right₀ {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) :

(turing.tape.mk' L R).right₀ = R

@[simp]

theorem turing.tape.mk'_left_right₀ {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

turing.tape.mk' T.left T.right₀ = T

theorem turing.tape.exists_mk' {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

∃ (L R : turing.list_blank Γ), T = turing.tape.mk' L R

@[simp]

theorem turing.tape.move_left_mk' {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) :

turing.tape.move turing.dir.left (turing.tape.mk' L R) = turing.tape.mk' L.tail (turing.list_blank.cons L.head R)

@[simp]

theorem turing.tape.move_right_mk' {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) :

turing.tape.move turing.dir.right (turing.tape.mk' L R) = turing.tape.mk' (turing.list_blank.cons R.head L) R.tail

def turing.tape.mk₂ {Γ : Type u_1} [inhabited Γ] (L R : list Γ) :

Construct a tape from a left side and an inclusive right side.

Equations

turing.tape.mk₂ L R = turing.tape.mk' (turing.list_blank.mk L) (turing.list_blank.mk R)

def turing.tape.mk₁ {Γ : Type u_1} [inhabited Γ] (l : list Γ) :

Construct a tape from a list, with the head of the list at the TM head and the rest going to the right.

Equations

turing.tape.mk₁ l = turing.tape.mk₂ list.nil l

def turing.tape.nth {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

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.)

Equations

T.nth -[1+ n] = T.left.nth n
T.nth ↑(n + 1) = T.right.nth n
T.nth 0 = T.head

@[simp]

theorem turing.tape.nth_zero {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

T.nth 0 = T.head

theorem turing.tape.right₀_nth {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) (n : ℕ) :

T.right₀.nth n = T.nth ↑n

@[simp]

theorem turing.tape.mk'_nth_nat {Γ : Type u_1} [inhabited Γ] (L R : turing.list_blank Γ) (n : ℕ) :

(turing.tape.mk' L R).nth ↑n = R.nth n

@[simp]

theorem turing.tape.move_left_nth {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) (i : ℤ) :

(turing.tape.move turing.dir.left T).nth i = T.nth (i - 1)

@[simp]

theorem turing.tape.move_right_nth {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) (i : ℤ) :

(turing.tape.move turing.dir.right T).nth i = T.nth (i + 1)

@[simp]

theorem turing.tape.move_right_n_head {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) (i : ℕ) :

(turing.tape.move turing.dir.right^[i] T).head = T.nth ↑i

def turing.tape.write {Γ : Type u_1} [inhabited Γ] (b : Γ) (T : turing.tape Γ) :

Replace the current value of the head on the tape.

Equations

turing.tape.write b T = {head := b, left := T.left, right := T.right}

@[simp]

theorem turing.tape.write_self {Γ : Type u_1} [inhabited Γ] (T : turing.tape Γ) :

turing.tape.write T.head T = T

@[simp]

theorem turing.tape.write_nth {Γ : Type u_1} [inhabited Γ] (b : Γ) (T : turing.tape Γ) {i : ℤ} :

(turing.tape.write b T).nth i = ite (i = 0) b (T.nth i)

@[simp]

theorem turing.tape.write_mk' {Γ : Type u_1} [inhabited Γ] (a b : Γ) (L R : turing.list_blank Γ) :

turing.tape.write b (turing.tape.mk' L (turing.list_blank.cons a R)) = turing.tape.mk' L (turing.list_blank.cons b R)

def turing.tape.map {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (T : turing.tape Γ) :

turing.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}

@[simp]

theorem turing.tape.map_fst {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (T : turing.tape Γ) :

(turing.tape.map f T).head = ⇑f T.head

@[simp]

theorem turing.tape.map_write {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (b : Γ) (T : turing.tape Γ) :

turing.tape.map f (turing.tape.write b T) = turing.tape.write (⇑f b) (turing.tape.map f T)

@[simp]

theorem turing.tape.write_move_right_n {Γ : Type u_1} [inhabited Γ] (f : Γ → Γ) (L R : turing.list_blank Γ) (n : ℕ) :

turing.tape.write (f (R.nth n)) (turing.tape.move turing.dir.right^[n] (turing.tape.mk' L R)) = turing.tape.move turing.dir.right^[n] (turing.tape.mk' L (turing.list_blank.modify_nth f n R))

theorem turing.tape.map_move {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (T : turing.tape Γ) (d : turing.dir) :

turing.tape.map f (turing.tape.move d T) = turing.tape.move d (turing.tape.map f T)

theorem turing.tape.map_mk' {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (L R : turing.list_blank Γ) :

turing.tape.map f (turing.tape.mk' L R) = turing.tape.mk' (turing.list_blank.map f L) (turing.list_blank.map f R)

theorem turing.tape.map_mk₂ {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (L R : list Γ) :

turing.tape.map f (turing.tape.mk₂ L R) = turing.tape.mk₂ (list.map ⇑f L) (list.map ⇑f R)

theorem turing.tape.map_mk₁ {Γ : Type u_1} {Γ' : Type u_2} [inhabited Γ] [inhabited Γ'] (f : turing.pointed_map Γ Γ') (l : list Γ) :

turing.tape.map f (turing.tape.mk₁ l) = turing.tape.mk₁ (list.map ⇑f l)

def turing.eval {σ : Type u_1} (f : σ → option σ) :

σ → part σ

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 part.none.

Equations

turing.eval f = pfun.fix (λ (s : σ), part.some (option.elim (sum.inl s) sum.inr (f s)))

def turing.reaches {σ : Type u_1} (f : σ → option σ) :

σ → σ → Prop

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)

def turing.reaches₁ {σ : Type u_1} (f : σ → option σ) :

σ → σ → Prop

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)

theorem turing.reaches₁_eq {σ : Type u_1} {f : σ → option σ} {a b c : σ} (h : f a = f b) :

turing.reaches₁ f a c ↔ turing.reaches₁ f b c

theorem turing.reaches_total {σ : Type u_1} {f : σ → option σ} {a b c : σ} (hab : turing.reaches f a b) (hac : turing.reaches f a c) :

turing.reaches f b c ∨ turing.reaches f c b

theorem turing.reaches₁_fwd {σ : Type u_1} {f : σ → option σ} {a b c : σ} (h₁ : turing.reaches₁ f a c) (h₂ : b ∈ f a) :

turing.reaches f b c

def turing.reaches₀ {σ : Type u_1} (f : σ → option σ) (a b : σ) :

Prop

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

theorem turing.reaches₀.trans {σ : Type u_1} {f : σ → option σ} {a b c : σ} (h₁ : turing.reaches₀ f a b) (h₂ : turing.reaches₀ f b c) :

turing.reaches₀ f a c

@[refl]

theorem turing.reaches₀.refl {σ : Type u_1} {f : σ → option σ} (a : σ) :

turing.reaches₀ f a a

theorem turing.reaches₀.single {σ : Type u_1} {f : σ → option σ} {a b : σ} (h : b ∈ f a) :

turing.reaches₀ f a b

theorem turing.reaches₀.head {σ : Type u_1} {f : σ → option σ} {a b c : σ} (h : b ∈ f a) (h₂ : turing.reaches₀ f b c) :

turing.reaches₀ f a c

theorem turing.reaches₀.tail {σ : Type u_1} {f : σ → option σ} {a b c : σ} (h₁ : turing.reaches₀ f a b) (h : c ∈ f b) :

turing.reaches₀ f a c

theorem turing.reaches₀_eq {σ : Type u_1} {f : σ → option σ} {a b : σ} (e : f a = f b) :

turing.reaches₀ f a b

theorem turing.reaches₁.to₀ {σ : Type u_1} {f : σ → option σ} {a b : σ} (h : turing.reaches₁ f a b) :

turing.reaches₀ f a b

theorem turing.reaches.to₀ {σ : Type u_1} {f : σ → option σ} {a b : σ} (h : turing.reaches f a b) :

turing.reaches₀ f a b

theorem turing.reaches₀.tail' {σ : Type u_1} {f : σ → option σ} {a b c : σ} (h : turing.reaches₀ f a b) (h₂ : c ∈ f b) :

turing.reaches₁ f a c

def turing.eval_induction {σ : Type u_1} {f : σ → option σ} {b : σ} {C : σ → Sort u_2} {a : σ} (h : b ∈ turing.eval f a) (H : Π (a : σ), b ∈ turing.eval f a → (Π (a' : σ), f a = option.some a' → C a') → C a) :

C a

(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 : σ), part.some (option.elim (sum.inl s) sum.inr (f s))) a') (h' : Π (a'' : σ), sum.inr a'' ∈ part.some (option.elim (sum.inl a') sum.inr (f a')) → C a''), H a' ha' (λ (b' : σ) (e : f a' = option.some b'), h' b' _))

theorem turing.mem_eval {σ : Type u_1} {f : σ → option σ} {a b : σ} :

b ∈ turing.eval f a ↔ turing.reaches f a b ∧ f b = option.none

theorem turing.eval_maximal₁ {σ : Type u_1} {f : σ → option σ} {a b : σ} (h : b ∈ turing.eval f a) (c : σ) :

¬turing.reaches₁ f b c

theorem turing.eval_maximal {σ : Type u_1} {f : σ → option σ} {a b : σ} (h : b ∈ turing.eval f a) {c : σ} :

turing.reaches f b c ↔ c = b

theorem turing.reaches_eval {σ : Type u_1} {f : σ → option σ} {a b : σ} (ab : turing.reaches f a b) :

turing.eval f a = turing.eval f b

def turing.respects {σ₁ : Type u_1} {σ₂ : Type u_2} (f₁ : σ₁ → option σ₁) (f₂ : σ₂ → option σ₂) (tr : σ₁ → σ₂ → Prop) :

Prop

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)

theorem turing.tr_reaches₁ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → option σ₁} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂ → Prop} (H : turing.respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) {b₁ : σ₁} (ab : turing.reaches₁ f₁ a₁ b₁) :

∃ (b₂ : σ₂), tr b₁ b₂ ∧ turing.reaches₁ f₂ a₂ b₂

theorem turing.tr_reaches {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → option σ₁} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂ → Prop} (H : turing.respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) {b₁ : σ₁} (ab : turing.reaches f₁ a₁ b₁) :

∃ (b₂ : σ₂), tr b₁ b₂ ∧ turing.reaches f₂ a₂ b₂

theorem turing.tr_reaches_rev {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → option σ₁} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂ → Prop} (H : turing.respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) {b₂ : σ₂} (ab : turing.reaches f₂ a₂ b₂) :

∃ (c₁ : σ₁) (c₂ : σ₂), turing.reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ turing.reaches f₁ a₁ c₁

theorem turing.tr_eval {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → option σ₁} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂ → Prop} (H : turing.respects f₁ f₂ tr) {a₁ b₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) (ab : b₁ ∈ turing.eval f₁ a₁) :

∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ turing.eval f₂ a₂

theorem turing.tr_eval_rev {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → option σ₁} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂ → Prop} (H : turing.respects f₁ f₂ tr) {a₁ : σ₁} {b₂ a₂ : σ₂} (aa : tr a₁ a₂) (ab : b₂ ∈ turing.eval f₂ a₂) :

∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ turing.eval f₁ a₁

theorem turing.tr_eval_dom {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → option σ₁} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂ → Prop} (H : turing.respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) :

(turing.eval f₂ a₂).dom ↔ (turing.eval f₁ a₁).dom

def turing.frespects {σ₁ : Type u_1} {σ₂ : Type u_2} (f₂ : σ₂ → option σ₂) (tr : σ₁ → σ₂) (a₂ : σ₂) :

option σ₁ → Prop

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)

theorem turing.frespects_eq {σ₁ : Type u_1} {σ₂ : Type u_2} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂} {a₂ b₂ : σ₂} (h : f₂ a₂ = f₂ b₂) {b₁ : option σ₁} :

turing.frespects f₂ tr a₂ b₁ ↔ turing.frespects f₂ tr b₂ b₁

theorem turing.fun_respects {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → option σ₁} {f₂ : σ₂ → option σ₂} {tr : σ₁ → σ₂} :

turing.respects f₁ f₂ (λ (a : σ₁) (b : σ₂), tr a = b) ↔ ∀ ⦃a₁ : σ₁⦄, turing.frespects f₂ tr (tr a₁) (f₁ a₁)

theorem turing.tr_eval' {σ₁ σ₂ : Type u_1} (f₁ : σ₁ → option σ₁) (f₂ : σ₂ → option σ₂) (tr : σ₁ → σ₂) (H : turing.respects f₁ f₂ (λ (a : σ₁) (b : σ₂), tr a = b)) (a₁ : σ₁) :

turing.eval f₂ (tr a₁) = tr <$> turing.eval f₁ a₁

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 action s : stmt and then transitions to state q'.

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.)

inductive turing.TM0.stmt (Γ : Type u_1) [inhabited Γ] :

Type u_1

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.

Instances for turing.TM0.stmt

turing.TM0.stmt.has_sizeof_inst
turing.TM0.stmt.inhabited

@[protected, instance]

def turing.TM0.stmt.inhabited (Γ : Type u_1) [inhabited Γ] :

inhabited (turing.TM0.stmt Γ)

Equations

turing.TM0.stmt.inhabited Γ = {default := turing.TM0.stmt.write inhabited.default}

@[nolint]

def turing.TM0.machine (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) [inhabited Λ] :

Type (max u_2 u_1)

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 Γ))

Instances for turing.TM0.machine

turing.TM0.machine.inhabited

@[protected, instance]

def turing.TM0.machine.inhabited (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) [inhabited Λ] :

inhabited (turing.TM0.machine Γ Λ)

Equations

turing.TM0.machine.inhabited Γ Λ = _.mpr (pi.inhabited Λ)

structure turing.TM0.cfg (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) [inhabited Λ] :

Type (max u_1 u_2)

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.

Instances for turing.TM0.cfg

turing.TM0.cfg.has_sizeof_inst
turing.TM0.cfg.inhabited

@[protected, instance]

def turing.TM0.cfg.inhabited (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) [inhabited Λ] :

inhabited (turing.TM0.cfg Γ Λ)

Equations

turing.TM0.cfg.inhabited Γ Λ = {default := {q := inhabited.default _inst_2, tape := inhabited.default turing.tape.inhabited}}

def turing.TM0.step {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) :

turing.TM0.cfg Γ Λ → option (turing.TM0.cfg Γ Λ)

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

def turing.TM0.reaches {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) :

turing.TM0.cfg Γ Λ → turing.TM0.cfg Γ Λ → Prop

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)

def turing.TM0.init {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (l : list Γ) :

turing.TM0.cfg Γ Λ

The initial configuration.

Equations

turing.TM0.init l = {q := inhabited.default _inst_2, tape := turing.tape.mk₁ l}

def turing.TM0.eval {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) (l : list Γ) :

part (turing.list_blank Γ)

Evaluate a Turing machine on initial input to a final state, if it terminates.

Equations

turing.TM0.eval M l = part.map (λ (c : turing.TM0.cfg Γ Λ), c.tape.right₀) (turing.eval (turing.TM0.step M) (turing.TM0.init l))

def turing.TM0.supports {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) (S : set Λ) :

Prop

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)

theorem turing.TM0.step_supports {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) {S : set Λ} (ss : turing.TM0.supports M S) {c c' : turing.TM0.cfg Γ Λ} :

c' ∈ turing.TM0.step M c → c.q ∈ S → c'.q ∈ S

theorem turing.TM0.univ_supports {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) :

turing.TM0.supports M set.univ

def turing.TM0.stmt.map {Γ : Type u_1} [inhabited Γ] {Γ' : Type u_2} [inhabited Γ'] (f : turing.pointed_map Γ Γ') :

turing.TM0.stmt Γ → turing.TM0.stmt Γ'

Map a TM statement across a function. This does nothing to move statements and maps the write values.

Equations

turing.TM0.stmt.map f (turing.TM0.stmt.write a) = turing.TM0.stmt.write (⇑f a)
turing.TM0.stmt.map f (turing.TM0.stmt.move d) = turing.TM0.stmt.move d

def turing.TM0.cfg.map {Γ : Type u_1} [inhabited Γ] {Γ' : Type u_2} [inhabited Γ'] {Λ : Type u_3} [inhabited Λ] {Λ' : Type u_4} [inhabited Λ'] (f : turing.pointed_map Γ Γ') (g : Λ → Λ') :

turing.TM0.cfg Γ Λ → turing.TM0.cfg Γ' Λ'

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}

def turing.TM0.machine.map {Γ : Type u_1} [inhabited Γ] {Γ' : Type u_2} [inhabited Γ'] {Λ : Type u_3} [inhabited Λ] {Λ' : Type u_4} [inhabited Λ'] (M : turing.TM0.machine Γ Λ) (f₁ : turing.pointed_map Γ Γ') (f₂ : turing.pointed_map Γ' Γ) (g₁ : Λ → Λ') (g₂ : Λ' → Λ) :

turing.TM0.machine Γ' Λ'

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))

theorem turing.TM0.machine.map_step {Γ : Type u_1} [inhabited Γ] {Γ' : Type u_2} [inhabited Γ'] {Λ : Type u_3} [inhabited Λ] {Λ' : Type u_4} [inhabited Λ'] (M : turing.TM0.machine Γ Λ) (f₁ : turing.pointed_map Γ Γ') (f₂ : turing.pointed_map Γ' Γ) (g₁ : Λ → Λ') (g₂ : Λ' → Λ) {S : set Λ} (f₂₁ : function.right_inverse ⇑f₁ ⇑f₂) (g₂₁ : ∀ (q : Λ), q ∈ S → g₂ (g₁ q) = q) (c : turing.TM0.cfg Γ Λ) :

c.q ∈ S → option.map (turing.TM0.cfg.map f₁ g₁) (turing.TM0.step M c) = turing.TM0.step (M.map f₁ f₂ g₁ g₂) (turing.TM0.cfg.map f₁ g₁ c)

theorem turing.TM0.map_init {Γ : Type u_1} [inhabited Γ] {Γ' : Type u_2} [inhabited Γ'] {Λ : Type u_3} [inhabited Λ] {Λ' : Type u_4} [inhabited Λ'] (f₁ : turing.pointed_map Γ Γ') (g₁ : turing.pointed_map Λ Λ') (l : list Γ) :

turing.TM0.cfg.map f₁ ⇑g₁ (turing.TM0.init l) = turing.TM0.init (list.map ⇑f₁ l)

theorem turing.TM0.machine.map_respects {Γ : Type u_1} [inhabited Γ] {Γ' : Type u_2} [inhabited Γ'] {Λ : Type u_3} [inhabited Λ] {Λ' : Type u_4} [inhabited Λ'] (M : turing.TM0.machine Γ Λ) (f₁ : turing.pointed_map Γ Γ') (f₂ : turing.pointed_map Γ' Γ) (g₁ : turing.pointed_map Λ Λ') (g₂ : Λ' → Λ) {S : set Λ} (ss : turing.TM0.supports M S) (f₂₁ : function.right_inverse ⇑f₁ ⇑f₂) (g₂₁ : ∀ (q : Λ), q ∈ S → g₂ (⇑g₁ q) = q) :

turing.respects (turing.TM0.step M) (turing.TM0.step (M.map f₁ f₂ ⇑g₁ g₂)) (λ (a : turing.TM0.cfg Γ Λ) (b : turing.TM0.cfg Γ' Λ'), a.q ∈ S ∧ turing.TM0.cfg.map f₁ ⇑g₁ a = b)

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 do q
write (f : Γ → σ → Γ) q: write f a T.head to the tape, then do q
load (f : Γ → σ → σ) q: change the internal state to f a T.head
branch (f : Γ → σ → bool) qtrue qfalse: If f a T.head is true, do qtrue, else qfalse
goto (f : Γ → σ → Λ): Go to label f a T.head
halt: 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.

inductive turing.TM1.stmt (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) (σ : Type u_3) :

Type (max u_1 u_2 u_3)

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.

Instances for turing.TM1.stmt

turing.TM1.stmt.has_sizeof_inst
turing.TM1.stmt.inhabited

@[protected, instance]

def turing.TM1.stmt.inhabited (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) (σ : Type u_3) :

inhabited (turing.TM1.stmt Γ Λ σ)

Equations

turing.TM1.stmt.inhabited Γ Λ σ = {default := turing.TM1.stmt.halt σ}

structure turing.TM1.cfg (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) (σ : Type u_3) :

Type (max u_1 u_2 u_3)

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.

Instances for turing.TM1.cfg

turing.TM1.cfg.has_sizeof_inst
turing.TM1.cfg.inhabited

@[protected, instance]

def turing.TM1.cfg.inhabited (Γ : Type u_1) [inhabited Γ] (Λ : Type u_2) (σ : Type u_3) [inhabited σ] :

inhabited (turing.TM1.cfg Γ Λ σ)

Equations

turing.TM1.cfg.inhabited Γ Λ σ = {default := {l := inhabited.default (option.inhabited Λ), var := inhabited.default _inst_2, tape := inhabited.default turing.tape.inhabited}}

def turing.TM1.step_aux {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} :

turing.TM1.stmt Γ Λ σ → σ → turing.tape Γ → turing.TM1.cfg Γ Λ σ

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)

def turing.TM1.step {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} (M : Λ → turing.TM1.stmt Γ Λ σ) :

turing.TM1.cfg Γ Λ σ → option (turing.TM1.cfg Γ Λ σ)

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

def turing.TM1.supports_stmt {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} (S : finset Λ) :

turing.TM1.stmt Γ Λ σ → Prop

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

noncomputable def turing.TM1.stmts₁ {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} :

turing.TM1.stmt Γ Λ σ → finset (turing.TM1.stmt Γ Λ σ)

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 ᾰ) = {turing.TM1.stmt.goto ᾰ}
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)

theorem turing.TM1.stmts₁_self {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} {q : turing.TM1.stmt Γ Λ σ} :

q ∈ turing.TM1.stmts₁ q

theorem turing.TM1.stmts₁_trans {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} {q₁ q₂ : turing.TM1.stmt Γ Λ σ} :

q₁ ∈ turing.TM1.stmts₁ q₂ → turing.TM1.stmts₁ q₁ ⊆ turing.TM1.stmts₁ q₂

theorem turing.TM1.stmts₁_supports_stmt_mono {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} {S : finset Λ} {q₁ q₂ : turing.TM1.stmt Γ Λ σ} (h : q₁ ∈ turing.TM1.stmts₁ q₂) (hs : turing.TM1.supports_stmt S q₂) :

turing.TM1.supports_stmt S q₁

noncomputable def turing.TM1.stmts {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} (M : Λ → turing.TM1.stmt Γ Λ σ) (S : finset Λ) :

finset (option (turing.TM1.stmt Γ Λ σ))

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 = ⇑finset.insert_none (S.bUnion (λ (q : Λ), turing.TM1.stmts₁ (M q)))

theorem turing.TM1.stmts_trans {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} {M : Λ → turing.TM1.stmt Γ Λ σ} {S : finset Λ} {q₁ q₂ : turing.TM1.stmt Γ Λ σ} (h₁ : q₁ ∈ turing.TM1.stmts₁ q₂) :

option.some q₂ ∈ turing.TM1.stmts M S → option.some q₁ ∈ turing.TM1.stmts M S

def turing.TM1.supports {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} [inhabited Λ] (M : Λ → turing.TM1.stmt Γ Λ σ) (S : finset Λ) :

Prop

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))

theorem turing.TM1.stmts_supports_stmt {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} [inhabited Λ] {M : Λ → turing.TM1.stmt Γ Λ σ} {S : finset Λ} {q : turing.TM1.stmt Γ Λ σ} (ss : turing.TM1.supports M S) :

option.some q ∈ turing.TM1.stmts M S → turing.TM1.supports_stmt S q

theorem turing.TM1.step_supports {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} [inhabited Λ] (M : Λ → turing.TM1.stmt Γ Λ σ) {S : finset Λ} (ss : turing.TM1.supports M S) {c c' : turing.TM1.cfg Γ Λ σ} :

c' ∈ turing.TM1.step M c → c.l ∈ ⇑finset.insert_none S → c'.l ∈ ⇑finset.insert_none S

def turing.TM1.init {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} [inhabited Λ] [inhabited σ] (l : list Γ) :

turing.TM1.cfg Γ Λ σ

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}

def turing.TM1.eval {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} {σ : Type u_3} [inhabited Λ] [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) (l : list Γ) :

part (turing.list_blank Γ)

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 = part.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 be option stmt₁ × σ, that is, a TM1 statement or none representing halt, and the possible settings of the internal variables. Note that this is an infinite set, because stmt₁ 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.

@[nolint]

def turing.TM1to0.Λ' {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) :

Type (max (max u_1 u_2 u_3) u_3)

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 Γ Λ σ) × σ)

Instances for turing.TM1to0.Λ'

turing.TM1to0.Λ'.inhabited

@[protected, instance]

def turing.TM1to0.Λ'.inhabited {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) :

inhabited (turing.TM1to0.Λ' M)

Equations

turing.TM1to0.Λ'.inhabited M = {default := (option.some (M inhabited.default), inhabited.default _inst_3)}

def turing.TM1to0.tr_aux {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) (s : Γ) :

turing.TM1.stmt Γ Λ σ → σ → turing.TM1to0.Λ' M × turing.TM0.stmt Γ

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)

def turing.TM1to0.tr {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) :

turing.TM0.machine Γ (turing.TM1to0.Λ' M)

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

def turing.TM1to0.tr_cfg {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) :

turing.TM1.cfg Γ Λ σ → turing.TM0.cfg Γ (turing.TM1to0.Λ' M)

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}

theorem turing.TM1to0.tr_respects {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) :

turing.respects (turing.TM1.step M) (turing.TM0.step (turing.TM1to0.tr M)) (λ (c₁ : turing.TM1.cfg Γ Λ σ) (c₂ : turing.TM0.cfg Γ (turing.TM1to0.Λ' M)), turing.TM1to0.tr_cfg M c₁ = c₂)

theorem turing.TM1to0.tr_eval {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) (l : list Γ) :

turing.TM0.eval (turing.TM1to0.tr M) l = turing.TM1.eval M l

noncomputable def turing.TM1to0.tr_stmts {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) [fintype σ] (S : finset Λ) :

finset (turing.TM1to0.Λ' M)

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

turing.TM1to0.tr_stmts M S = turing.TM1.stmts M S ×ˢ finset.univ

theorem turing.TM1to0.tr_supports {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) [fintype σ] {S : finset Λ} (ss : turing.TM1.supports M S) :

turing.TM0.supports (turing.TM1to0.tr M) ↑(turing.TM1to0.tr_stmts M S)

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.

theorem turing.TM1to1.exists_enc_dec {Γ : Type u_1} [inhabited Γ] [fintype Γ] :

∃ (n : ℕ) (enc : Γ → vector bool n) (dec : vector bool n → Γ), enc inhabited.default = vector.replicate n bool.ff ∧ ∀ (a : Γ), dec (enc a) = a

inductive turing.TM1to1.Λ' {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] :

Type (max u_1 u_2 u_3)

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.

Instances for turing.TM1to1.Λ'

turing.TM1to1.Λ'.has_sizeof_inst
turing.TM1to1.Λ'.inhabited

@[protected, instance]

def turing.TM1to1.Λ'.inhabited {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] :

inhabited turing.TM1to1.Λ'

Equations

turing.TM1to1.Λ'.inhabited = {default := turing.TM1to1.Λ'.normal inhabited.default}

def turing.TM1to1.read_aux {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (n : ℕ) :

(vector bool n → turing.TM1.stmt bool turing.TM1to1.Λ' σ) → turing.TM1.stmt bool turing.TM1to1.Λ' σ

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

def turing.TM1to1.move {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} (d : turing.dir) (q : turing.TM1.stmt bool turing.TM1to1.Λ' σ) :

turing.TM1.stmt bool turing.TM1to1.Λ' σ

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

def turing.TM1to1.read {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} (dec : vector bool n → Γ) (f : Γ → turing.TM1.stmt bool turing.TM1to1.Λ' σ) :

turing.TM1.stmt bool turing.TM1to1.Λ' σ

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)))

def turing.TM1to1.write {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] :

list bool → turing.TM1.stmt bool turing.TM1to1.Λ' σ → turing.TM1.stmt bool turing.TM1to1.Λ' σ

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

def turing.TM1to1.tr_normal {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} (dec : vector bool n → Γ) :

turing.TM1.stmt Γ Λ σ → turing.TM1.stmt bool turing.TM1to1.Λ' σ

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)

theorem turing.TM1to1.step_aux_move {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} (d : turing.dir) (q : turing.TM1.stmt bool turing.TM1to1.Λ' σ) (v : σ) (T : turing.tape bool) :

turing.TM1.step_aux (turing.TM1to1.move d q) v T = turing.TM1.step_aux q v (turing.tape.move d^[n] T)

theorem turing.TM1to1.supports_stmt_move {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} {S : finset turing.TM1to1.Λ'} {d : turing.dir} {q : turing.TM1.stmt bool turing.TM1to1.Λ' σ} :

turing.TM1.supports_stmt S (turing.TM1to1.move d q) = turing.TM1.supports_stmt S q

theorem turing.TM1to1.supports_stmt_write {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {S : finset turing.TM1to1.Λ'} {l : list bool} {q : turing.TM1.stmt bool turing.TM1to1.Λ' σ} :

turing.TM1.supports_stmt S (turing.TM1to1.write l q) = turing.TM1.supports_stmt S q

theorem turing.TM1to1.supports_stmt_read {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} (dec : vector bool n → Γ) {S : finset turing.TM1to1.Λ'} {f : Γ → turing.TM1.stmt bool turing.TM1to1.Λ' σ} :

(∀ (a : Γ), turing.TM1.supports_stmt S (f a)) → turing.TM1.supports_stmt S (turing.TM1to1.read dec f)

def turing.TM1to1.tr_tape' {Γ : Type u_1} [inhabited Γ] {n : ℕ} {enc : Γ → vector bool n} (enc0 : enc inhabited.default = vector.replicate n bool.ff) (L R : turing.list_blank Γ) :

turing.tape bool

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) _)

def turing.TM1to1.tr_tape {Γ : Type u_1} [inhabited Γ] {n : ℕ} {enc : Γ → vector bool n} (enc0 : enc inhabited.default = vector.replicate n bool.ff) (T : turing.tape Γ) :

turing.tape bool

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₀

theorem turing.TM1to1.tr_tape_mk' {Γ : Type u_1} [inhabited Γ] {n : ℕ} {enc : Γ → vector bool n} (enc0 : enc inhabited.default = vector.replicate n bool.ff) (L R : turing.list_blank Γ) :

turing.TM1to1.tr_tape enc0 (turing.tape.mk' L R) = turing.TM1to1.tr_tape' enc0 L R

def turing.TM1to1.tr {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} (enc : Γ → vector bool n) (dec : vector bool n → Γ) (M : Λ → turing.TM1.stmt Γ Λ σ) :

turing.TM1to1.Λ' → turing.TM1.stmt bool turing.TM1to1.Λ' σ

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)

def turing.TM1to1.tr_cfg {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} {enc : Γ → vector bool n} (enc0 : enc inhabited.default = vector.replicate n bool.ff) :

turing.TM1.cfg Γ Λ σ → turing.TM1.cfg bool turing.TM1to1.Λ' σ

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}

theorem turing.TM1to1.tr_tape'_move_left {Γ : Type u_1} [inhabited Γ] {n : ℕ} {enc : Γ → vector bool n} (enc0 : enc inhabited.default = vector.replicate n bool.ff) (L R : turing.list_blank Γ) :

turing.tape.move turing.dir.left^[n] (turing.TM1to1.tr_tape' enc0 L R) = turing.TM1to1.tr_tape' enc0 L.tail (turing.list_blank.cons L.head R)

theorem turing.TM1to1.tr_tape'_move_right {Γ : Type u_1} [inhabited Γ] {n : ℕ} {enc : Γ → vector bool n} (enc0 : enc inhabited.default = vector.replicate n bool.ff) (L R : turing.list_blank Γ) :

turing.tape.move turing.dir.right^[n] (turing.TM1to1.tr_tape' enc0 L R) = turing.TM1to1.tr_tape' enc0 (turing.list_blank.cons R.head L) R.tail

theorem turing.TM1to1.step_aux_write {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} {enc : Γ → vector bool n} (enc0 : enc inhabited.default = vector.replicate n bool.ff) (q : turing.TM1.stmt bool turing.TM1to1.Λ' σ) (v : σ) (a b : Γ) (L R : turing.list_blank Γ) :

turing.TM1.step_aux (turing.TM1to1.write (enc a).to_list q) v (turing.TM1to1.tr_tape' enc0 L (turing.list_blank.cons b R)) = turing.TM1.step_aux q v (turing.TM1to1.tr_tape' enc0 (turing.list_blank.cons a L) R)

theorem turing.TM1to1.step_aux_read {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} {enc : Γ → vector bool n} (dec : vector bool n → Γ) (enc0 : enc inhabited.default = vector.replicate n bool.ff) (encdec : ∀ (a : Γ), dec (enc a) = a) (f : Γ → turing.TM1.stmt bool turing.TM1to1.Λ' σ) (v : σ) (L R : turing.list_blank Γ) :

turing.TM1.step_aux (turing.TM1to1.read dec f) v (turing.TM1to1.tr_tape' enc0 L R) = turing.TM1.step_aux (f R.head) v (turing.TM1to1.tr_tape' enc0 L R)

theorem turing.TM1to1.tr_respects {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} {enc : Γ → vector bool n} (dec : vector bool n → Γ) (enc0 : enc inhabited.default = vector.replicate n bool.ff) (M : Λ → turing.TM1.stmt Γ Λ σ) (encdec : ∀ (a : Γ), dec (enc a) = a) :

turing.respects (turing.TM1.step M) (turing.TM1.step (turing.TM1to1.tr enc dec M)) (λ (c₁ : turing.TM1.cfg Γ Λ σ) (c₂ : turing.TM1.cfg bool turing.TM1to1.Λ' σ), turing.TM1to1.tr_cfg enc0 c₁ = c₂)

noncomputable def turing.TM1to1.writes {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] [fintype Γ] :

turing.TM1.stmt Γ Λ σ → finset turing.TM1to1.Λ'

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

noncomputable def turing.TM1to1.tr_supp {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] (M : Λ → turing.TM1.stmt Γ Λ σ) [fintype Γ] (S : finset Λ) :

finset turing.TM1to1.Λ'

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.bUnion (λ (l : Λ), has_insert.insert (turing.TM1to1.Λ'.normal l) (turing.TM1to1.writes (M l)))

theorem turing.TM1to1.tr_supports {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] {σ : Type u_3} [inhabited σ] {n : ℕ} {enc : Γ → vector bool n} (dec : vector bool n → Γ) (M : Λ → turing.TM1.stmt Γ Λ σ) [fintype Γ] {S : finset Λ} (ss : turing.TM1.supports M S) :

turing.TM1.supports (turing.TM1to1.tr enc dec M) (turing.TM1to1.tr_supp M S)

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).

inductive turing.TM0to1.Λ' {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] :

Type (max u_1 u_2)

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.

Instances for turing.TM0to1.Λ'

turing.TM0to1.Λ'.has_sizeof_inst
turing.TM0to1.Λ'.inhabited

@[protected, instance]

def turing.TM0to1.Λ'.inhabited {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] :

inhabited turing.TM0to1.Λ'

Equations

turing.TM0to1.Λ'.inhabited = {default := turing.TM0to1.Λ'.normal inhabited.default}

def turing.TM0to1.tr {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) :

turing.TM0to1.Λ' → turing.TM1.stmt Γ turing.TM0to1.Λ' unit

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

def turing.TM0to1.tr_cfg {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) :

turing.TM0.cfg Γ Λ → turing.TM1.cfg Γ turing.TM0to1.Λ' unit

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 := unit.star(), tape := T}

theorem turing.TM0to1.tr_respects {Γ : Type u_1} [inhabited Γ] {Λ : Type u_2} [inhabited Λ] (M : turing.TM0.machine Γ Λ) :

turing.respects (turing.TM0.step M) (turing.TM1.step (turing.TM0to1.tr M)) (λ (a : turing.TM0.cfg Γ Λ) (b : turing.TM1.cfg Γ turing.TM0to1.Λ' unit), turing.TM0to1.tr_cfg M a = b)

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 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.

inductive turing.TM2.stmt {K : Type u_1} [decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) :

Type (max u_1 u_2 u_3 u_4)

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.

Instances for turing.TM2.stmt

turing.TM2.stmt.has_sizeof_inst
turing.TM2.stmt.inhabited

@[protected, instance]

def turing.TM2.stmt.inhabited {K : Type u_1} [decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) :

inhabited (turing.TM2.stmt Γ Λ σ)

Equations

turing.TM2.stmt.inhabited Γ Λ σ = {default := turing.TM2.stmt.halt σ}

structure turing.TM2.cfg {K : Type u_1} [decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) :

Type (max u_1 u_2 u_3 u_4)

l : option Λ
var : σ
stk : Π (k : K), list (Γ k)

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.)

Instances for turing.TM2.cfg

turing.TM2.cfg.has_sizeof_inst
turing.TM2.cfg.inhabited

@[protected, instance]

def turing.TM2.cfg.inhabited {K : Type u_1} [decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) [inhabited σ] :

inhabited (turing.TM2.cfg Γ Λ σ)

Equations

turing.TM2.cfg.inhabited Γ Λ σ = {default := {l := inhabited.default (option.inhabited Λ), var := inhabited.default _inst_2, stk := inhabited.default (pi.inhabited K)}}

@[simp]

def turing.TM2.step_aux {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} :

turing.TM2.stmt Γ Λ σ → σ → (Π (k : K), list (Γ k)) → turing.TM2.cfg Γ Λ σ

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))

@[simp]

def turing.TM2.step {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (M : Λ → turing.TM2.stmt Γ Λ σ) :

turing.TM2.cfg Γ Λ σ → option (turing.TM2.cfg Γ Λ σ)

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

def turing.TM2.reaches {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (M : Λ → turing.TM2.stmt Γ Λ σ) :

turing.TM2.cfg Γ Λ σ → turing.TM2.cfg Γ Λ σ → Prop

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)

def turing.TM2.supports_stmt {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : finset Λ) :

turing.TM2.stmt Γ Λ σ → Prop

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

noncomputable def turing.TM2.stmts₁ {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} :

turing.TM2.stmt Γ Λ σ → finset (turing.TM2.stmt Γ Λ σ)

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)

theorem turing.TM2.stmts₁_self {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q : turing.TM2.stmt Γ Λ σ} :

q ∈ turing.TM2.stmts₁ q

theorem turing.TM2.stmts₁_trans {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q₁ q₂ : turing.TM2.stmt Γ Λ σ} :

q₁ ∈ turing.TM2.stmts₁ q₂ → turing.TM2.stmts₁ q₁ ⊆ turing.TM2.stmts₁ q₂

theorem turing.TM2.stmts₁_supports_stmt_mono {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {S : finset Λ} {q₁ q₂ : turing.TM2.stmt Γ Λ σ} (h : q₁ ∈ turing.TM2.stmts₁ q₂) (hs : turing.TM2.supports_stmt S q₂) :

turing.TM2.supports_stmt S q₁

noncomputable def turing.TM2.stmts {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (M : Λ → turing.TM2.stmt Γ Λ σ) (S : finset Λ) :

finset (option (turing.TM2.stmt Γ Λ σ))

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

Equations

turing.TM2.stmts M S = ⇑finset.insert_none (S.bUnion (λ (q : Λ), turing.TM2.stmts₁ (M q)))

theorem turing.TM2.stmts_trans {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {M : Λ → turing.TM2.stmt Γ Λ σ} {S : finset Λ} {q₁ q₂ : turing.TM2.stmt Γ Λ σ} (h₁ : q₁ ∈ turing.TM2.stmts₁ q₂) :

option.some q₂ ∈ turing.TM2.stmts M S → option.some q₁ ∈ turing.TM2.stmts M S

def turing.TM2.supports {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inhabited Λ] (M : Λ → turing.TM2.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 = (inhabited.default ∈ S ∧ ∀ (q : Λ), q ∈ S → turing.TM2.supports_stmt S (M q))

theorem turing.TM2.stmts_supports_stmt {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inhabited Λ] {M : Λ → turing.TM2.stmt Γ Λ σ} {S : finset Λ} {q : turing.TM2.stmt Γ Λ σ} (ss : turing.TM2.supports M S) :

option.some q ∈ turing.TM2.stmts M S → turing.TM2.supports_stmt S q

theorem turing.TM2.step_supports {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inhabited Λ] (M : Λ → turing.TM2.stmt Γ Λ σ) {S : finset Λ} (ss : turing.TM2.supports M S) {c c' : turing.TM2.cfg Γ Λ σ} :

c' ∈ turing.TM2.step M c → c.l ∈ ⇑finset.insert_none S → c'.l ∈ ⇑finset.insert_none S

def turing.TM2.init {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inhabited Λ] [inhabited σ] (k : K) (L : list (Γ k)) :

turing.TM2.cfg Γ Λ σ

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}

def turing.TM2.eval {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inhabited Λ] [inhabited σ] (M : Λ → turing.TM2.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 (λ (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 : st_act 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 : turing.list_blank (Π (k : K), option (Γ k))} {k : K} {S : list (Γ k)} (n : ℕ) (hL : turing.list_blank.map (turing.proj k) L = turing.list_blank.mk (list.map option.some S).reverse) :

L.nth n k = S.reverse.nth n

@[nolint]

def turing.TM2to1.Γ' {K : Type u_1} [decidable_eq K] {Γ : 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.Γ' = (bool × Π (k : K), option (Γ k))

Instances for turing.TM2to1.Γ'

@[protected, instance]

def turing.TM2to1.Γ'.inhabited {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} :

inhabited turing.TM2to1.Γ'

Equations

turing.TM2to1.Γ'.inhabited = {default := (bool.ff, λ (_x : K), option.none)}

@[protected, instance]

def turing.TM2to1.Γ'.fintype {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} [fintype K] [Π (k : K), fintype (Γ k)] :

fintype turing.TM2to1.Γ'

Equations

turing.TM2to1.Γ'.fintype = prod.fintype bool (Π (k : K), option (Γ k))

def turing.TM2to1.add_bottom {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} (L : turing.list_blank (Π (k : K), option (Γ k))) :

turing.list_blank turing.TM2to1.Γ'

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)

theorem turing.TM2to1.add_bottom_map {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} (L : turing.list_blank (Π (k : K), option (Γ k))) :

turing.list_blank.map {f := prod.snd (Π (k : K), option (Γ k)), map_pt' := _} (turing.TM2to1.add_bottom L) = L

theorem turing.TM2to1.add_bottom_modify_nth {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} (f : (Π (k : K), option (Γ k)) → Π (k : K), option (Γ k)) (L : turing.list_blank (Π (k : K), option (Γ k))) (n : ℕ) :

turing.list_blank.modify_nth (λ (a : turing.TM2to1.Γ'), (a.fst, f a.snd)) n (turing.TM2to1.add_bottom L) = turing.TM2to1.add_bottom (turing.list_blank.modify_nth f n L)

theorem turing.TM2to1.add_bottom_nth_snd {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} (L : turing.list_blank (Π (k : K), option (Γ k))) (n : ℕ) :

((turing.TM2to1.add_bottom L).nth n).snd = L.nth n

theorem turing.TM2to1.add_bottom_nth_succ_fst {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} (L : turing.list_blank (Π (k : K), option (Γ k))) (n : ℕ) :

((turing.TM2to1.add_bottom L).nth (n + 1)).fst = bool.ff

theorem turing.TM2to1.add_bottom_head_fst {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} (L : turing.list_blank (Π (k : K), option (Γ k))) :

(turing.TM2to1.add_bottom L).head.fst = bool.tt

inductive turing.TM2to1.st_act {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {σ : Type u_4} [inhabited σ] (k : K) :

Type (max u_2 u_4)

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.

Instances for turing.TM2to1.st_act

turing.TM2to1.st_act.has_sizeof_inst
turing.TM2to1.st_act.inhabited

@[protected, instance]

def turing.TM2to1.st_act.inhabited {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {σ : Type u_4} [inhabited σ] {k : K} :

inhabited (turing.TM2to1.st_act k)

Equations

turing.TM2to1.st_act.inhabited = {default := turing.TM2to1.st_act.peek (λ (s : σ) (_x : option (Γ k)), s)}

@[nolint]

def turing.TM2to1.st_run {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] {k : K} :

turing.TM2to1.st_act k → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ

The TM2 statement corresponding to a stack action.

Equations

turing.TM2to1.st_run (turing.TM2to1.st_act.pop f) = turing.TM2.stmt.pop k f
turing.TM2to1.st_run (turing.TM2to1.st_act.peek f) = turing.TM2.stmt.peek k f
turing.TM2to1.st_run (turing.TM2to1.st_act.push f) = turing.TM2.stmt.push k f

def turing.TM2to1.st_var {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {σ : Type u_4} [inhabited σ] {k : K} (v : σ) (l : list (Γ k)) :

turing.TM2to1.st_act k → σ

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

def turing.TM2to1.st_write {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {σ : Type u_4} [inhabited σ] {k : K} (v : σ) (l : list (Γ k)) :

turing.TM2to1.st_act k → list (Γ k)

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

def turing.TM2to1.stmt_st_rec {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] {C : turing.TM2.stmt Γ Λ σ → Sort l} (H₁ : Π (k : K) (s : turing.TM2to1.st_act k) (q : turing.TM2.stmt Γ Λ σ), C q → C (turing.TM2to1.st_run s q)) (H₂ : Π (a : σ → σ) (q : turing.TM2.stmt Γ Λ σ), C q → C (turing.TM2.stmt.load a q)) (H₃ : Π (p : σ → bool) (q₁ q₂ : turing.TM2.stmt Γ Λ σ), C q₁ → C q₂ → C (turing.TM2.stmt.branch p q₁ q₂)) (H₄ : Π (l : σ → Λ), C (turing.TM2.stmt.goto l)) (H₅ : C turing.TM2.stmt.halt) (n : turing.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.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)

theorem turing.TM2to1.supports_run {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (S : finset Λ) {k : K} (s : turing.TM2to1.st_act k) (q : turing.TM2.stmt Γ Λ σ) :

turing.TM2.supports_stmt S (turing.TM2to1.st_run s q) ↔ turing.TM2.supports_stmt S q

inductive turing.TM2to1.Λ' {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] :

Type (max u_1 u_2 u_3 u_4)

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.

Instances for turing.TM2to1.Λ'

turing.TM2to1.Λ'.has_sizeof_inst
turing.TM2to1.Λ'.inhabited

@[protected, instance]

def turing.TM2to1.Λ'.inhabited {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] :

inhabited turing.TM2to1.Λ'

Equations

turing.TM2to1.Λ'.inhabited = {default := turing.TM2to1.Λ'.normal inhabited.default}

def turing.TM2to1.tr_st_act {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] {k : K} (q : turing.TM1.stmt turing.TM2to1.Γ' turing.TM2to1.Λ' σ) :

turing.TM2to1.st_act k → turing.TM1.stmt turing.TM2to1.Γ' turing.TM2to1.Λ' σ

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)

def turing.TM2to1.tr_init {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} (k : K) (L : list (Γ k)) :

list turing.TM2to1.Γ'

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

theorem turing.TM2to1.step_run {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] {k : K} (q : turing.TM2.stmt Γ Λ σ) (v : σ) (S : Π (k : K), list (Γ k)) (s : turing.TM2to1.st_act k) :

turing.TM2.step_aux (turing.TM2to1.st_run s q) v S = turing.TM2.step_aux q (turing.TM2to1.st_var v (S k) s) (function.update S k (turing.TM2to1.st_write v (S k) s))

def turing.TM2to1.tr_normal {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] :

turing.TM2.stmt Γ Λ σ → turing.TM1.stmt turing.TM2to1.Γ' turing.TM2to1.Λ' σ

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)

theorem turing.TM2to1.tr_normal_run {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] {k : K} (s : turing.TM2to1.st_act k) (q : turing.TM2.stmt Γ Λ σ) :

turing.TM2to1.tr_normal (turing.TM2to1.st_run s q) = turing.TM1.stmt.goto (λ (_x : turing.TM2to1.Γ') (_x : σ), turing.TM2to1.Λ'.go k s q)

noncomputable def turing.TM2to1.tr_stmts₁ {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] :

turing.TM2.stmt Γ Λ σ → finset turing.TM2to1.Λ'

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 ᾰ) = ∅
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

theorem turing.TM2to1.tr_stmts₁_run {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] {k : K} {s : turing.TM2to1.st_act k} {q : turing.TM2.stmt Γ Λ σ} :

turing.TM2to1.tr_stmts₁ (turing.TM2to1.st_run s q) = {turing.TM2to1.Λ'.go k s q, turing.TM2to1.Λ'.ret q} ∪ turing.TM2to1.tr_stmts₁ q

theorem turing.TM2to1.tr_respects_aux₂ {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] {k : K} {q : turing.TM1.stmt turing.TM2to1.Γ' turing.TM2to1.Λ' σ} {v : σ} {S : Π (k : K), list (Γ k)} {L : turing.list_blank (Π (k : K), option (Γ k))} (hL : ∀ (k : K), turing.list_blank.map (turing.proj k) L = turing.list_blank.mk (list.map option.some (S k)).reverse) (o : turing.TM2to1.st_act k) :

let v' : σ := turing.TM2to1.st_var v (S k) o, Sk' : list (Γ k) := turing.TM2to1.st_write v (S k) o, S' : Π (a : K), list (Γ a) := function.update S k Sk' in ∃ (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.TM1.step_aux (turing.TM2to1.tr_st_act q o) v (turing.tape.move turing.dir.right^[(S k).length] (turing.tape.mk' ∅ (turing.TM2to1.add_bottom L))) = turing.TM1.step_aux q v' (turing.tape.move turing.dir.right^[(S' k).length] (turing.tape.mk' ∅ (turing.TM2to1.add_bottom L')))

def turing.TM2to1.tr {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) :

turing.TM2to1.Λ' → turing.TM1.stmt turing.TM2to1.Γ' turing.TM2to1.Λ' σ

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)

inductive turing.TM2to1.tr_cfg {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) :

turing.TM2.cfg Γ Λ σ → turing.TM1.cfg turing.TM2to1.Γ' turing.TM2to1.Λ' σ → Prop

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.

theorem turing.TM2to1.tr_respects_aux₁ {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) {k : K} (o : turing.TM2to1.st_act k) (q : turing.TM2.stmt Γ Λ σ) (v : σ) {S : list (Γ k)} {L : turing.list_blank (Π (k : K), option (Γ k))} (hL : turing.list_blank.map (turing.proj k) L = turing.list_blank.mk (list.map option.some S).reverse) (n : ℕ) (H : n ≤ S.length) :

turing.reaches₀ (turing.TM1.step (turing.TM2to1.tr M)) {l := option.some (turing.TM2to1.Λ'.go k o q), var := v, tape := turing.tape.mk' ∅ (turing.TM2to1.add_bottom L)} {l := option.some (turing.TM2to1.Λ'.go k o q), var := v, tape := turing.tape.move turing.dir.right^[n] (turing.tape.mk' ∅ (turing.TM2to1.add_bottom L))}

theorem turing.TM2to1.tr_respects_aux₃ {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) {q : turing.TM2.stmt Γ Λ σ} {v : σ} {L : turing.list_blank (Π (k : K), option (Γ k))} (n : ℕ) :

turing.reaches₀ (turing.TM1.step (turing.TM2to1.tr M)) {l := option.some (turing.TM2to1.Λ'.ret q), var := v, tape := turing.tape.move turing.dir.right^[n] (turing.tape.mk' ∅ (turing.TM2to1.add_bottom L))} {l := option.some (turing.TM2to1.Λ'.ret q), var := v, tape := turing.tape.mk' ∅ (turing.TM2to1.add_bottom L)}

theorem turing.TM2to1.tr_respects_aux {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) {q : turing.TM2.stmt Γ Λ σ} {v : σ} {T : turing.list_blank (Π (i : K), option (Γ i))} {k : K} {S : Π (k : K), list (Γ k)} (hT : ∀ (k : K), turing.list_blank.map (turing.proj k) T = turing.list_blank.mk (list.map option.some (S k)).reverse) (o : turing.TM2to1.st_act k) (IH : ∀ {v : σ} {S : Π (k : K), list (Γ k)} {T : turing.list_blank (Π (k : K), option (Γ k))}, (∀ (k : K), turing.list_blank.map (turing.proj k) T = turing.list_blank.mk (list.map option.some (S k)).reverse) → (∃ (b : turing.TM1.cfg turing.TM2to1.Γ' turing.TM2to1.Λ' σ), turing.TM2to1.tr_cfg M (turing.TM2.step_aux q v S) b ∧ turing.reaches (turing.TM1.step (turing.TM2to1.tr M)) (turing.TM1.step_aux (turing.TM2to1.tr_normal q) v (turing.tape.mk' ∅ (turing.TM2to1.add_bottom T))) b)) :

∃ (b : turing.TM1.cfg turing.TM2to1.Γ' turing.TM2to1.Λ' σ), turing.TM2to1.tr_cfg M (turing.TM2.step_aux (turing.TM2to1.st_run o q) v S) b ∧ turing.reaches (turing.TM1.step (turing.TM2to1.tr M)) (turing.TM1.step_aux (turing.TM2to1.tr_normal (turing.TM2to1.st_run o q)) v (turing.tape.mk' ∅ (turing.TM2to1.add_bottom T))) b

theorem turing.TM2to1.tr_respects {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) :

turing.respects (turing.TM2.step M) (turing.TM1.step (turing.TM2to1.tr M)) (turing.TM2to1.tr_cfg M)

theorem turing.TM2to1.tr_cfg_init {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) (k : K) (L : list (Γ k)) :

turing.TM2to1.tr_cfg M (turing.TM2.init k L) (turing.TM1.init (turing.TM2to1.tr_init k L))

theorem turing.TM2to1.tr_eval_dom {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) (k : K) (L : list (Γ k)) :

(turing.TM1.eval (turing.TM2to1.tr M) (turing.TM2to1.tr_init k L)).dom ↔ (turing.TM2.eval M k L).dom

theorem turing.TM2to1.tr_eval {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) (k : K) (L : list (Γ k)) {L₁ : turing.list_blank turing.TM2to1.Γ'} {L₂ : list (Γ k)} (H₁ : L₁ ∈ turing.TM1.eval (turing.TM2to1.tr M) (turing.TM2to1.tr_init k L)) (H₂ : L₂ ∈ turing.TM2.eval M k L) :

∃ (S : Π (k : K), list (Γ k)) (L' : turing.list_blank (Π (k : K), option (Γ k))), turing.TM2to1.add_bottom L' = L₁ ∧ (∀ (k : K), turing.list_blank.map (turing.proj k) L' = turing.list_blank.mk (list.map option.some (S k)).reverse) ∧ S k = L₂

noncomputable def turing.TM2to1.tr_supp {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) (S : finset Λ) :

finset turing.TM2to1.Λ'

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

Equations

turing.TM2to1.tr_supp M S = S.bUnion (λ (l : Λ), has_insert.insert (turing.TM2to1.Λ'.normal l) (turing.TM2to1.tr_stmts₁ (M l)))

theorem turing.TM2to1.tr_supports {K : Type u_1} [decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [inhabited Λ] {σ : Type u_4} [inhabited σ] (M : Λ → turing.TM2.stmt Γ Λ σ) {S : finset Λ} (ss : turing.TM2.supports M S) :

turing.TM1.supports (turing.TM2to1.tr M) (turing.TM2to1.tr_supp M S)