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

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

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

Определим конструктивно процедуру COMB, которая по произвольному терму строит соответствующее комбинаторное выражение.

Если терм u не содержит абстрактора λ, очевидно
  COMB(u) ≡ u.

Для произвольного терма вида λx. w процедура определим индуктивно по построению терма.

• Пусть w - переменная. Тогда
  если w ≡ x, то COMB(λx. x) ≡ I;
  если w ≡ y (x y), то COMB(λx. y) ≡ К y.
• Пусть w - аппликация, т.е. w ≡ u v.
  Тогда по предположению индукции существуют термы u' и v' без абстрактора, такие что u' ≡ COMB(λx.u) и v' ≡ COMB(λx.v).
  Положим COMB(λx.u v) ≡ Su' v'.

Пример

• Найдём комбинаторное выражение для λx.(x y).
• COMB(x) = I, COMB(y) = Ky
• COMB(λx.(x y)) = S I (Ky)

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

1. освободиться от λ-абстракций,
2. избежать захвата переменной,
3. развивать комбинаторную алгебру упрощения комбинаторных выражений, например:
   ∀ f : I f = f
   S K K = I