English
The interpretation of Nat.Partrec.Code as a partial function: each code defines a partial function Nat →. Nat.
Русский
Интерпретация Nat.Partrec.Code как частичной функции: каждый код определяет частичную функцию Nat → Nat.
LaTeX
$$$\\mathrm{eval} : \\mathrm{Code} \\to \\mathbb{N} \\to^. \\mathbb{N}$$$
Lean4
/-- 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. For `f` an argument of the form `Nat.pair a m`,
`rfind' f m` returns the least `a` such that `f a m = 0`, if one exists and `f b m` terminates
for `b < a`
-/
def eval : Code → ℕ →. ℕ
| zero => pure 0
| succ => Nat.succ
| left => ↑fun n : ℕ => n.unpair.1
| right => ↑fun n : ℕ => n.unpair.2
| pair cf cg => fun n => Nat.pair <$> eval cf n <*> eval cg n
| comp cf cg => fun n => eval cg n >>= eval cf
| prec cf cg =>
Nat.unpaired fun a n =>
n.rec (eval cf a) fun y IH => do
let i ← IH
eval cg (Nat.pair a (Nat.pair y i))
| rfind' cf =>
Nat.unpaired fun a m => (Nat.rfind fun n => (fun m => m = 0) <$> eval cf (Nat.pair a (n + m))).map (· + m)
