English
Let α and σ be types with effective encodings. For any partial function f from α to σ, f is partial-recursive if and only if the function n ↦ Part.bind(decode2 α n) (λ a, encode(f a)) is Nat-partial-recursive.
Русский
Пусть α и σ — типы с эффективной кодировкой. Для любой частично определимой функции f : α → σ верно, что f частично вычислима тогда и только тогда функция n ↦ Part.bind(decode2 α n) (λ a, encode(f a)) является Nat-чрезвычайно вычислимой.
LaTeX
$$$\mathrm{Partrec}(f) \iff \mathrm{Nat.Partrec}\Bigl( n \mapsto \mathrm{Part.bind}\big(\decode_2^{\alpha} n\big)\big(\lambda a. \mathrm{encode}(f(a))\big) \Bigr)$$$
Lean4
theorem bind_decode₂_iff {f : α →. σ} :
Partrec f ↔ Nat.Partrec fun n => Part.bind (decode₂ α n) fun a => (f a).map encode :=
⟨fun hf =>
nat_iff.1 <|
(Computable.ofOption Primrec.decode₂.to_comp).bind <| (map hf (Computable.encode.comp snd).to₂).comp snd,
fun h => map_encode_iff.1 <| by simpa [encodek₂] using (nat_iff.2 h).comp (@Computable.encode α _)⟩
