English
A function f : ℕ ⇀ ℕ is partial recursive if and only if there exists a Code c with eval c = f.
Русский
Функция f: ℕ ⇀ ℕ частично рекурсивна тогда и только тогда, когда существует код c такой, что eval c = f.
LaTeX
$$$\\forall f:\\mathbb{N} \\to\\mathbb{N}\\!\\!\\!\\!\\,\\text{(partial)},\\; Nat.Partrec\\ f \\iff \\exists c:\\ Code, eval c = f$$$
Lean4
/-- A function is partial recursive if and only if there is a code implementing it. Therefore,
`eval` is a **universal partial recursive function**. -/
theorem exists_code {f : ℕ →. ℕ} : Nat.Partrec f ↔ ∃ c : Code, eval c = f :=
by
refine ⟨fun h => ?_, ?_⟩
·
induction h with
| zero => exact ⟨zero, rfl⟩
| succ => exact ⟨succ, rfl⟩
| left => exact ⟨left, rfl⟩
| right => exact ⟨right, rfl⟩
| pair pf pg hf hg =>
rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
exact ⟨pair cf cg, rfl⟩
| comp pf pg hf hg =>
rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
exact ⟨comp cf cg, rfl⟩
| prec pf pg hf hg =>
rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
exact ⟨prec cf cg, rfl⟩
| rfind pf hf =>
rcases hf with ⟨cf, rfl⟩
refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
· rintro ⟨c, rfl⟩
induction c with
| zero => exact Nat.Partrec.zero
| succ => exact Nat.Partrec.succ
| left => exact Nat.Partrec.left
| right => exact Nat.Partrec.right
| pair cf cg pf pg => exact pf.pair pg
| comp cf cg pf pg => exact pf.comp pg
| prec cf cg pf pg => exact pf.prec pg
| rfind' cf pf => exact pf.rfind'
