English
There is a bounded, option-valued evaluation evaln: ℕ → Code → ℕ → Option ℕ, defined by a finite set of recursive clauses (zero, succ, left, right, pair, comp, prec, rfind') that halts with a value when allowed by the bound.
Русский
Существует ограниченная по границе вычислительная функция evaln: ℕ × Code × ℕ → Option ℕ, определённая указанными рекурсивными правилами (zero, succ, left, right, pair, comp, prec, rfind'), которая возвращает значение, если вычисление завершилось в рамках границы.
LaTeX
$$$\\mathrm{def}\\;\\mathrm{evaln}:\\mathbb{N} \\to Code \\to \\mathbb{N} \\to \\mathrm{Option}\\mathbb{N}\\;|\\;0,\\;k+1,\\;\\text{zero},\\;\\text{succ},\\;\\text{left},\\;\\text{right},\\;\\text{pair},\\;\\text{comp},\\;\\text{prec},\\;\\text{rfind'}$$$
Lean4
/-- A modified evaluation for the code which returns an `Option ℕ` instead of a `Part ℕ`. To avoid
undecidability, `evaln` takes a parameter `k` and fails if it encounters a number ≥ k in the course
of its execution. Other than this, the semantics are the same as in `Nat.Partrec.Code.eval`.
-/
def evaln : ℕ → Code → ℕ → Option ℕ
| 0, _ => fun _ => Option.none
| k + 1, zero => fun n => do
guard (n ≤ k)
return 0
| k + 1, succ => fun n => do
guard (n ≤ k)
return (Nat.succ n)
| k + 1, left => fun n => do
guard (n ≤ k)
return n.unpair.1
| k + 1, right => fun n => do
guard (n ≤ k)
pure n.unpair.2
| k + 1, pair cf cg => fun n => do
guard (n ≤ k)
Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n
| k + 1, comp cf cg => fun n => do
guard (n ≤ k)
let x ← evaln (k + 1) cg n
evaln (k + 1) cf x
| k + 1, prec cf cg => fun n => do
guard (n ≤ k)
n.unpaired fun a n =>
n.casesOn (evaln (k + 1) cf a) fun y => do
let i ← evaln k (prec cf cg) (Nat.pair a y)
evaln (k + 1) cg (Nat.pair a (Nat.pair y i))
| k + 1, rfind' cf => fun n => do
guard (n ≤ k)
n.unpaired fun a m => do
let x ← evaln (k + 1) cf (Nat.pair a m)
if x = 0 then
pure m
else
evaln k (rfind' cf) (Nat.pair a (m + 1))
