SKI базис

Само λ-исчисление можно построить всего на трёх из них — S, K, I. В комбинаторной логике их берут за примитивы:

Причём I даже не обязателен как примитив — он выражается через S и K:

Давайте подставим и докажем формулу — раскроем $\mathrm{S}\,\mathrm{K}\,\mathrm{K}$ на произвольном аргументе $z$ по определениям (1.28):

На любом $z$ получаем $z$ — ровно то, что делает $\mathrm{I}$, значит $\mathrm{S}\,\mathrm{K}\,\mathrm{K} = \mathrm{I}$.

Любой λ-терм механически переводится в комбинаторы. Терм строится тремя способами — переменная, применение и абстракция; переменные и применение в комбинаторной логике уже есть, а вот абстракцию нужно устранить. Это делает bracket abstraction — операция $[x]\,M$, «вынести переменную $x$ из терма $M$». Её результат — комбинаторный терм, в котором $x$ уже не встречается, но который, если подать ему $x$ обратно, снова сводится к $M$. Определяется она по виду тела $M$:

• $[x]\,x = \mathrm{I}$: тело — это сама $x$; вернуть аргумент как есть умеет $\mathrm{I}$.
• $[x]\,M = \mathrm{K}\,M$ при $x \notin \mathrm{FV}(M)$: тело от $x$ не зависит, поэтому переданный аргумент надо просто выбросить.
• $[x]\,(M\,N) = \mathrm{S}\,([x]\,M)\,([x]\,N)$: в применении $x$ может прятаться и в $M$, и в $N$, поэтому аргумент нужно раздать обоим — этим и занимается $\mathrm{S}$.

Если же тело само — абстракция $\lambda y.\,M$, сперва убирают внутреннюю переменную, а потом внешнюю: $[x]\,(\lambda y.\,M) = [x]\,([y]\,M)$; так вложенные $\lambda$ снимаются изнутри наружу, пока не останутся только переменные и применения.

Разберём $\lambda x.\,f\,x\,x$. Тело $f\,x\,x$ — это применение $(f\,x)\,x$, так что раскручиваем правилом для применения, сводя всё к $\mathrm{S}$, $\mathrm{K}$, $\mathrm{I}$:

Переменных в ответе нет — только $\mathrm{S}$, $\mathrm{K}$, $\mathrm{I}$ и свободная $f$: $\lambda x.\,f\,x\,x \;\rightsquigarrow\; \mathrm{S}\,(\mathrm{S}\,(\mathrm{K}\,f)\,\mathrm{I})\,\mathrm{I}$.