Учебник по Haskell

. . .

Такие правила называют δ-редукцией (дельта-редукция).

14.2 Комбинаторная логика

Одновременно с лямбда-исчислением развивалась комбинаторная логика. Она отличается более ком-

пактным представлением. Есть всего лишь одно правило, это применение функции к аргументу. А функции

строятся не из произвольных термов, а из набора основных функций. Набор основных функций называют

базисом.

Рассмотрим лямбда-термы:

λx. x,

λy. y,

λz. z

Все эти термы несут один и тот же смысл. Они представляют тождественную функцию. Они равны, но с

точностью до обозначений. Эта навязчивая проблема с переобозначением аргументов была решена в комби-

наторной логике. Посмотрим как строятся термы:

222 | Глава 14: Лямбда-исчисление

• Есть набор переменных x, y, z, …. Переменная – это терм.

• Есть две константы K и S, они являются термами.

• Если M и N – термы, то ( MN) – терм.

• Других термов нет.

Определены правила редукции для базисных термов:

Kxy

=

x

Sxyz

=

xz( yz)

В этих правилах мы пользуемся соглашением о расстановки скобок. Также как и в лямбда исчислении в

применении скобки группируются влево. Когда мы пишем Kxy, мы подразумеваем (( Kx) y). Термы в ком-

бинаторной логике принято называть комбинаторами. Редукция происходит до тех пор пока мы можем за-

менять вхождения базисных комбинаторов. Так если мы видим связку KXY или SXY Z, где X, Y , Z произ-

вольные термы, то мы можем их заменить согласно правилам редукции. Такие связки называют редексами.

Если в терме нет ни одного редекса, то он находится в нормальной форме. Замену редекса принято называть

свёрткой

Интересно, что комбинаторы K и S совпадают с определением класса Applicative для функций:

instance Applicative (r-> ) where

pure a r = a

(<*> ) a b r = a r (b r)

В этом определении у функций есть общее окружение r, из которого они могут читать значения, так же как

и в случае типа Reader. В методе pure (комбинатор K) мы игнорируем окружение (это константная функция),

а в методе <*> (комбинатор S) передаём окружение в функцию и аргумент и составляем применение функции

в контексте окружения r к значению, которое было получено в контексте того же окружения.

Вернёмся к проблеме различного представления тождественной функции в лямбда-исчислении. В ком-

бинаторной логике тождественная функция выражается так:

I = SKK

Проверим, определяет ли этот комбинатор тождественную функцию:

Ix = SKKx = Kx( Kx) = x

Сначала мы заменили I на его определение, затем свернули по комбинатору S, затем по левому комби-

натору K. В итоге получилось, что

Ix = x

Связь с лямбда-исчислением

Комбинаторная логика и лямбда-исчисление тесно связаны между собой. Можно определить функцию

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

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

Так постепенно мы придём к выражению, считаем что скобки группируются вправо:

[ x 1] . [ x 2] . ... [ xn] . T

Немного истории

Комбинаторную логику открыл Моисей Шейнфинкель. В 1920 году на докладе в Гёттингене он рассказал

основные положения этой теории. Комбинаторная логика направлена на выделение простейших строитель-

ных блоков математической логики. В этом докладе появилось понятие частичного применения. Шейнфин-

кель показал как функции многих переменных могут быть сведены к функциям одного переменного. Далее

в докладе описываются пять основных функций, называемых комбинаторами:

Ix

= x

– функция тождества

Cxy = x

– константная функция

T xyz = xzy

– функция перестановки

Zxyz = x( yz)

– функция группировки

Sxyz = xz( yz)

– функция слияния