Modelling partial recursive functions using Turing machines

The files TMConfig and TMToPartrec define 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

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' : Code
• succ : Code
• tail : Code
• cons : Code → Code → Code
• comp : Code → Code → Code
• case : Code → Code → Code
• fix : Code → Code

instance Turing.ToPartrec.instDecidableEqCode : DecidableEq Code

Equations

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

instance Turing.ToPartrec.instInhabitedCode : Inhabited Code

Equations

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

def Turing.ToPartrec.Code.eval : 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 : zero'.eval = fun (v : List ℕ) => pure (0 :: v)

@[simp]

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

@[simp]

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

@[simp]

theorem Turing.ToPartrec.Code.cons_eval (f fs : 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 : Code) : (f.comp g).eval = fun (v : List ℕ) => g.eval v >>= f.eval

@[simp]

theorem Turing.ToPartrec.Code.case_eval (f g : 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 : 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 : 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 ℕ) : nil.eval v = pure []

def Turing.ToPartrec.Code.id : 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 ℕ) : id.eval v = pure v

def Turing.ToPartrec.Code.head : 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 ℕ) : head.eval v = pure [v.headI]

def Turing.ToPartrec.Code.zero : 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 ℕ) : zero.eval v = pure [0]

def Turing.ToPartrec.Code.pred : 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 ℕ) : pred.eval v = pure [v.headI.pred]

def Turing.ToPartrec.Code.rfind (f : Code) : 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 : Code) : 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 : Code), ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v) (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) : ∃ (c : 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 : 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 : Cont
• cons₁ : Code → List ℕ → Cont → Cont
• cons₂ : List ℕ → Cont → Cont
• comp : Code → Cont → Cont
• fix : Code → Cont → Cont

instance Turing.ToPartrec.instInhabitedCont : Inhabited Cont

Equations

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

def Turing.ToPartrec.Cont.eval : 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 ℕ → Cfg
• ret : Cont → List ℕ → Cfg

instance Turing.ToPartrec.instInhabitedCfg : Inhabited Cfg

Equations

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

def Turing.ToPartrec.stepNormal : Code → Cont → List ℕ → 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 : Cont → List ℕ → 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 : Cfg → Option 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 : Cont → Cont → 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' : Cont} {v : List ℕ} : (k.then k').eval v = k.eval v >>= k'.eval

def Turing.ToPartrec.Cfg.then : Cfg → Cont → 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 : Code) (k k' : Cont) (v : List ℕ) : stepNormal c (k.then k') v = (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' : Cont} {v : List ℕ} : stepRet (k.then k') v = (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 : 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 : Code} (h : c.Ok) {v : List ℕ} : Turing.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

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

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

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

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

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