Modelling partial recursive functions using Turing machines

This file defines a simplified basis for partial recursive functions, and a Turing.TM2 model Turing machine for evaluating these functions. This amounts to a constructive proof that every Partrec function can be evaluated by a Turing machine.

Main definitions

• ToPartrec.Code: a simplified basis for partial recursive functions, valued in List ℕ →. List ℕ.
  • ToPartrec.Code.eval: semantics for a ToPartrec.Code program
• PartrecToTM2.tr: A TM2 turing machine which can evaluate code programs

A simplified basis for partrec

This section constructs the type Code, which is a data type of programs with List ℕ input and output, with enough expressivity to write any partial recursive function. The primitives are:

• zero' appends a 0 to the input. That is, zero' v = 0 :: v.
• succ returns the successor of the head of the input, defaulting to zero if there is no head:
  • succ [] = [1]
  • succ (n :: v) = [n + 1]
• tail returns the tail of the input
  • tail [] = []
  • tail (n :: v) = v
• cons f fs calls f and fs on the input and conses the results:
  • cons f fs v = (f v).head :: fs v
• comp f g calls f on the output of g:
  • comp f g v = f (g v)
• case f g cases on the head of the input, calling f or g depending on whether it is zero or a successor (similar to Nat.casesOn).
  • case f g [] = f []
  • case f g (0 :: v) = f v
  • case f g (n+1 :: v) = g (n :: v)
• fix f calls f repeatedly, using the head of the result of f to decide whether to call f again or finish:
  • fix f v = [] if f v = []
  • fix f v = w if f v = 0 :: w
  • fix f v = fix f w if f v = n+1 :: w (the exact value of n is discarded)

This basis is convenient because it is closer to the Turing machine model - the key operations are splitting and merging of lists of unknown length, while the messy n-ary composition operation from the traditional basis for partial recursive functions is absent - but it retains a compositional semantics. The first step in transitioning to Turing machines is to make a sequential evaluator for this basis, which we take up in the next section.

inductive Turing.ToPartrec.Code : Type

The type of codes for primitive recursive functions. Unlike Nat.Partrec.Code, this uses a set of operations on List ℕ. See Code.eval for a description of the behavior of the primitives.

• zero' : Turing.ToPartrec.Code
• succ : Turing.ToPartrec.Code
• tail : Turing.ToPartrec.Code
• cons : Turing.ToPartrec.Code → Turing.ToPartrec.Code → Turing.ToPartrec.Code
• comp : Turing.ToPartrec.Code → Turing.ToPartrec.Code → Turing.ToPartrec.Code
• case : Turing.ToPartrec.Code → Turing.ToPartrec.Code → Turing.ToPartrec.Code
• fix : Turing.ToPartrec.Code → Turing.ToPartrec.Code

instance Turing.ToPartrec.instDecidableEqCode : DecidableEq Turing.ToPartrec.Code

Equations

• Turing.ToPartrec.instDecidableEqCode = Turing.ToPartrec.decEqCode✝

instance Turing.ToPartrec.instInhabitedCode : Inhabited Turing.ToPartrec.Code

Equations

