English
The ability to compute a function f via decoding from natural numbers is equivalent to computing f directly, under suitable encodings.
Русский
Возможность вычисления функции f через декодирование из чисел равносильна вычислению самой функции f напрямую при подходящих кодировках.
LaTeX
$$$\mathrm{Computable}\; (f : \alpha \to \beta \to \mathrm{Option} \sigma) \iff \mathrm{Computable}_2 f$$$
Lean4
theorem bind_decode_iff {f : α → β → Option σ} :
(Computable₂ fun a n => (decode (α := β) n).bind (f a)) ↔ Computable₂ f :=
⟨fun hf =>
Nat.Partrec.of_eq
(((Partrec.nat_iff.2 (Nat.Partrec.ppred.comp <| Nat.Partrec.of_primrec <| Primcodable.prim (α := β))).comp
snd).bind
(Computable.comp hf fst).to₂.partrec₂)
fun n =>
by
simp only [decode_prod_val, decode_nat, Option.map_some, PFun.coe_val, bind_eq_bind, bind_some, Part.map_bind,
map_some]
cases decode (α := α) n.unpair.1 <;> simp
cases decode (α := β) n.unpair.2 <;> simp,
fun hf =>
by
have :
Partrec fun a : α × ℕ =>
(encode (decode (α := β) a.2)).casesOn (some Option.none) fun n => Part.map (f a.1) (decode (α := β) n) :=
Partrec.nat_casesOn_right (h := fun (a : α × ℕ) (n : ℕ) ↦ map (fun b ↦ f a.1 b) (Part.ofOption (decode n)))
(Primrec.encdec.to_comp.comp snd) (const Option.none)
((ofOption (Computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)
refine this.of_eq fun a => ?_
simp; cases decode (α := β) a.2 <;> simp [encodek]⟩
