Теорема Клини

Лемма

Примитивные функции лямбда-определимы.

Доказательство

• U^p_j ≡ λx₀x₁...x_p.x_j
• S ≡ Suc ≡ λx y z.y (x y z)
• Z ≡ λx.⌈0⌉ ≡ λx.(λf x.x)

Лемма

Класс лямбда-определимых функций замкнут относительно композиции, примитивной рекурсии и минимизации.

Теорема Клини

Лямбда-определимые числовые функции — это в точности частично-рекурсивные функции.