Теорема о рекурсии

Для любого лямбда-терма g найдётся терм a, такой что a = g[x := a] для некоторой переменной x.

∀ g ∃ a : a = g[x := a].

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

Положим, a — неподвижная точка терма λx.g

Можно определять лямбда-термы через самих себя с помощью уравнения с рекурсии. Это наводит на мысль, что есть способ кодирования частично-рекурсивных функций на языке лямбда-исчисления.