Unknown - haskell-notes

λ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 )

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

С помощью этих функций можно избавиться в формулах от переменных, так например свойство комму-

тативности функции A можно представить так: T A = A . Эти комбинаторы зависят друг от друга. Можно

убедиться в том, что:

I

=

SCC

Z

=

S ( CS ) S

T

=

S ( ZZS )( CC )

Все комбинаторы выражаются через комбинаторы C и S . Ранее мы пользовались другими обозначениями

для этих комбинаторов. Обозначения K и S ввёл Хаскель Карри (Haskell Curry). Независимо от Шейнфинкеля

он переоткрыл комбинаторную логику и существенно развил её. В современной комбинаторной логике для

обозначения комбинаторов I , C , T , Z и S (по Шейнфинкелю) принято использовать имена I , K , C , B , S

(по Карри).

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

14.3 Лямбда-исчисление с типами

Мы можем добавить в лямбда-исчисление типы. Предположим, что у нас есть множество V базовых типов.

Тогда тип это:

T = V | T → T

Тип может быть либо одним элементом из множества базовых типов. Либо стрелочным (функциональ-

ным) типом. Выражение “терм M имеет тип α ” принято писать так: Mα . Стрелочный тип α → β как и в

Haskell говорит о том, что если у нас есть значение типа α , то с помощью операции применения мы можем

из терма с этим стрелочным типом получить терм типа β .

Опишем правила построения термов в лямбда-исчислении с типами:

• Переменные xα , yβ , zγ , … являются термами.

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

• Если xα – переменная и Mβ – терм, то ( λxα. Mβ ) α→β – терм

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

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