• Turing.ToPartrec.instInhabitedCode = { default := Turing.ToPartrec.Code.zero' }

def Turing.ToPartrec.Code.eval : Turing.ToPartrec.Code → List ℕ →. List ℕ

The semantics of the Code primitives, as partial functions List ℕ →. List ℕ. By convention we functions that return a single result return a singleton [n], or in some cases n :: v where v will be ignored by a subsequent function.

• zero' appends a 0 to the input. That is, zero' v = 0 :: v.
• succ returns the successor of the head of the input, defaulting to zero if there is no head:
  • succ [] = [1]
  • succ (n :: v) = [n + 1]
• tail returns the tail of the input
  • tail [] = []
  • tail (n :: v) = v
• cons f fs calls f and fs on the input and conses the results:
  • cons f fs v = (f v).head :: fs v
• comp f g calls f on the output of g:
  • comp f g v = f (g v)
• case f g cases on the head of the input, calling f or g depending on whether it is zero or a successor (similar to Nat.casesOn).
  • case f g [] = f []
  • case f g (0 :: v) = f v
  • case f g (n+1 :: v) = g (n :: v)
• fix f calls f repeatedly, using the head of the result of f to decide whether to call f again or finish:
  • fix f v = [] if f v = []
  • fix f v = w if f v = 0 :: w
  • fix f v = fix f w if f v = n+1 :: w (the exact value of n is discarded)

Equations

• Turing.ToPartrec.Code.zero'.eval = fun (v : List ℕ) => pure (0 :: v)
• Turing.ToPartrec.Code.succ.eval = fun (v : List ℕ) => pure [v.headI.succ]
• Turing.ToPartrec.Code.tail.eval = fun (v : List ℕ) => pure v.tail
• (f.cons fs).eval = fun (v : List ℕ) => do let n ← f.eval v let ns ← fs.eval v pure (n.headI :: ns)
• (f.comp g).eval = fun (v : List ℕ) => g.eval v >>= f.eval
• (f.case g).eval = fun (v : List ℕ) => Nat.rec (f.eval v.tail) (fun (y : ℕ) (x : Part (List ℕ)) => g.eval (y :: v.tail)) v.headI
• f.fix.eval = PFun.fix fun (v : List ℕ) => Part.map (fun (v : List ℕ) => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)

@[simp]

theorem Turing.ToPartrec.Code.zero'_eval : Turing.ToPartrec.Code.zero'.eval = fun (v : List ℕ) => pure (0 :: v)

@[simp]

theorem Turing.ToPartrec.Code.succ_eval : Turing.ToPartrec.Code.succ.eval = fun (v : List ℕ) => pure [v.headI.succ]

@[simp]

theorem Turing.ToPartrec.Code.tail_eval : Turing.ToPartrec.Code.tail.eval = fun (v : List ℕ) => pure v.tail

@[simp]

theorem Turing.ToPartrec.Code.cons_eval (f fs : Turing.ToPartrec.Code) : (f.cons fs).eval = fun (v : List ℕ) => do let n ← f.eval v let ns ← fs.eval v pure (n.headI :: ns)

@[simp]

theorem Turing.ToPartrec.Code.comp_eval (f g : Turing.ToPartrec.Code) : (f.comp g).eval = fun (v : List ℕ) => g.eval v >>= f.eval

@[simp]

theorem Turing.ToPartrec.Code.case_eval (f g : Turing.ToPartrec.Code) : (f.case g).eval = fun (v : List ℕ) => Nat.rec (f.eval v.tail) (fun (y : ℕ) (x : Part (List ℕ)) => g.eval (y :: v.tail)) v.headI

@[simp]

theorem Turing.ToPartrec.Code.fix_eval (f : Turing.ToPartrec.Code) : f.fix.eval = PFun.fix fun (v : List ℕ) => Part.map (fun (v : List ℕ) => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)

def Turing.ToPartrec.Code.nil : Turing.ToPartrec.Code

nil is the constant nil function: nil v = [].

Equations

• Turing.ToPartrec.Code.nil = Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.succ

@[simp]

theorem Turing.ToPartrec.Code.nil_eval (v : List ℕ) : Turing.ToPartrec.Code.nil.eval v = pure []

def Turing.ToPartrec.Code.id : Turing.ToPartrec.Code

id is the identity function: id v = v.

Equations

• Turing.ToPartrec.Code.id = Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.zero'

@[simp]

theorem Turing.ToPartrec.Code.id_eval (v : List ℕ) : Turing.ToPartrec.Code.id.eval v = pure v

def Turing.ToPartrec.Code.head : Turing.ToPartrec.Code

head gets the head of the input list: head [] = [0], head (n :: v) = [n].

Equations

• Turing.ToPartrec.Code.head = Turing.ToPartrec.Code.id.cons Turing.ToPartrec.Code.nil

@[simp]

theorem Turing.ToPartrec.Code.head_eval (v : List ℕ) : Turing.ToPartrec.Code.head.eval v = pure [v.headI]

def Turing.ToPartrec.Code.zero : Turing.ToPartrec.Code

zero is the constant zero function: zero v = [0].

Equations

• Turing.ToPartrec.Code.zero = Turing.ToPartrec.Code.zero'.cons Turing.ToPartrec.Code.nil

@[simp]

theorem Turing.ToPartrec.Code.zero_eval (v : List ℕ) : Turing.ToPartrec.Code.zero.eval v = pure [0]

def Turing.ToPartrec.Code.pred : Turing.ToPartrec.Code

pred returns the predecessor of the head of the input: pred [] = [0], pred (0 :: v) = [0], pred (n+1 :: v) = [n].

Equations

• Turing.ToPartrec.Code.pred = Turing.ToPartrec.Code.zero.case Turing.ToPartrec.Code.head

@[simp]

theorem Turing.ToPartrec.Code.pred_eval (v : List ℕ) : Turing.ToPartrec.Code.pred.eval v = pure [v.headI.pred]

def Turing.ToPartrec.Code.rfind (f : Turing.ToPartrec.Code) : Turing.ToPartrec.Code

rfind f performs the function of the rfind primitive of partial recursive functions. rfind f v returns the smallest n such that (f (n :: v)).head = 0.

It is implemented as:

rfind f v = pred (fix (fun (n::v) => f (n::v) :: n+1 :: v) (0 :: v))

The idea is that the initial state is 0 :: v, and the fix keeps n :: v as its internal state; it calls f (n :: v) as the exit test and n+1 :: v as the next state. At the end we get n+1 :: v where n is the desired output, and pred (n+1 :: v) = [n] returns the result.

Equations

• f.rfind = Turing.ToPartrec.Code.pred.comp ((f.cons (Turing.ToPartrec.Code.succ.cons Turing.ToPartrec.Code.tail)).fix.comp Turing.ToPartrec.Code.zero')

def Turing.ToPartrec.Code.prec (f g : Turing.ToPartrec.Code) : Turing.ToPartrec.Code

prec f g implements the prec (primitive recursion) operation of partial recursive functions. prec f g evaluates as:

• prec f g [] = [f []]
• prec f g (0 :: v) = [f v]
• prec f g (n+1 :: v) = [g (n :: prec f g (n :: v) :: v)]

It is implemented as:

G (a :: b :: IH :: v) = (b :: a+1 :: b-1 :: g (a :: IH :: v) :: v)
F (0 :: f_v :: v) = (f_v :: v)
F (n+1 :: f_v :: v) = (fix G (0 :: n :: f_v :: v)).tail.tail
prec f g (a :: v) = [(F (a :: f v :: v)).head]

Because fix always evaluates its body at least once, we must special case the 0 case to avoid calling g more times than necessary (which could be bad if g diverges). If the input is 0 :: v, then F (0 :: f v :: v) = (f v :: v) so we return [f v]. If the input is n+1 :: v, we evaluate the function from the bottom up, with initial state 0 :: n :: f v :: v. The first number counts up, providing arguments for the applications to g, while the second number counts down, providing the exit condition (this is the initial b in the return value of G, which is stripped by fix). After the fix is complete, the final state is n :: 0 :: res :: v where res is the desired result, and the rest reduces this to [res].

Equations

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

theorem Turing.ToPartrec.Code.exists_code.comp {m n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : Fin n → List.Vector ℕ m →. ℕ} (hf : ∃ (c : Turing.ToPartrec.Code), ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v) (hg : ∀ (i : Fin n), ∃ (c : Turing.ToPartrec.Code), ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) : ∃ (c : Turing.ToPartrec.Code), ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((List.Vector.mOfFn fun (i : Fin n) => g i v) >>= f)

theorem Turing.ToPartrec.Code.exists_code {n : ℕ} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : ∃ (c : Turing.ToPartrec.Code), ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v

From compositional semantics to sequential semantics

Our initial sequential model is designed to be as similar as possible to the compositional semantics in terms of its primitives, but it is a sequential semantics, meaning that rather than defining an eval c : List ℕ →. List ℕ function for each program, defined by recursion on programs, we have a type Cfg with a step function step : Cfg → Option cfg that provides a deterministic evaluation order. In order to do this, we introduce the notion of a continuation, which can be viewed as a Code with a hole in it where evaluation is currently taking place. Continuations can be assigned a List ℕ →. List ℕ semantics as well, with the interpretation being that given a List ℕ result returned from the code in the hole, the remainder of the program will evaluate to a List ℕ final value.

The continuations are:

• halt: the empty continuation: the hole is the whole program, whatever is returned is the final result. In our notation this is just _.
• cons₁ fs v k: evaluating the first part of a cons, that is k (_ :: fs v), where k is the outer continuation.
• cons₂ ns k: evaluating the second part of a cons: k (ns.headI :: _). (Technically we don't need to hold on to all of ns here since we are already committed to taking the head, but this is more regular.)
• comp f k: evaluating the first part of a composition: k (f _).
• fix f k: waiting for the result of f in a fix f expression: k (if _.headI = 0 then _.tail else fix f (_.tail))

The type Cfg of evaluation states is:

• ret k v: we have received a result, and are now evaluating the continuation k with result v; that is, k v where k is ready to evaluate.
• halt v: we are done and the result is v.

The main theorem of this section is that for each code c, the state stepNormal c halt v steps to v' in finitely many steps if and only if Code.eval c v = some v'.

inductive Turing.ToPartrec.Cont : Type

The type of continuations, built up during evaluation of a Code expression.

• halt : Turing.ToPartrec.Cont
• cons₁ : Turing.ToPartrec.Code → List ℕ → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
• cons₂ : List ℕ → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
• comp : Turing.ToPartrec.Code → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
• fix : Turing.ToPartrec.Code → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont

instance Turing.ToPartrec.instInhabitedCont : Inhabited Turing.ToPartrec.Cont

Equations

• Turing.ToPartrec.instInhabitedCont = { default := Turing.ToPartrec.Cont.halt }

def Turing.ToPartrec.Cont.eval : Turing.ToPartrec.Cont → List ℕ →. List ℕ

The semantics of a continuation.

Equations

• Turing.ToPartrec.Cont.halt.eval = pure
• (Turing.ToPartrec.Cont.cons₁ fs as k).eval = fun (v : List ℕ) => do let ns ← fs.eval as k.eval (v.headI :: ns)
• (Turing.ToPartrec.Cont.cons₂ ns k).eval = fun (v : List ℕ) => k.eval (ns.headI :: v)
• (Turing.ToPartrec.Cont.comp f k).eval = fun (v : List ℕ) => f.eval v >>= k.eval
• (Turing.ToPartrec.Cont.fix f k).eval = fun (v : List ℕ) => if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval

inductive Turing.ToPartrec.Cfg : Type

The set of configurations of the machine:

• halt v: The machine is about to stop and v : List ℕ is the result.
• ret k v: The machine is about to pass v : List ℕ to continuation k : Cont.

We don't have a state corresponding to normal evaluation because these are evaluated immediately to a ret "in zero steps" using the stepNormal function.

• halt : List ℕ → Turing.ToPartrec.Cfg
• ret : Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg

instance Turing.ToPartrec.instInhabitedCfg : Inhabited Turing.ToPartrec.Cfg

Equations

• Turing.ToPartrec.instInhabitedCfg = { default := Turing.ToPartrec.Cfg.halt default }

def Turing.ToPartrec.stepNormal : Turing.ToPartrec.Code → Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg

Evaluating c : Code in a continuation k : Cont and input v : List ℕ. This goes by recursion on c, building an augmented continuation and a value to pass to it.

• zero' v = 0 :: v evaluates immediately, so we return it to the parent continuation
• succ v = [v.headI.succ] evaluates immediately, so we return it to the parent continuation
• tail v = v.tail evaluates immediately, so we return it to the parent continuation
• cons f fs v = (f v).headI :: fs v requires two sub-evaluations, so we evaluate f v in the continuation k (_.headI :: fs v) (called Cont.cons₁ fs v k)
• comp f g v = f (g v) requires two sub-evaluations, so we evaluate g v in the continuation k (f _) (called Cont.comp f k)
• case f g v = v.head.casesOn (f v.tail) (fun n => g (n :: v.tail)) has the information needed to evaluate the case statement, so we do that and transition to either f v or g (n :: v.tail).
• fix f v = let v' := f v; if v'.headI = 0 then k v'.tail else fix f v'.tail needs to first evaluate f v, so we do that and leave the rest for the continuation (called Cont.fix f k)

Equations

• One or more equations did not get rendered due to their size.
• Turing.ToPartrec.stepNormal Turing.ToPartrec.Code.zero' = fun (k : Turing.ToPartrec.Cont) (v : List ℕ) => Turing.ToPartrec.Cfg.ret k (0 :: v)
• Turing.ToPartrec.stepNormal Turing.ToPartrec.Code.succ = fun (k : Turing.ToPartrec.Cont) (v : List ℕ) => Turing.ToPartrec.Cfg.ret k [v.headI.succ]
• Turing.ToPartrec.stepNormal Turing.ToPartrec.Code.tail = fun (k : Turing.ToPartrec.Cont) (v : List ℕ) => Turing.ToPartrec.Cfg.ret k v.tail
• Turing.ToPartrec.stepNormal (f.cons fs) = fun (k : Turing.ToPartrec.Cont) (v : List ℕ) => Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.cons₁ fs v k) v
• Turing.ToPartrec.stepNormal (f.comp g) = fun (k : Turing.ToPartrec.Cont) (v : List ℕ) => Turing.ToPartrec.stepNormal g (Turing.ToPartrec.Cont.comp f k) v
• Turing.ToPartrec.stepNormal f.fix = fun (k : Turing.ToPartrec.Cont) (v : List ℕ) => Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v

def Turing.ToPartrec.stepRet : Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg

Evaluating a continuation k : Cont on input v : List ℕ. This is the second part of evaluation, when we receive results from continuations built by stepNormal.

• Cont.halt v = v, so we are done and transition to the Cfg.halt v state
• Cont.cons₁ fs as k v = k (v.headI :: fs as), so we evaluate fs as now with the continuation k (v.headI :: _) (called cons₂ v k).
• Cont.cons₂ ns k v = k (ns.headI :: v), where we now have everything we need to evaluate ns.headI :: v, so we return it to k.
• Cont.comp f k v = k (f v), so we call f v with k as the continuation.
• Cont.fix f k v = k (if v.headI = 0 then k v.tail else fix f v.tail), where v is a value, so we evaluate the if statement and either call k with v.tail, or call fix f v with k as the continuation (which immediately calls f with Cont.fix f k as the continuation).

Equations

• Turing.ToPartrec.stepRet Turing.ToPartrec.Cont.halt x✝ = Turing.ToPartrec.Cfg.halt x✝
• Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.cons₁ fs as k) x✝ = Turing.ToPartrec.stepNormal fs (Turing.ToPartrec.Cont.cons₂ x✝ k) as
• Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.cons₂ ns k) x✝ = Turing.ToPartrec.stepRet k (ns.headI :: x✝)
• Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.comp f k) x✝ = Turing.ToPartrec.stepNormal f k x✝
• Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.fix f k) x✝ = if x✝.headI = 0 then Turing.ToPartrec.stepRet k x✝.tail else Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) x✝.tail

