to_comp

Mathlib.Computability.Partrec

URI: https://scilib.ai/kg/mathlib#Primrec.to_comp

← MathLib Explorer

English

If f is Primrec, then f is computable.

Русский

Если f примитивно-рекурсивна, то она вычисуема.

LaTeX

$$$\text{Primrec } f \Rightarrow \text{Computable } f$$$

Lean4

theorem to_comp {α σ} [Primcodable α] [Primcodable σ] {f : α → σ} (hf : Primrec f) : Computable f :=
  (Nat.Partrec.ppred.comp (Nat.Partrec.of_primrec hf)).of_eq fun n => by simp; cases decode (α := α) n <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru