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

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

fa : a = f[x := a].

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

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

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