Theorems · Definition · logic and foundations

Turing.ToPartrec.Code.prec

Turing.ToPartrec.Code → 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].

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

1 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms