Theorems · Definition · logic and foundations

Turing.ToPartrec.Code.eval

Turing.ToPartrec.Code → List ℕ →. List ℕ

The semantics of the Code primitives, as partial functions List ℕ →. List ℕ. By convention, 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)

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

23 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms