English
Primitive recursion yields a partial recursive function: given computable f, partial g and 2-ary h, the recursion a ↦ (f a).rec (g a) (λ y IH. IH.bind (λ i. h a (y,i))) is partial recursive.
Русский
Прямая рекурсия даёт частично рекурсивную функцию: если f вычислима, g частично рекурсивна и h — частично рекурсивна на парах, то рекурсивная схема задаётся частично рекурсивной.
LaTeX
$$$\forall f,g,h,\ hf:Computable(f),\ hg:Partrec(g),\ hh:Partrec_2(h),\ Partrec(\lambda a. (f(a)).rec (g(a)) (\lambda y IH. IH.bind(\lambda i. h(a,(y,i)))))$$$
Lean4
theorem nat_rec {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ} (hf : Computable f) (hg : Partrec g) (hh : Partrec₂ h) :
Partrec fun a => (f a).rec (g a) fun y IH => IH.bind fun i => h a (y, i) :=
(Nat.Partrec.prec' hf hg hh).of_eq fun n =>
by
rcases e : decode (α := α) n with - | a <;> simp [e]
induction f a with simp
| succ m IH
rw [IH, Part.bind_map]
congr; funext s
simp [encodek]