def Turing.ToPartrec.step : Turing.ToPartrec.Cfg → Option Turing.ToPartrec.Cfg

If we are not done (in Cfg.halt state), then we must be still stuck on a continuation, so this main loop calls stepRet with the new continuation. The overall step function transitions from one Cfg to another, only halting at the Cfg.halt state.

Equations

• Turing.ToPartrec.step (Turing.ToPartrec.Cfg.halt a) = none
• Turing.ToPartrec.step (Turing.ToPartrec.Cfg.ret k v) = some (Turing.ToPartrec.stepRet k v)

def Turing.ToPartrec.Cont.then : Turing.ToPartrec.Cont → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont

In order to extract a compositional semantics from the sequential execution behavior of configurations, we observe that continuations have a monoid structure, with Cont.halt as the unit and Cont.then as the multiplication. Cont.then k₁ k₂ runs k₁ until it halts, and then takes the result of k₁ and passes it to k₂.

We will not prove it is associative (although it is), but we are instead interested in the associativity law k₂ (eval c k₁) = eval c (k₁.then k₂). This holds at both the sequential and compositional levels, and allows us to express running a machine without the ambient continuation and relate it to the original machine's evaluation steps. In the literature this is usually where one uses Turing machines embedded inside other Turing machines, but this approach allows us to avoid changing the ambient type Cfg in the middle of the recursion.

Equations

• Turing.ToPartrec.Cont.halt.then = fun (k' : Turing.ToPartrec.Cont) => k'
• (Turing.ToPartrec.Cont.cons₁ fs as k).then = fun (k' : Turing.ToPartrec.Cont) => Turing.ToPartrec.Cont.cons₁ fs as (k.then k')
• (Turing.ToPartrec.Cont.cons₂ ns k).then = fun (k' : Turing.ToPartrec.Cont) => Turing.ToPartrec.Cont.cons₂ ns (k.then k')
• (Turing.ToPartrec.Cont.comp f k).then = fun (k' : Turing.ToPartrec.Cont) => Turing.ToPartrec.Cont.comp f (k.then k')
• (Turing.ToPartrec.Cont.fix f k).then = fun (k' : Turing.ToPartrec.Cont) => Turing.ToPartrec.Cont.fix f (k.then k')

theorem Turing.ToPartrec.Cont.then_eval {k k' : Turing.ToPartrec.Cont} {v : List ℕ} : (k.then k').eval v = k.eval v >>= k'.eval

def Turing.ToPartrec.Cfg.then : Turing.ToPartrec.Cfg → Turing.ToPartrec.Cont → Turing.ToPartrec.Cfg

The then k function is a "configuration homomorphism". Its operation on states is to append k to the continuation of a Cfg.ret state, and to run k on v if we are in the Cfg.halt v state.

Equations

• (Turing.ToPartrec.Cfg.halt a).then = fun (k' : Turing.ToPartrec.Cont) => Turing.ToPartrec.stepRet k' a
• (Turing.ToPartrec.Cfg.ret k v).then = fun (k' : Turing.ToPartrec.Cont) => Turing.ToPartrec.Cfg.ret (k.then k') v

theorem Turing.ToPartrec.stepNormal_then (c : Turing.ToPartrec.Code) (k k' : Turing.ToPartrec.Cont) (v : List ℕ) : Turing.ToPartrec.stepNormal c (k.then k') v = (Turing.ToPartrec.stepNormal c k v).then k'

The stepNormal function respects the then k' homomorphism. Note that this is an exact equality, not a simulation; the original and embedded machines move in lock-step until the embedded machine reaches the halt state.

theorem Turing.ToPartrec.stepRet_then {k k' : Turing.ToPartrec.Cont} {v : List ℕ} : Turing.ToPartrec.stepRet (k.then k') v = (Turing.ToPartrec.stepRet k v).then k'

The stepRet function respects the then k' homomorphism. Note that this is an exact equality, not a simulation; the original and embedded machines move in lock-step until the embedded machine reaches the halt state.

def Turing.ToPartrec.Code.Ok (c : Turing.ToPartrec.Code) : Prop

This is a temporary definition, because we will prove in code_is_ok that it always holds. It asserts that c is semantically correct; that is, for any k and v, eval (stepNormal c k v) = eval (Cfg.ret k (Code.eval c v)), as an equality of partial values (so one diverges iff the other does).

In particular, we can let k = Cont.halt, and then this asserts that stepNormal c Cont.halt v evaluates to Cfg.halt (Code.eval c v).

Equations

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

theorem Turing.ToPartrec.Code.Ok.zero {c : Turing.ToPartrec.Code} (h : c.Ok) {v : List ℕ} : Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) = Turing.ToPartrec.Cfg.halt <$> c.eval v

theorem Turing.ToPartrec.stepNormal.is_ret (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont) (v : List ℕ) : ∃ (k' : Turing.ToPartrec.Cont) (v' : List ℕ), Turing.ToPartrec.stepNormal c k v = Turing.ToPartrec.Cfg.ret k' v'

theorem Turing.ToPartrec.cont_eval_fix {f : Turing.ToPartrec.Code} {k : Turing.ToPartrec.Cont} {v : List ℕ} (fok : f.Ok) : Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v) = do let v ← f.fix.eval v Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.Cfg.ret k v)

theorem Turing.ToPartrec.code_is_ok (c : Turing.ToPartrec.Code) : c.Ok

theorem Turing.ToPartrec.stepNormal_eval (c : Turing.ToPartrec.Code) (v : List ℕ) : Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) = Turing.ToPartrec.Cfg.halt <$> c.eval v

theorem Turing.ToPartrec.stepRet_eval {k : Turing.ToPartrec.Cont} {v : List ℕ} : Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepRet k v) = Turing.ToPartrec.Cfg.halt <$> k.eval v

Simulating sequentialized partial recursive functions in TM2

