English
There exists a computable function f: Code → ℕ → Code such that eval (f c n) x = eval c (pair n x) for all c, n, x.
Русский
Существует вычислимая функция f: Code → ℕ → Code такая, что eval (f c n) x = eval c (pair n x) для всех c, n, x.
LaTeX
$$$\\exists f:\\, Code \\to\\mathbb{N} \\to Code,\\;\\mathrm{Computable}_2 f \\wedge \\forall c\\,\\forall n\\,\\forall x,\\ \\mathrm{eval}(f\\ c\\ n)\\ x = \\mathrm{eval}\\ c\\ (\\mathrm{pair}(n,x))$$$
Lean4
/-- **Roger's fixed-point theorem**: any total, computable `f` has a fixed point.
That is, under the interpretation given by `Nat.Partrec.Code.eval`, there is a code `c`
such that `c` and `f c` have the same evaluation.
-/
theorem fixed_point {f : Code → Code} (hf : Computable f) : ∃ c : Code, eval (f c) = eval c :=
let g (x y : ℕ) : Part ℕ := eval (ofNat Code x) x >>= fun b => eval (ofNat Code b) y
have : Partrec₂ g :=
(eval_part.comp ((Computable.ofNat _).comp fst) fst).bind
(eval_part.comp ((Computable.ofNat _).comp snd) (snd.comp fst)).to₂
let ⟨cg, eg⟩ := exists_code.1 this
have eg' : ∀ a n, eval cg (Nat.pair a n) = Part.map encode (g a n) := by simp [eg]
let F (x : ℕ) : Code := f (curry cg x)
have : Computable F := hf.comp (primrec₂_curry.comp (_root_.Primrec.const cg) _root_.Primrec.id).to_comp
let ⟨cF, eF⟩ := exists_code.1 this
have eF' : eval cF (encode cF) = Part.some (encode (F (encode cF))) := by simp [eF]
⟨curry cg (encode cF),
funext fun n =>
show eval (f (curry cg (encode cF))) n = eval (curry cg (encode cF)) n by simp [F, g, eg', eF', Part.map_id']⟩
