Комбинáторная полнота

Теорема. Для каждого лямбда-терма существует эквивалент без λ-абстракций с теми же свободными переменными, записанный с помощью комбинаторов.

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

Достаточно найти комбинаторное выражение для произвольного λx. w, где w не содержит абстрактора λ. Тогда мы сможем применить такую процедуру к самым внутренним абстракциям снизу-вверх.

Что дают комбинаторы

  1. освободиться от λ-абстракций,
  2. избежать захвата переменной.