At this point we have a sequential model of partial recursive functions: the Cfg type and step : Cfg → Option Cfg function from the previous section. The key feature of this model is that it does a finite amount of computation (in fact, an amount which is statically bounded by the size of the program) between each step, and no individual step can diverge (unlike the compositional semantics, where every sub-part of the computation is potentially divergent). So we can utilize the same techniques as in the other TM simulations in Computability.TuringMachine to prove that each step corresponds to a finite number of steps in a lower level model. (We don't prove it here, but in anticipation of the complexity class P, the simulation is actually polynomial-time as well.)

The target model is Turing.TM2, which has a fixed finite set of stacks, a bit of local storage, with programs selected from a potentially infinite (but finitely accessible) set of program positions, or labels Λ, each of which executes a finite sequence of basic stack commands.

For this program we will need four stacks, each on an alphabet Γ' like so:

inductive Γ'  | consₗ | cons | bit0 | bit1

We represent a number as a bit sequence, lists of numbers by putting cons after each element, and lists of lists of natural numbers by putting consₗ after each list. For example:

0 ~> []
1 ~> [bit1]
6 ~> [bit0, bit1, bit1]
[1, 2] ~> [bit1, cons, bit0, bit1, cons]
[[], [1, 2]] ~> [consₗ, bit1, cons, bit0, bit1, cons, consₗ]

The four stacks are main, rev, aux, stack. In normal mode, main contains the input to the current program (a List ℕ) and stack contains data (a List (List ℕ)) associated to the current continuation, and in ret mode main contains the value that is being passed to the continuation and stack contains the data for the continuation. The rev and aux stacks are usually empty; rev is used to store reversed data when e.g. moving a value from one stack to another, while aux is used as a temporary for a main/stack swap that happens during cons₁ evaluation.

The only local store we need is Option Γ', which stores the result of the last pop operation. (Most of our working data are natural numbers, which are too large to fit in the local store.)

The continuations from the previous section are data-carrying, containing all the values that have been computed and are awaiting other arguments. In order to have only a finite number of continuations appear in the program so that they can be used in machine states, we separate the data part (anything with type List ℕ) from the Cont type, producing a Cont' type that lacks this information. The data is kept on the stack stack.

Because we want to have subroutines for e.g. moving an entire stack to another place, we use an infinite inductive type Λ' so that we can execute a program and then return to do something else without having to define too many different kinds of intermediate states. (We must nevertheless prove that only finitely many labels are accessible.) The labels are:

• move p k₁ k₂ q: move elements from stack k₁ to k₂ while p holds of the value being moved. The last element, that fails p, is placed in neither stack but left in the local store. At the end of the operation, k₂ will have the elements of k₁ in reverse order. Then do q.
• clear p k q: delete elements from stack k until p is true. Like move, the last element is left in the local storage. Then do q.
• copy q: Move all elements from rev to both main and stack (in reverse order), then do q. That is, it takes (a, b, c, d) to (b.reverse ++ a, [], c, b.reverse ++ d).
• push k f q: push f s, where s is the local store, to stack k, then do q. This is a duplicate of the push instruction that is part of the TM2 model, but by having a subroutine just for this purpose we can build up programs to execute inside a goto statement, where we have the flexibility to be general recursive.
• read (f : Option Γ' → Λ'): go to state f s where s is the local store. Again this is only here for convenience.
• succ q: perform a successor operation. Assuming [n] is encoded on main before, [n+1] will be on main after. This implements successor for binary natural numbers.
• pred q₁ q₂: perform a predecessor operation or case statement. If [] is encoded on main before, then we transition to q₁ with [] on main; if (0 :: v) is on main before then v will be on main after and we transition to q₁; and if (n+1 :: v) is on main before then n :: v will be on main after and we transition to q₂.
• ret k: call continuation k. Each continuation has its own interpretation of the data in stack and sets up the data for the next continuation.
  • ret (cons₁ fs k): v :: KData on stack and ns on main, and the next step expects v on main and ns :: KData on stack. So we have to do a little dance here with six reverse-moves using the aux stack to perform a three-point swap, each of which involves two reversals.
  • ret (cons₂ k): ns :: KData is on stack and v is on main, and we have to put ns.headI :: v on main and KData on stack. This is done using the head subroutine.
  • ret (fix f k): This stores no data, so we just check if main starts with 0 and if so, remove it and call k, otherwise clear the first value and call f.
  • ret halt: the stack is empty, and main has the output. Do nothing and halt.

In addition to these basic states, we define some additional subroutines that are used in the above:

• push', peek', pop' are special versions of the builtins that use the local store to supply inputs and outputs.
• unrev: special case move false rev main to move everything from rev back to main. Used as a cleanup operation in several functions.
• moveExcl p k₁ k₂ q: same as move but pushes the last value read back onto the source stack.
• move₂ p k₁ k₂ q: double move, so that the result comes out in the right order at the target stack. Implemented as moveExcl p k rev; move false rev k₂. Assumes that neither k₁ nor k₂ is rev and rev is initially empty.
• head k q: get the first natural number from stack k and reverse-move it to rev, then clear the rest of the list at k and then unrev to reverse-move the head value to main. This is used with k = main to implement regular head, i.e. if v is on main before then [v.headI] will be on main after; and also with k = stack for the cons operation, which has v on main and ns :: KData on stack, and results in KData on stack and ns.headI :: v on main.
• trNormal is the main entry point, defining states that perform a given code computation. It mostly just dispatches to functions written above.

The main theorem of this section is tr_eval, which asserts that for each that for each code c, the state init c v steps to halt v' in finitely many steps if and only if Code.eval c v = some v'.

inductive Turing.PartrecToTM2.Γ' : Type

The alphabet for the stacks in the program. bit0 and bit1 are used to represent ℕ values as lists of binary digits, cons is used to separate List ℕ values, and consₗ is used to separate List (List ℕ) values. See the section documentation.

• consₗ : Turing.PartrecToTM2.Γ'
• cons : Turing.PartrecToTM2.Γ'
• bit0 : Turing.PartrecToTM2.Γ'
• bit1 : Turing.PartrecToTM2.Γ'

instance Turing.PartrecToTM2.instDecidableEqΓ' : DecidableEq Turing.PartrecToTM2.Γ'

Equations

• Turing.PartrecToTM2.instDecidableEqΓ' x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Turing.PartrecToTM2.instInhabitedΓ' : Inhabited Turing.PartrecToTM2.Γ'

Equations

• Turing.PartrecToTM2.instInhabitedΓ' = { default := Turing.PartrecToTM2.Γ'.consₗ }

instance Turing.PartrecToTM2.instFintypeΓ' : Fintype Turing.PartrecToTM2.Γ'

Equations

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

inductive Turing.PartrecToTM2.K' : Type

The four stacks used by the program. main is used to store the input value in trNormal mode and the output value in Λ'.ret mode, while stack is used to keep all the data for the continuations. rev is used to store reversed lists when transferring values between stacks, and aux is only used once in cons₁. See the section documentation.

• main : Turing.PartrecToTM2.K'
• rev : Turing.PartrecToTM2.K'
• aux : Turing.PartrecToTM2.K'
• stack : Turing.PartrecToTM2.K'

instance Turing.PartrecToTM2.instDecidableEqK' : DecidableEq Turing.PartrecToTM2.K'

Equations

• Turing.PartrecToTM2.instDecidableEqK' x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Turing.PartrecToTM2.instInhabitedK' : Inhabited Turing.PartrecToTM2.K'

Equations

• Turing.PartrecToTM2.instInhabitedK' = { default := Turing.PartrecToTM2.K'.main }

inductive Turing.PartrecToTM2.Cont' : Type

Continuations as in ToPartrec.Cont but with the data removed. This is done because we want the set of all continuations in the program to be finite (so that it can ultimately be encoded into the finite state machine of a Turing machine), but a continuation can handle a potentially infinite number of data values during execution.

• halt : Turing.PartrecToTM2.Cont'
• cons₁ : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'
• cons₂ : Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'
• comp : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'
• fix : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'

instance Turing.PartrecToTM2.instDecidableEqCont' : DecidableEq Turing.PartrecToTM2.Cont'

Equations

• Turing.PartrecToTM2.instDecidableEqCont' = Turing.PartrecToTM2.decEqCont'✝

instance Turing.PartrecToTM2.instInhabitedCont' : Inhabited Turing.PartrecToTM2.Cont'

Equations

• Turing.PartrecToTM2.instInhabitedCont' = { default := Turing.PartrecToTM2.Cont'.halt }

inductive Turing.PartrecToTM2.Λ' : Type

The set of program positions. We make extensive use of inductive types here to let us describe "subroutines"; for example clear p k q is a program that clears stack k, then does q where q is another label. In order to prevent this from resulting in an infinite number of distinct accessible states, we are careful to be non-recursive (although loops are okay). See the section documentation for a description of all the programs.

• move (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'
• clear (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'
• copy (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'
• push (k : Turing.PartrecToTM2.K') (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'
• read (f : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'
• succ (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'
• pred (q₁ q₂ : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'
• ret (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.Λ'

instance Turing.PartrecToTM2.Λ'.instInhabited : Inhabited Turing.PartrecToTM2.Λ'

Equations

• Turing.PartrecToTM2.Λ'.instInhabited = { default := Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt }

instance Turing.PartrecToTM2.Λ'.instDecidableEq : DecidableEq Turing.PartrecToTM2.Λ'

Equations

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

def Turing.PartrecToTM2.Stmt' : Type

The type of TM2 statements used by this machine.

Equations

• Turing.PartrecToTM2.Stmt' = Turing.TM2.Stmt (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')

instance Turing.PartrecToTM2.instStmt'Inhabited : Inhabited Turing.PartrecToTM2.Stmt'

Equations

• Turing.PartrecToTM2.instStmt'Inhabited = Turing.TM2.Stmt.inhabited (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')

def Turing.PartrecToTM2.Cfg' : Type

The type of TM2 configurations used by this machine.

Equations

• Turing.PartrecToTM2.Cfg' = Turing.TM2.Cfg (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')

instance Turing.PartrecToTM2.instCfg'Inhabited : Inhabited Turing.PartrecToTM2.Cfg'

Equations

• Turing.PartrecToTM2.instCfg'Inhabited = Turing.TM2.Cfg.inhabited (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')

def Turing.PartrecToTM2.natEnd : Turing.PartrecToTM2.Γ' → Bool

A predicate that detects the end of a natural number, either Γ'.cons or Γ'.consₗ (or implicitly the end of the list), for use in predicate-taking functions like move and clear.

Equations

• Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.Γ'.consₗ = true
• Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.Γ'.cons = true
• Turing.PartrecToTM2.natEnd x✝ = false

def Turing.PartrecToTM2.pop' (k : Turing.PartrecToTM2.K') : Turing.PartrecToTM2.Stmt' → Turing.PartrecToTM2.Stmt'

Pop a value from the stack and place the result in local store.

Equations

• Turing.PartrecToTM2.pop' k = Turing.TM2.Stmt.pop k fun (x v : Option Turing.PartrecToTM2.Γ') => v

def Turing.PartrecToTM2.peek' (k : Turing.PartrecToTM2.K') : Turing.PartrecToTM2.Stmt' → Turing.PartrecToTM2.Stmt'

Peek a value from the stack and place the result in local store.

Equations

• Turing.PartrecToTM2.peek' k = Turing.TM2.Stmt.peek k fun (x v : Option Turing.PartrecToTM2.Γ') => v

