52700.fb2
φ( x)
=
x
φ( K)
=
λxy. x
φ( S)
=
λxyz. xz( yz)
φ( XY )
=
φ( X) φ( Y )
В первом уравнении x – переменная. Также можно определить функцию ψ, которая переводит термы
лямбда-исчисления в термы комбинаторной логики.
Комбинаторная логика | 223
ψ( x)
=
x
ψ( XY )
=
ψ( X) ψ( Y )
ψ( λx. Y )
=
[ x] . ψ( Y )
Запись [ x] . T , где x – переменная, T – терм, обозначает такой терм D, из которого можно получить терм
T подстановкой переменной x, выполнено свойство:
([ x] . T ) x = T
Эта запись означает параметризацию терма T по переменной x. Терм [ x] . T можно получить с помощью
следующего алгоритма:
[ x] . x
=
SKK
[ x] . X
=
KX,
x /
∈ V ( X)
[ x] . XY
=
S([ x] . X)([ x] . Y )
В первом уравнении мы заменяем переменную на тождественную функцию, поскольку переменные сов-
падают. Запись V ( X) во втором уравнении обозначает множество всех переменных в терме X. Поскольку
переменная по которой мы хотим параметризовать терм (или абстрагировать) не участвует в самом терме,
мы можем проигнорировать её с помощью постоянной функции K. В последнем уравнении мы параметри-
зуем применение.
С помощью этого алгоритма можно для любого терма T , все переменные которого содержатся в
{x 1 , ...xn} составить такой комбинатор D, что Dx 1 ...xn = T . Для этого мы последовательно парметризуем
терм T по всем переменным:
[ x 1 , ..., xn] . T = [ x 1] . ([ x 2 , ..., xn] . T )