English
If f is Partrec, then PFun.fix f is Partrec.
Русский
Если f частично вычислима, то PFun.fix f частично вычислима.
LaTeX
$$$\mathrm{Partrec}(f) \Rightarrow \mathrm{Partrec}(\mathrm{PFun}.fix f)$$$
Lean4
theorem fix {f : α →. σ ⊕ α} (hf : Partrec f) : Partrec (PFun.fix f) :=
by
let F : α → ℕ →. σ ⊕ α := fun a n =>
n.rec (some (Sum.inr a)) fun _ IH => IH.bind fun s => Sum.casesOn s (fun _ => Part.some s) f
have hF : Partrec₂ F :=
Partrec.nat_rec snd (sumInr.comp fst).partrec
(sumCasesOn_right (snd.comp snd) (snd.comp <| snd.comp fst).to₂ (hf.comp snd).to₂).to₂
let p a n := @Part.map _ Bool (fun s => Sum.casesOn s (fun _ => true) fun _ => false) (F a n)
have hp : Partrec₂ p := hF.map ((sumCasesOn Computable.id (const true).to₂ (const false).to₂).comp snd).to₂
exact
((Partrec.rfind hp).bind (hF.bind (sumCasesOn_right snd snd.to₂ none.to₂).to₂).to₂).of_eq fun a =>
ext fun b => by simpa [p] using fix_aux f _ _