def Turing.PartrecToTM2.push' (k : Turing.PartrecToTM2.K') : Turing.PartrecToTM2.Stmt' → Turing.PartrecToTM2.Stmt'

Push the value in the local store to the given stack.

Equations

• Turing.PartrecToTM2.push' k = Turing.TM2.Stmt.push k fun (x : Option Turing.PartrecToTM2.Γ') => x.iget

def Turing.PartrecToTM2.unrev (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'

Move everything from the rev stack to the main stack (reversed).

Equations

• Turing.PartrecToTM2.unrev = Turing.PartrecToTM2.Λ'.move (fun (x : Turing.PartrecToTM2.Γ') => false) Turing.PartrecToTM2.K'.rev Turing.PartrecToTM2.K'.main

def Turing.PartrecToTM2.moveExcl (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'

Move elements from k₁ to k₂ while p holds, with the last element being left on k₁.

Equations

• Turing.PartrecToTM2.moveExcl p k₁ k₂ q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ (Turing.PartrecToTM2.Λ'.push k₁ id q)

def Turing.PartrecToTM2.move₂ (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'

Move elements from k₁ to k₂ without reversion, by performing a double move via the rev stack.

Equations

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

def Turing.PartrecToTM2.head (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ'

Assuming trList v is on the front of stack k, remove it, and push v.headI onto main. See the section documentation.

Equations

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

def Turing.PartrecToTM2.trNormal : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Λ'

The program that evaluates code c with continuation k. This expects an initial state where trList v is on main, trContStack k is on stack, and aux and rev are empty. See the section documentation for details.

Equations

• One or more equations did not get rendered due to their size.
• Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.succ x✝ = Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret x✝).succ
• Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.tail x✝ = Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret x✝)
• Turing.PartrecToTM2.trNormal (f.comp g) x✝ = Turing.PartrecToTM2.trNormal g (Turing.PartrecToTM2.Cont'.comp f x✝)
• Turing.PartrecToTM2.trNormal (f.case g) x✝ = (Turing.PartrecToTM2.trNormal f x✝).pred (Turing.PartrecToTM2.trNormal g x✝)
• Turing.PartrecToTM2.trNormal f.fix x✝ = Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f x✝)

def Turing.PartrecToTM2.tr : Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Stmt'

The main program. See the section documentation for details.

Equations

• One or more equations did not get rendered due to their size.
• Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.read q) = Turing.TM2.Stmt.goto q
• Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)) = Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.trNormal f k
• Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt) = Turing.TM2.Stmt.load (fun (x : Option Turing.PartrecToTM2.Γ') => none) Turing.TM2.Stmt.halt

@[simp]

theorem Turing.PartrecToTM2.tr_move (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) = Turing.PartrecToTM2.pop' k₁ (Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => s.elim true p) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q) (Turing.PartrecToTM2.push' k₂ (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Λ'.move p k₁ k₂ q)))

@[simp]

theorem Turing.PartrecToTM2.tr_push (k : Turing.PartrecToTM2.K') (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.push k f q) = Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => (f s).isSome) (Turing.TM2.Stmt.push k (fun (s : Option Turing.PartrecToTM2.Γ') => (f s).iget) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q)) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q)

@[simp]

theorem Turing.PartrecToTM2.tr_read (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.read q) = Turing.TM2.Stmt.goto q

@[simp]

theorem Turing.PartrecToTM2.tr_clear (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.clear p k q) = Turing.PartrecToTM2.pop' k (Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => s.elim true p) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Λ'.clear p k q))

@[simp]

theorem Turing.PartrecToTM2.tr_copy (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.tr q.copy = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.rev (Turing.TM2.Stmt.branch Option.isSome (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.stack (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q.copy))) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q))

@[simp]

theorem Turing.PartrecToTM2.tr_succ (q : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.tr q.succ = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => decide (s = some Turing.PartrecToTM2.Γ'.bit1)) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Γ'.bit0) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q.succ)) (Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => decide (s = some Turing.PartrecToTM2.Γ'.cons)) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Γ'.cons) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Γ'.bit1) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.unrev q))) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Γ'.bit1) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.unrev q))))

@[simp]

theorem Turing.PartrecToTM2.tr_pred (q₁ q₂ : Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.tr (q₁.pred q₂) = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => decide (s = some Turing.PartrecToTM2.Γ'.bit0)) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Γ'.bit1) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q₁.pred q₂)) (Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.natEnd s.iget) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => q₁) (Turing.PartrecToTM2.peek' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.branch (fun (s : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.natEnd s.iget) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.unrev q₂) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.Γ'.bit0) (Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.unrev q₂))))))

@[simp]

theorem Turing.PartrecToTM2.tr_ret_cons₁ (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)) = Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.move₂ (fun (x : Turing.PartrecToTM2.Γ') => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux (Turing.PartrecToTM2.move₂ (fun (s : Turing.PartrecToTM2.Γ') => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.move₂ (fun (x : Turing.PartrecToTM2.Γ') => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.trNormal fs k.cons₂)))

@[simp]

theorem Turing.PartrecToTM2.tr_ret_cons₂ (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k.cons₂) = Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)

@[simp]

theorem Turing.PartrecToTM2.tr_ret_comp (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)) = Turing.TM2.Stmt.goto fun (x : Option Turing.PartrecToTM2.Γ') => Turing.PartrecToTM2.trNormal f k

@[simp]

theorem Turing.PartrecToTM2.tr_ret_fix (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)) = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.goto fun (s : Option Turing.PartrecToTM2.Γ') => bif Turing.PartrecToTM2.natEnd s.iget then Turing.PartrecToTM2.Λ'.ret k else Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f k)))

@[simp]

theorem Turing.PartrecToTM2.tr_ret_halt : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt) = Turing.TM2.Stmt.load (fun (x : Option Turing.PartrecToTM2.Γ') => none) Turing.TM2.Stmt.halt

def Turing.PartrecToTM2.trCont : Turing.ToPartrec.Cont → Turing.PartrecToTM2.Cont'

Translating a Cont continuation to a Cont' continuation simply entails dropping all the data. This data is instead encoded in trContStack in the configuration.

Equations

• Turing.PartrecToTM2.trCont Turing.ToPartrec.Cont.halt = Turing.PartrecToTM2.Cont'.halt
• Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.cons₁ fs as k) = Turing.PartrecToTM2.Cont'.cons₁ fs (Turing.PartrecToTM2.trCont k)
• Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.cons₂ ns k) = (Turing.PartrecToTM2.trCont k).cons₂
• Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.comp f k) = Turing.PartrecToTM2.Cont'.comp f (Turing.PartrecToTM2.trCont k)
• Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.fix f k) = Turing.PartrecToTM2.Cont'.fix f (Turing.PartrecToTM2.trCont k)

def Turing.PartrecToTM2.trPosNum : PosNum → List Turing.PartrecToTM2.Γ'

We use PosNum to define the translation of binary natural numbers. A natural number is represented as a little-endian list of bit0 and bit1 elements:

1 = [bit1]
2 = [bit0, bit1]
3 = [bit1, bit1]
4 = [bit0, bit0, bit1]

In particular, this representation guarantees no trailing bit0's at the end of the list.

Equations

• Turing.PartrecToTM2.trPosNum PosNum.one = [Turing.PartrecToTM2.Γ'.bit1]
• Turing.PartrecToTM2.trPosNum n.bit0 = Turing.PartrecToTM2.Γ'.bit0 :: Turing.PartrecToTM2.trPosNum n
• Turing.PartrecToTM2.trPosNum n.bit1 = Turing.PartrecToTM2.Γ'.bit1 :: Turing.PartrecToTM2.trPosNum n

def Turing.PartrecToTM2.trNum : Num → List Turing.PartrecToTM2.Γ'

We use Num to define the translation of binary natural numbers. Positive numbers are translated using trPosNum, and trNum 0 = []. So there are never any trailing bit0's in a translated Num.

0 = []
1 = [bit1]
2 = [bit0, bit1]
3 = [bit1, bit1]
4 = [bit0, bit0, bit1]

Equations

• Turing.PartrecToTM2.trNum Num.zero = []
• Turing.PartrecToTM2.trNum (Num.pos n) = Turing.PartrecToTM2.trPosNum n

def Turing.PartrecToTM2.trNat (n : ℕ) : List Turing.PartrecToTM2.Γ'

Because we use binary encoding, we define trNat in terms of trNum, using Num, which are binary natural numbers. (We could also use Nat.binaryRecOn, but Num and PosNum make for easy inductions.)

Equations

• Turing.PartrecToTM2.trNat n = Turing.PartrecToTM2.trNum ↑n

@[simp]

theorem Turing.PartrecToTM2.trNat_zero : Turing.PartrecToTM2.trNat 0 = []

theorem Turing.PartrecToTM2.trNat_default : Turing.PartrecToTM2.trNat default = []

def Turing.PartrecToTM2.trList : List ℕ → List Turing.PartrecToTM2.Γ'

Lists are translated with a cons after each encoded number. For example:

[] = []
[0] = [cons]
[1] = [bit1, cons]
[6, 0] = [bit0, bit1, bit1, cons, cons]

Equations

• Turing.PartrecToTM2.trList [] = []
• Turing.PartrecToTM2.trList (n :: ns) = Turing.PartrecToTM2.trNat n ++ Turing.PartrecToTM2.Γ'.cons :: Turing.PartrecToTM2.trList ns

def Turing.PartrecToTM2.trLList : List (List ℕ) → List Turing.PartrecToTM2.Γ'

Lists of lists are translated with a consₗ after each encoded list. For example:

[] = []
[[]] = [consₗ]
[[], []] = [consₗ, consₗ]
[[0]] = [cons, consₗ]
[[1, 2], [0]] = [bit1, cons, bit0, bit1, cons, consₗ, cons, consₗ]

Equations

• Turing.PartrecToTM2.trLList [] = []
• Turing.PartrecToTM2.trLList (l :: ls) = Turing.PartrecToTM2.trList l ++ Turing.PartrecToTM2.Γ'.consₗ :: Turing.PartrecToTM2.trLList ls

def Turing.PartrecToTM2.contStack : Turing.ToPartrec.Cont → List (List ℕ)

The data part of a continuation is a list of lists, which is encoded on the stack stack using trLList.

Equations

• Turing.PartrecToTM2.contStack Turing.ToPartrec.Cont.halt = []
• Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.cons₁ fs as k) = as :: Turing.PartrecToTM2.contStack k
• Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.cons₂ ns k) = ns :: Turing.PartrecToTM2.contStack k
• Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.comp f k) = Turing.PartrecToTM2.contStack k
• Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.fix f k) = Turing.PartrecToTM2.contStack k

def Turing.PartrecToTM2.trContStack (k : Turing.ToPartrec.Cont) : List Turing.PartrecToTM2.Γ'

The data part of a continuation is a list of lists, which is encoded on the stack stack using trLList.

Equations

• Turing.PartrecToTM2.trContStack k = Turing.PartrecToTM2.trLList (Turing.PartrecToTM2.contStack k)

def Turing.PartrecToTM2.K'.elim (a b c d : List Turing.PartrecToTM2.Γ') : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'

This is the nondependent eliminator for K', but we use it specifically here in order to represent the stack data as four lists rather than as a function K' → List Γ', because this makes rewrites easier. The theorems K'.elim_update_main et. al. show how such a function is updated after an update to one of the components.

Equations

• Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.main = a
• Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.rev = b
• Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.aux = c
• Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.stack = d

theorem Turing.PartrecToTM2.K'.elim_main (a b c d : List Turing.PartrecToTM2.Γ') : Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.main = a

theorem Turing.PartrecToTM2.K'.elim_rev (a b c d : List Turing.PartrecToTM2.Γ') : Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.rev = b

theorem Turing.PartrecToTM2.K'.elim_aux (a b c d : List Turing.PartrecToTM2.Γ') : Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.aux = c

theorem Turing.PartrecToTM2.K'.elim_stack (a b c d : List Turing.PartrecToTM2.Γ') : Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.stack = d

@[simp]

theorem Turing.PartrecToTM2.K'.elim_update_main {a b c d a' : List Turing.PartrecToTM2.Γ'} : Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.main a' = Turing.PartrecToTM2.K'.elim a' b c d

@[simp]

theorem Turing.PartrecToTM2.K'.elim_update_rev {a b c d b' : List Turing.PartrecToTM2.Γ'} : Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.rev b' = Turing.PartrecToTM2.K'.elim a b' c d

@[simp]

theorem Turing.PartrecToTM2.K'.elim_update_aux {a b c d c' : List Turing.PartrecToTM2.Γ'} : Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.aux c' = Turing.PartrecToTM2.K'.elim a b c' d

@[simp]

theorem Turing.PartrecToTM2.K'.elim_update_stack {a b c d d' : List Turing.PartrecToTM2.Γ'} : Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.stack d' = Turing.PartrecToTM2.K'.elim a b c d'

def Turing.PartrecToTM2.halt (v : List ℕ) : Turing.PartrecToTM2.Cfg'

The halting state corresponding to a List ℕ output value.

Equations

• Turing.PartrecToTM2.halt v = { l := none, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] [] }

def Turing.PartrecToTM2.TrCfg : Turing.ToPartrec.Cfg → Turing.PartrecToTM2.Cfg' → Prop

The Cfg states map to Cfg' states almost one to one, except that in normal operation the local store contains an arbitrary garbage value. To make the final theorem cleaner we explicitly clear it in the halt state so that there is exactly one configuration corresponding to output v.

Equations

• One or more equations did not get rendered due to their size.
• Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.Cfg.halt v) x✝ = (x✝ = Turing.PartrecToTM2.halt v)

def Turing.PartrecToTM2.splitAtPred {α : Type u_1} (p : α → Bool) : List α → List α × Option α × List α

This could be a general list definition, but it is also somewhat specialized to this application. splitAtPred p L will search L for the first element satisfying p. If it is found, say L = l₁ ++ a :: l₂ where a satisfies p but l₁ does not, then it returns (l₁, some a, l₂). Otherwise, if there is no such element, it returns (L, none, []).

Equations

• Turing.PartrecToTM2.splitAtPred p [] = ([], none, [])
• Turing.PartrecToTM2.splitAtPred p (a :: as) = bif p a then ([], some a, as) else match Turing.PartrecToTM2.splitAtPred p as with | (l₁, o, l₂) => (a :: l₁, o, l₂)

theorem Turing.PartrecToTM2.splitAtPred_eq {α : Type u_1} (p : α → Bool) (L l₁ : List α) (o : Option α) (l₂ : List α) : (∀ x ∈ l₁, p x = false) → Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) => p a = true ∧ L = l₁ ++ a :: l₂) o → Turing.PartrecToTM2.splitAtPred p L = (l₁, o, l₂)

theorem Turing.PartrecToTM2.splitAtPred_false {α : Type u_1} (L : List α) : Turing.PartrecToTM2.splitAtPred (fun (x : α) => false) L = (L, none, [])

theorem Turing.PartrecToTM2.move_ok {p : Turing.PartrecToTM2.Γ' → Bool} {k₁ k₂ : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {L₁ : List Turing.PartrecToTM2.Γ'} {o : Option Turing.PartrecToTM2.Γ'} {L₂ : List Turing.PartrecToTM2.Γ'} {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'} (h₁ : k₁ ≠ k₂) (e : Turing.PartrecToTM2.splitAtPred p (S k₁) = (L₁, o, L₂)) : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q), var := s, stk := S } { l := some q, var := o, stk := Function.update (Function.update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }

theorem Turing.PartrecToTM2.unrev_ok {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'} : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.unrev q), var := s, stk := S } { l := some q, var := none, stk := Function.update (Function.update S Turing.PartrecToTM2.K'.rev []) Turing.PartrecToTM2.K'.main ((S Turing.PartrecToTM2.K'.rev).reverseAux (S Turing.PartrecToTM2.K'.main)) }

theorem Turing.PartrecToTM2.move₂_ok {p : Turing.PartrecToTM2.Γ' → Bool} {k₁ k₂ : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {L₁ : List Turing.PartrecToTM2.Γ'} {o : Option Turing.PartrecToTM2.Γ'} {L₂ : List Turing.PartrecToTM2.Γ'} {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'} (h₁ : k₁ ≠ Turing.PartrecToTM2.K'.rev ∧ k₂ ≠ Turing.PartrecToTM2.K'.rev ∧ k₁ ≠ k₂) (h₂ : S Turing.PartrecToTM2.K'.rev = []) (e : Turing.PartrecToTM2.splitAtPred p (S k₁) = (L₁, o, L₂)) : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.move₂ p k₁ k₂ q), var := s, stk := S } { l := some q, var := none, stk := Function.update (Function.update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂) }

