Theorems · Definition · logic and foundations

Nat.Partrec.Code.eval

Nat.Partrec.Code → ℕ →. ℕ

The interpretation of a Nat.Partrec.Code as a partial function. * Nat.Partrec.Code.zero: The constant zero function. * Nat.Partrec.Code.succ: The successor function. * Nat.Partrec.Code.left: Left unpairing of a pair of ℕ (encoded by Nat.pair) * Nat.Partrec.Code.right: Right unpairing of a pair of ℕ (encoded by Nat.pair) * Nat.Partrec.Code.pair: Pairs the outputs of argument codes using Nat.pair. * Nat.Partrec.Code.comp: Composition of two argument codes. * Nat.Partrec.Code.prec: Primitive recursion. Given an argument of the form Nat.pair a n: * If n = 0, returns eval cf a. * If n = succ k, returns eval cg (pair a (pair k (eval (prec cf cg) (pair a k)))) * Nat.Partrec.Code.rfind': Minimization starting at a provided value. Given an argument of the form Nat.pair a m, returns the least n ≥ m such that eval cf (pair a n) = 0, if such an n exists and if eval cf (pair a k) terminates for all m ≤ k ≤ n.

Defined in

Mathlib.Computability.PartrecCode

Cited by

25 results in Mathlib

Foundations

Depth 26 from the axioms · uses no axioms