to_comp

Mathlib.Computability.Partrec

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

English

If f is Primrec₂, then f is computable.

Русский

Если f — примитивно-рекурсивная функция двух аргументов, то она вычисуема.

LaTeX

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

Lean4

nonrec theorem to_comp {α β σ} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (hf : Primrec₂ f) :
    Computable₂ f :=
  hf.to_comp

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

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

Разделы

Аффилиация

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