Unknown - haskell-notes

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

находится внутри функции. Лямбда исчисление решает эту проблему.

Расширение лямбда исчисления

Предположим, что мы решили написать язык программирования на основе лямбда-исчисления. Было бы

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

спросить у него чему равно значение и получить ответ очень быстро.

В этом случае пользуются расширенным лямбда исчислением. В нём два типа примитивов это перемен-

ные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем

дополнить исчисление константами:

+ , ∗, 0 , 1 , 2 , ...

И ввести для них правила редукции, которые запрашивают ответ у процессора:

a + b

=

AddW ithCP U ( a, b )

a ∗ b = M ulW ithCP U ( a, b )

Так же мы можем определить и константы для логических значений:

T rue, F alse, If, N ot, And, Or

И определить правила редукции:

If T rue a b

=

a

If F alse a b

=

b

N ot T rue

=

F alse

N ot F alse

=

T rue

Add F alse a

=

F alse

Add T rue b

=

b

. . .

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

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 )

=