Modelling partial recursive functions using Turing machines #

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

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 #

• to_partrec.code: a simplified basis for partial recursive functions, valued in list ℕ →. list ℕ.
  • to_partrec.code.eval: semantics for a to_partrec.code program
• partrec_to_TM2.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.cases_on).
  • 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.

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.head :: _). (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 _.head = 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 step_normal c halt v steps to v' in finitely many steps if and only if code.eval c v = some 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.turing_machine 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 :: k_data on stack and ns on main, and the next step expects v on main and ns :: k_data 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 :: k_data is on stack and v is on main, and we have to put ns.head :: v on main and k_data 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 ff rev main to move everything from rev back to main. Used as a cleanup operation in several functions.
• move_excl 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 move_excl p k rev; move ff 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.head] will be on main after; and also with k = stack for the cons operation, which has v on main and ns :: k_data on stack, and results in k_data on stack and ns.head :: v on main.
• tr_normal 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'.