theorem Turing.PartrecToTM2.clear_ok {p : Turing.PartrecToTM2.Γ' → Bool} {k : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {L₁ : List Turing.PartrecToTM2.Γ'} {o : Option Turing.PartrecToTM2.Γ'} {L₂ : List Turing.PartrecToTM2.Γ'} {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'} (e : Turing.PartrecToTM2.splitAtPred p (S k) = (L₁, o, L₂)) : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.Λ'.clear p k q), var := s, stk := S } { l := some q, var := o, stk := Function.update S k L₂ }

theorem Turing.PartrecToTM2.copy_ok (q : Turing.PartrecToTM2.Λ') (s : Option Turing.PartrecToTM2.Γ') (a b c d : List Turing.PartrecToTM2.Γ') : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some q.copy, var := s, stk := Turing.PartrecToTM2.K'.elim a b c d } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (b.reverseAux a) [] c (b.reverseAux d) }

theorem Turing.PartrecToTM2.trPosNum_natEnd (n : PosNum) (x : Turing.PartrecToTM2.Γ') : x ∈ Turing.PartrecToTM2.trPosNum n → Turing.PartrecToTM2.natEnd x = false

theorem Turing.PartrecToTM2.trNum_natEnd (n : Num) (x : Turing.PartrecToTM2.Γ') : x ∈ Turing.PartrecToTM2.trNum n → Turing.PartrecToTM2.natEnd x = false

theorem Turing.PartrecToTM2.trNat_natEnd (n : ℕ) (x : Turing.PartrecToTM2.Γ') : x ∈ Turing.PartrecToTM2.trNat n → Turing.PartrecToTM2.natEnd x = false

theorem Turing.PartrecToTM2.trList_ne_consₗ (l : List ℕ) (x : Turing.PartrecToTM2.Γ') : x ∈ Turing.PartrecToTM2.trList l → x ≠ Turing.PartrecToTM2.Γ'.consₗ

theorem Turing.PartrecToTM2.head_main_ok {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {L : List ℕ} {c d : List Turing.PartrecToTM2.Γ'} : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.main q), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList L) [] c d } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [L.headI]) [] c d }

theorem Turing.PartrecToTM2.head_stack_ok {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {L₁ L₂ : List ℕ} {L₃ : List Turing.PartrecToTM2.Γ'} : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack q), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList L₁) [] [] (Turing.PartrecToTM2.trList L₂ ++ Turing.PartrecToTM2.Γ'.consₗ :: L₃) } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList (L₂.headI :: L₁)) [] [] L₃ }

theorem Turing.PartrecToTM2.succ_ok {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {n : ℕ} {c d : List Turing.PartrecToTM2.Γ'} : Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some q.succ, var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [n]) [] c d } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [n.succ]) [] c d }

theorem Turing.PartrecToTM2.pred_ok (q₁ q₂ : Turing.PartrecToTM2.Λ') (s : Option Turing.PartrecToTM2.Γ') (v : List ℕ) (c d : List Turing.PartrecToTM2.Γ') : ∃ (s' : Option Turing.PartrecToTM2.Γ'), Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (q₁.pred q₂), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] c d } (Nat.rec { l := some q₁, var := s', stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v.tail) [] c d } (fun (n : ℕ) (x : Turing.TM2.Cfg (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')) => { l := some q₂, var := s', stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList (n :: v.tail)) [] c d }) v.headI)

theorem Turing.PartrecToTM2.trNormal_respects (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont) (v : List ℕ) (s : Option Turing.PartrecToTM2.Γ') : ∃ (b₂ : Turing.PartrecToTM2.Cfg'), Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepNormal c k v) b₂ ∧ Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.trNormal c (Turing.PartrecToTM2.trCont k)), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] (Turing.PartrecToTM2.trContStack k) } b₂

theorem Turing.PartrecToTM2.tr_ret_respects (k : Turing.ToPartrec.Cont) (v : List ℕ) (s : Option Turing.PartrecToTM2.Γ') : ∃ (b₂ : Turing.PartrecToTM2.Cfg'), Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepRet k v) b₂ ∧ Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.trCont k)), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] (Turing.PartrecToTM2.trContStack k) } b₂

theorem Turing.PartrecToTM2.tr_respects : Turing.Respects Turing.ToPartrec.step (Turing.TM2.step Turing.PartrecToTM2.tr) Turing.PartrecToTM2.TrCfg

def Turing.PartrecToTM2.init (c : Turing.ToPartrec.Code) (v : List ℕ) : Turing.PartrecToTM2.Cfg'

The initial state, evaluating function c on input v.

Equations

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

theorem Turing.PartrecToTM2.tr_init (c : Turing.ToPartrec.Code) (v : List ℕ) : ∃ (b : Turing.PartrecToTM2.Cfg'), Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) b ∧ Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c v) b

theorem Turing.PartrecToTM2.tr_eval (c : Turing.ToPartrec.Code) (v : List ℕ) : Turing.eval (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c v) = Turing.PartrecToTM2.halt <$> c.eval v

def Turing.PartrecToTM2.trStmts₁ : Turing.PartrecToTM2.Λ' → Finset Turing.PartrecToTM2.Λ'

The set of machine states reachable via downward label jumps, discounting jumps via ret.

Equations

• One or more equations did not get rendered due to their size.
• Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) = insert (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) (Turing.PartrecToTM2.trStmts₁ q)
• Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.push k s q) = insert (Turing.PartrecToTM2.Λ'.push k s q) (Turing.PartrecToTM2.trStmts₁ q)
• Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.clear p k q) = insert (Turing.PartrecToTM2.Λ'.clear p k q) (Turing.PartrecToTM2.trStmts₁ q)
• Turing.PartrecToTM2.trStmts₁ q.copy = insert q.copy (Turing.PartrecToTM2.trStmts₁ q)
• Turing.PartrecToTM2.trStmts₁ q.succ = insert q.succ (insert (Turing.PartrecToTM2.unrev q) (Turing.PartrecToTM2.trStmts₁ q))
• Turing.PartrecToTM2.trStmts₁ (q₁.pred q₂) = insert (q₁.pred q₂) (Turing.PartrecToTM2.trStmts₁ q₁ ∪ insert (Turing.PartrecToTM2.unrev q₂) (Turing.PartrecToTM2.trStmts₁ q₂))
• Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.ret k) = {Turing.PartrecToTM2.Λ'.ret k}

theorem Turing.PartrecToTM2.trStmts₁_trans {q q' : Turing.PartrecToTM2.Λ'} : q' ∈ Turing.PartrecToTM2.trStmts₁ q → Turing.PartrecToTM2.trStmts₁ q' ⊆ Turing.PartrecToTM2.trStmts₁ q

theorem Turing.PartrecToTM2.trStmts₁_self (q : Turing.PartrecToTM2.Λ') : q ∈ Turing.PartrecToTM2.trStmts₁ q

def Turing.PartrecToTM2.codeSupp' : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Finset Turing.PartrecToTM2.Λ'

The (finite!) set of machine states visited during the course of evaluation of c, including the state ret k but not any states after that (that is, the states visited while evaluating k).

Equations

• One or more equations did not get rendered due to their size.
• Turing.PartrecToTM2.codeSupp' Turing.ToPartrec.Code.zero' x✝ = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.zero' x✝)
• Turing.PartrecToTM2.codeSupp' Turing.ToPartrec.Code.succ x✝ = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.succ x✝)
• Turing.PartrecToTM2.codeSupp' Turing.ToPartrec.Code.tail x✝ = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.tail x✝)

@[simp]

theorem Turing.PartrecToTM2.codeSupp'_self (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ⊆ Turing.PartrecToTM2.codeSupp' c k

def Turing.PartrecToTM2.contSupp : Turing.PartrecToTM2.Cont' → Finset Turing.PartrecToTM2.Λ'

The (finite!) set of machine states visited during the course of evaluation of a continuation k, not including the initial state ret k.

Equations

• One or more equations did not get rendered due to their size.
• Turing.PartrecToTM2.contSupp k.cons₂ = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪ Turing.PartrecToTM2.contSupp k
• Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.comp f k) = Turing.PartrecToTM2.codeSupp' f k ∪ Turing.PartrecToTM2.contSupp k
• Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.fix f k) = Turing.PartrecToTM2.codeSupp' f.fix k ∪ Turing.PartrecToTM2.contSupp k
• Turing.PartrecToTM2.contSupp Turing.PartrecToTM2.Cont'.halt = ∅

