fixed_point₂ — Mathlib

English

Kleene's second recursion theorem: for any total computable f, there exists c such that eval c = f c.

Русский

Теорема о второй рекурсии Клейна: для любой полной вычислимой функции f существует код c, такой что eval c = f c.

LaTeX

$$$\\forall f:\\ Code \\rightarrow Code,\\; (Computable\\ f) \\rightarrow \\exists c:\\; eval\\ c = f\\ c$$$

Lean4

/-- **Kleene's second recursion theorem** -/
theorem fixed_point₂ {f : Code → ℕ →. ℕ} (hf : Partrec₂ f) : ∃ c : Code, eval c = f c :=
  let ⟨cf, ef⟩ := exists_code.1 hf
  (fixed_point (primrec₂_curry.comp (_root_.Primrec.const cf) Primrec.encode).to_comp).imp fun c e =>
    funext fun n => by simp [e.symm, ef, Part.map_id']

Похожие утверждения