52700.fb2 Учебник по Haskell - читать онлайн бесплатно полную версию книги . Страница 249

Учебник по Haskell - читать онлайн бесплатно полную версию книги . Страница 249

φ, которая переводит термы комбинаторной логики в термы лямбда-исчисления:

φ( 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 )