mathlib3documentation

computability.tm_to_partrec

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.

@[protected, instance]
@[protected, instance]

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.

Instances for `turing.to_partrec.code`
@[simp]

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

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

Equations
@[simp]

`id` is the identity function: `id v = v`.

Equations
@[simp]

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

Equations
@[simp]

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

Equations
@[simp]

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

Equations
@[simp]

`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 (λ (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

`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
theorem turing.to_partrec.code.exists_code.comp {m n : } {f : n →. } {g : fin n m →. } (hf : (c : turing.to_partrec.code), (v : n), c.eval v.val = ) (hg : (i : fin n), (c : turing.to_partrec.code), (v : m), c.eval v.val = has_pure.pure <\$> g i v) :
(c : turing.to_partrec.code), (v : m), c.eval v.val = has_pure.pure <\$> (vector.m_of_fn (λ (i : fin n), g i v) >>= f)
theorem turing.to_partrec.code.exists_code {n : } {f : n →. } (hf : nat.partrec' f) :
(c : turing.to_partrec.code), (v : n), c.eval v.val =

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

@[protected, instance]

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

Instances for `turing.to_partrec.cont`

The semantics of a continuation.

Equations
@[protected, instance]
inductive turing.to_partrec.cfg  :
• halt :
• ret :

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 `step_normal` function.

Instances for `turing.to_partrec.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.head.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).head :: fs v` requires two sub-evaluations, so we evaluate `f v` in the continuation `k (_.head :: 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.cases_on (f v.tail) (λ 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 in if v'.head = 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

Evaluating a continuation `k : cont` on input `v : list ℕ`. This is the second part of evaluation, when we receive results from continuations built by `step_normal`.

• `cont.halt v = v`, so we are done and transition to the `cfg.halt v` state
• `cont.cons₁ fs as k v = k (v.head :: fs as)`, so we evaluate `fs as` now with the continuation `k (v.head :: _)` (called `cons₂ v k`).
• `cont.cons₂ ns k v = k (ns.head :: v)`, where we now have everything we need to evaluate `ns.head :: 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.head = 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

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

Equations

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

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
• k' = v

The `step_normal` 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.

The `step_ret` 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.

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 (step_normal 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 `step_normal c cont.halt v` evaluates to `cfg.halt (code.eval c v)`.

Equations
theorem turing.to_partrec.code.ok.zero (h : c.ok) {v : list } :
theorem turing.to_partrec.cont_eval_fix {v : list } (fok : f.ok) :
= f.fix.eval v >>= λ (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'`.

@[protected, instance]
@[protected, instance]
@[protected, instance]

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.

Instances for `turing.partrec_to_TM2.Γ'`

The four stacks used by the program. `main` is used to store the input value in `tr_normal` 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.

Instances for `turing.partrec_to_TM2.K'`
@[protected, instance]
@[protected, instance]

Continuations as in `to_partrec.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.

Instances for `turing.partrec_to_TM2.cont'`
@[protected, instance]
@[protected, instance]

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.

Instances for `turing.partrec_to_TM2.Λ'`
@[protected, instance]
Equations
@[protected, instance]
Equations

The type of TM2 statements used by this machine.

Equations
Instances for `turing.partrec_to_TM2.stmt'`
@[protected, instance]
@[protected, instance]

The type of TM2 configurations used by this machine.

Equations
Instances for `turing.partrec_to_TM2.cfg'`
@[simp]

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
@[simp]

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

Equations
• = (λ (x v : , v)
@[simp]

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

Equations
• = (λ (x v : , v)
@[simp]

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

Equations

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

Equations

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

Equations
• q =

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

Equations

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

Equations
@[simp]

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

Equations
@[simp]

The main program. See the section documentation for details.

Equations

Translating a `cont` continuation to a `cont'` continuation simply entails dropping all the data. This data is instead encoded in `tr_cont_stack` in the configuration.

Equations

We use `pos_num` 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

We use `num` to define the translation of binary natural numbers. Positive numbers are translated using `tr_pos_num`, and `tr_num 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

Because we use binary encoding, we define `tr_nat` in terms of `tr_num`, using `num`, which are binary natural numbers. (We could also use `nat.binary_rec_on`, but `num` and `pos_num` make for easy inductions.)

Equations
@[simp]
@[simp]

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
@[simp]

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
@[simp]

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

Equations

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

Equations
@[simp]

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

The halting state corresponding to a `list ℕ` output value.

Equations

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
def turing.partrec_to_TM2.split_at_pred {α : Type u_1} (p : α bool) :
list α list α × × list α

This could be a general list definition, but it is also somewhat specialized to this application. `split_at_pred 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
• = cond (p a) (list.nil α, , as) (turing.partrec_to_TM2.split_at_pred._match_1 a
• turing.partrec_to_TM2.split_at_pred._match_1 a (l₁, o, l₂) = (a :: l₁, o, l₂)
theorem turing.partrec_to_TM2.split_at_pred_eq {α : Type u_1} (p : α bool) (L l₁ : list α) (o : option α) (l₂ : list α) :
( (x : α), x l₁ p x = bool.ff) option.elim (L = l₁ l₂ = list.nil) (λ (a : α), p a = bool.tt L = l₁ ++ a :: l₂) o = (l₁, o, l₂)
theorem turing.partrec_to_TM2.move_ok {k₁ k₂ : turing.partrec_to_TM2.K'} (h₁ : k₁ k₂) (e : = (L₁, o, L₂)) :
{l := option.some k₂ q), var := s, stk := S} {l := , var := o, stk := function.update k₁ L₂) k₂ (L₁.reverse_core (S k₂))}
theorem turing.partrec_to_TM2.move₂_ok {k₁ k₂ : turing.partrec_to_TM2.K'} (h₁ : k₁ k₂) (e : = (L₁, o, L₂)) :
{l := option.some k₂ q), var := s, stk := S} {l := , var := , stk := function.update k₁ L₂)) k₂ (L₁ ++ S k₂)}
theorem turing.partrec_to_TM2.clear_ok (e : = (L₁, o, L₂)) :
{l := , var := s, stk := S} {l := , var := o, stk := L₂}
theorem turing.partrec_to_TM2.copy_ok (a b c d : list turing.partrec_to_TM2.Γ') :
{l := , var := s, stk := d} {l := , var := , stk := (b.reverse_core d)}
theorem turing.partrec_to_TM2.pred_ok (q₁ q₂ : turing.partrec_to_TM2.Λ') (v : list ) (c d : list turing.partrec_to_TM2.Γ') :
(s' : , {l := option.some (q₁.pred q₂), var := s, stk := (nat.elim {l := , var := s', stk := (λ (n : ) (_x : , {l := , var := s', stk := v.head)

The initial state, evaluating function `c` on input `v`.

Equations

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

Equations

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
@[simp]

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

Equations

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
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

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

Equations

A shorthand for the predicate that we are proving in the main theorems `tr_stmts₁_supports`, `code_supp'_supports`, `cont_supp_supports`, `code_supp_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
theorem turing.partrec_to_TM2.tr_stmts₁_supports' (H₁ : q) (H₂ : S) (H₃ : K S ) :

The set `code_supp c k` is a finite set that witnesses the effective finiteness of the `tr` Turing machine. Starting from the initial state `tr_normal c k`, forward simulation uses only states in `code_supp 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`.