def Turing.PartrecToTM2.codeSupp (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Finset Turing.PartrecToTM2.Λ'

The (finite!) set of machine states visited during the course of evaluation of c in continuation k. This is actually closed under forward simulation (see tr_supports), and the existence of this set means that the machine constructed in this section is in fact a proper Turing machine, with a finite set of states.

Equations

• Turing.PartrecToTM2.codeSupp c k = Turing.PartrecToTM2.codeSupp' c k ∪ Turing.PartrecToTM2.contSupp k

@[simp]

theorem Turing.PartrecToTM2.codeSupp_self (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ⊆ Turing.PartrecToTM2.codeSupp c k

@[simp]

theorem Turing.PartrecToTM2.codeSupp_zero (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.zero' k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.zero' k) ∪ Turing.PartrecToTM2.contSupp k

@[simp]

theorem Turing.PartrecToTM2.codeSupp_succ (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.succ k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.succ k) ∪ Turing.PartrecToTM2.contSupp k

@[simp]

theorem Turing.PartrecToTM2.codeSupp_tail (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.tail k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.tail k) ∪ Turing.PartrecToTM2.contSupp k

@[simp]

theorem Turing.PartrecToTM2.codeSupp_cons (f fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.codeSupp (f.cons fs) k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.cons fs) k) ∪ Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.cons₁ fs k)

@[simp]

theorem Turing.PartrecToTM2.codeSupp_comp (f g : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.codeSupp (f.comp g) k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.comp g) k) ∪ Turing.PartrecToTM2.codeSupp g (Turing.PartrecToTM2.Cont'.comp f k)

@[simp]

theorem Turing.PartrecToTM2.codeSupp_case (f g : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.codeSupp (f.case g) k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.case g) k) ∪ (Turing.PartrecToTM2.codeSupp f k ∪ Turing.PartrecToTM2.codeSupp g k)

@[simp]

theorem Turing.PartrecToTM2.codeSupp_fix (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.codeSupp f.fix k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal f.fix k) ∪ Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.fix f k)

@[simp]

theorem Turing.PartrecToTM2.contSupp_cons₁ (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.cons₁ fs k) = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.move₂ (fun (x : Turing.PartrecToTM2.Γ') => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux (Turing.PartrecToTM2.move₂ (fun (s : Turing.PartrecToTM2.Γ') => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.move₂ (fun (x : Turing.PartrecToTM2.Γ') => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.trNormal fs k.cons₂)))) ∪ Turing.PartrecToTM2.codeSupp fs k.cons₂

@[simp]

theorem Turing.PartrecToTM2.contSupp_cons₂ (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.contSupp k.cons₂ = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪ Turing.PartrecToTM2.contSupp k

@[simp]

theorem Turing.PartrecToTM2.contSupp_comp (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.comp f k) = Turing.PartrecToTM2.codeSupp f k

theorem Turing.PartrecToTM2.contSupp_fix (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.fix f k) = Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.fix f k)

@[simp]

theorem Turing.PartrecToTM2.contSupp_halt : Turing.PartrecToTM2.contSupp Turing.PartrecToTM2.Cont'.halt = ∅

def Turing.PartrecToTM2.Λ'.Supports (S : Finset Turing.PartrecToTM2.Λ') : Turing.PartrecToTM2.Λ' → Prop

The statement Λ'.Supports S q means that contSupp k ⊆ S for any ret k reachable from q. (This is a technical condition used in the proof that the machine is supported.)

Equations

• Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) = Turing.PartrecToTM2.Λ'.Supports S q
• Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.push k s q) = Turing.PartrecToTM2.Λ'.Supports S q
• Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.read q) = ∀ (s : Option Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Λ'.Supports S (q s)
• Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.clear p k q) = Turing.PartrecToTM2.Λ'.Supports S q
• Turing.PartrecToTM2.Λ'.Supports S q.copy = Turing.PartrecToTM2.Λ'.Supports S q
• Turing.PartrecToTM2.Λ'.Supports S q.succ = Turing.PartrecToTM2.Λ'.Supports S q
• Turing.PartrecToTM2.Λ'.Supports S (q₁.pred q₂) = (Turing.PartrecToTM2.Λ'.Supports S q₁ ∧ Turing.PartrecToTM2.Λ'.Supports S q₂)
• Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.ret k) = (Turing.PartrecToTM2.contSupp k ⊆ S)

def Turing.PartrecToTM2.Supports (K S : Finset Turing.PartrecToTM2.Λ') : Prop

A shorthand for the predicate that we are proving in the main theorems trStmts₁_supports, codeSupp'_supports, contSupp_supports, codeSupp_supports. The set S is fixed throughout the proof, and denotes the full set of states in the machine, while K is a subset that we are currently proving a property about. The predicate asserts that every state in K is closed in S under forward simulation, i.e. stepping forward through evaluation starting from any state in K stays entirely within S.

Equations

• Turing.PartrecToTM2.Supports K S = ∀ q ∈ K, Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q)

theorem Turing.PartrecToTM2.supports_insert {K S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'} : Turing.PartrecToTM2.Supports (insert q K) S ↔ Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q) ∧ Turing.PartrecToTM2.Supports K S

theorem Turing.PartrecToTM2.supports_singleton {S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'} : Turing.PartrecToTM2.Supports {q} S ↔ Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q)

theorem Turing.PartrecToTM2.supports_union {K₁ K₂ S : Finset Turing.PartrecToTM2.Λ'} : Turing.PartrecToTM2.Supports (K₁ ∪ K₂) S ↔ Turing.PartrecToTM2.Supports K₁ S ∧ Turing.PartrecToTM2.Supports K₂ S

theorem Turing.PartrecToTM2.supports_biUnion {K : Option Turing.PartrecToTM2.Γ' → Finset Turing.PartrecToTM2.Λ'} {S : Finset Turing.PartrecToTM2.Λ'} : Turing.PartrecToTM2.Supports (Finset.univ.biUnion K) S ↔ ∀ (a : Option Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Supports (K a) S

theorem Turing.PartrecToTM2.head_supports {S : Finset Turing.PartrecToTM2.Λ'} {k : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'} (H : Turing.PartrecToTM2.Λ'.Supports S q) : Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.head k q)

theorem Turing.PartrecToTM2.ret_supports {S : Finset Turing.PartrecToTM2.Λ'} {k : Turing.PartrecToTM2.Cont'} (H₁ : Turing.PartrecToTM2.contSupp k ⊆ S) : Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k))

theorem Turing.PartrecToTM2.trStmts₁_supports {S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'} (H₁ : Turing.PartrecToTM2.Λ'.Supports S q) (HS₁ : Turing.PartrecToTM2.trStmts₁ q ⊆ S) : Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.trStmts₁ q) S

theorem Turing.PartrecToTM2.trStmts₁_supports' {S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'} {K : Finset Turing.PartrecToTM2.Λ'} (H₁ : Turing.PartrecToTM2.Λ'.Supports S q) (H₂ : Turing.PartrecToTM2.trStmts₁ q ∪ K ⊆ S) (H₃ : K ⊆ S → Turing.PartrecToTM2.Supports K S) : Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.trStmts₁ q ∪ K) S

theorem Turing.PartrecToTM2.trNormal_supports {S : Finset Turing.PartrecToTM2.Λ'} {c : Turing.ToPartrec.Code} {k : Turing.PartrecToTM2.Cont'} (Hk : Turing.PartrecToTM2.codeSupp c k ⊆ S) : Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.trNormal c k)

theorem Turing.PartrecToTM2.codeSupp'_supports {S : Finset Turing.PartrecToTM2.Λ'} {c : Turing.ToPartrec.Code} {k : Turing.PartrecToTM2.Cont'} (H : Turing.PartrecToTM2.codeSupp c k ⊆ S) : Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.codeSupp' c k) S

theorem Turing.PartrecToTM2.contSupp_supports {S : Finset Turing.PartrecToTM2.Λ'} {k : Turing.PartrecToTM2.Cont'} (H : Turing.PartrecToTM2.contSupp k ⊆ S) : Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.contSupp k) S

theorem Turing.PartrecToTM2.codeSupp_supports {S : Finset Turing.PartrecToTM2.Λ'} {c : Turing.ToPartrec.Code} {k : Turing.PartrecToTM2.Cont'} (H : Turing.PartrecToTM2.codeSupp c k ⊆ S) : Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.codeSupp c k) S

theorem Turing.PartrecToTM2.tr_supports (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont') : Turing.TM2.Supports Turing.PartrecToTM2.tr (Turing.PartrecToTM2.codeSupp c k)

The set codeSupp c k is a finite set that witnesses the effective finiteness of the tr Turing machine. Starting from the initial state trNormal c k, forward simulation uses only states in codeSupp c k, so this is a finite state machine. Even though the underlying type of state labels Λ' is infinite, for a given partial recursive function c and continuation k, only finitely many states are accessed, corresponding roughly to subterms of c.