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

В этой главе мы узнаем о лямбда-исчислении. Лямбда-исчисление описывает понятие алгоритма. Ещё до появления компьютеров в 30-е годы двадцатого века математиков интересовал вопрос о возможности создания алгоритма, который мог бы на основе заданных аксиом дать ответ о том верно или нет некоторое логическое высказывание. Например у нас есть базовые утверждения и логические связки такие как “и”, “или”, “для любого из”, “существует один из”, с помощью которых мы можем строить из базовых высказываний составные. Некоторые из них окажутся ложными, а другие истинными. Нам интересно узнать какие. Но для решения этой задачи прежде всего необходимо было понять а что же такое алгоритм?

Ответ на этот вопрос дали Алонсо Чёрч (Alonso Church) и Алан Тьюринг (Alan Turing). Чёрч разработал лямбда-исчисление, а Тьюринг теорию машин Тьюринга. Оказалось, что задача автоматического определения истинности формул в общем случае не имеет решения.

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

В рамках теории машин Тьюринга алгоритм описывается по-другому. Машина Тьюринга имеет внутреннее состояние, Состояние содержит некоторое значение, которое изменяется по ходу работы машины. Машина живёт не сама по себе, она читает ленту символов. Лента символов – это большая цепочка букв. На каждую букву машина реагирует серией действий. Она может изменить значение состояния, обновить букву в ленте или перейти к следующему или предыдущему символу. Есть состояния, которые обозначают конец работы, они называются терминальными. Как только машина дойдёт до терминального состояния мы считаем, что вычисление алгоритма закончилось. После этого мы можем считать результат из состояний машины.

Функциональные языки программирования основаны на лямбда-исчислении. Поэтому мы будем говорить именно об этом описании алгоритма.

Лямбда исчисление без типов

Составление термов

Можно считать, что лямбда исчисление это такой маленький язык программирования. В нём есть множество символов, которые считаются переменными, они что-то обозначают и неделимы. В лямбда-исчислении программный код называется термом. Для написания программного кода у нас есть всего три правила:

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

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

• Если $x$ – переменная, а $M$ – терм, то $(\lambda x .M)$ – терм

В формальном описании добавляют ещё одно правило, оно говорит о том, что других термов нет. Первое правило, говорит о том, что у нас есть алфавит символов, который что-то обозначает, эти символы являются базовыми строительными блоками программы. Второе и третье правила говорят о том как из базовых элементов получаются составные. Второе правило – это правило применения функции к аргументу. В нём $M$ обозначает функцию, а $N$ обозначает аргумент. Все функции являются функциями одного аргумента, но они могут принимать и возвращать функции. Поэтому применение трёх аргументов к функции $Fun$ будет выглядеть так:

$$(((Fun\ Arg1)\ Arg2)\ Arg3)$$

Третье правило говорит о том как создавать функции. Специальный символ лямбда ($\lambda$) в выражении $(\lambda x .M)$ говорит о том, что мы собираемся определить функцию с аргументом $x$ и телом функции $M$. С такими функциями мы уже сталкивались. Это безымянные функции. Приведём несколько примеров функций. Начнём с самого простого, определим тождественную функцию:

$$(\lambda x .x)$$

Функция принимает аргумент $x$ и тут же возвращает его в теле. Теперь посмотрим на константную функцию:

$$(\lambda x .(\lambda y .x))$$

Константная функция является функцией двух аргументов, поэтому наш терм принимает переменную $x$ и возвращает другой терм функцию $(\lambda y .x)$. Эта функция принимает $y$, а возвращает x. В Haskell мы бы написали это так:

\x -> (\y -> x)

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

$$(\lambda f .(\lambda g .(\lambda x .(f(gx)))))$$

Переменные $f$ и $g$ – это функции, которые участвуют в композиции, а $x$ это вход результирующей функции. Уже в таком простом выражении у нас пять скобок на конце. Давайте введём несколько соглашений, которые облегчат написание термов:

С этими соглашениями мы можем переписать терм для композиции так:

$$\lambda f g x .f(gx)$$

Сравните с выражением на языке Haskell:

\f g x -> f (g x)

Выражения очень похожи. Haskell иногда называют засахаренной версией лямбда исчисления. В лямбда-исчислении мы не будем ставить пробелы для применения аргументов к функции. Мы будем считать, что все имена однобуквенные. При этом переменные мы будем писать с маленькой буквы, а составные термы с большой.

Определим ещё несколько функций. Например так выглядит функция flip:

$$\lambda fxy .fyx$$

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

$$\lambda f .\lambda xy .fyx$$

Определим функцию on, она принимает функцию двух аргументов $*$ и функцию одного аргумента $f$, а возвращает функцию двух аргументов, в которой к аргументам сначала применяется функция $f$, а затем они передаются в функцию $*$:

$$\lambda * f .\lambda x .*(fx)(fx)$$

В лямбда-исчислении есть только префиксное применение поэтому мы написали $*(fx)(fx)$ вместо привычного $(fx)*(fx)$. Здесь операция $*$ это не только умножение, а любая бинарная функция.

Абстракция

Функции в лямбда-исчислении называют абстракциями. Мы берём терм $M$ и параметризуем его по переменной $x$ в выражении $\lambda x. M$. При этом если в терме $M$ встречается переменная $x$, то она становится связанной. Например в терме $\lambda x . \lambda y . x$$ Переменная $x$ является связанной, но в терме $\lambda y . x$, она уже не связана. Такие переменные называют свободными. Множество связанных переменных терма $M$ мы будем обозначать $BV(M)$$ от англ. bound variables, а множество свободных переменных мы будем обозначать $FV(M)$ от англ. free variables.

На интуитивном уровне процесс абстракции заключается в том, что мы смотрим на несколько частных случаев и видим в них что-то общее. Это общее мы выделяем в функцию, которая параметризована частностями. Например мы видим выражения:

$$\lambda x .+xx, \quad \lambda x .*xx$$

И в том и в другом у нас есть функция двух аргументов $+$ или $*$ и мы делаем из неё функцию одного аргумента. Мы можем абстрагировать (параметризовать) это поведение в такую функцию:

$$\lambda b.\lambda x.b xx$$

На Haskell мы бы записали это так:

\b -> \x -> b x x

Редукция. Вычисление термов

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

$$(\lambda x .M)\ N$$

Заменяются на

$$M[x = N]$$

Эта запись означает, что в терме $M$ все вхождения $x$ заменяются на терм $N$. Этот процесс называется редукцией терма. А выражения вида $(\lambda x .M)\ N$ называются редексами. Проведём к примеру редукцию терма:

$$(\lambda b.\lambda x.b xx) *$$

Для этого нам нужно в терме $(\lambda x.b xx)$ заменить все вхождения переменной $b$ на переменную $*$. После этого мы получим терм:

$$\lambda x .* xx$$

В этом терме нет редексов. Это означает, что он вычислен или находится в нормальной форме.

$\alpha$-преобразование

При подстановке необходимо следить за тем, чтобы у нас не появлялись лишние связывания переменных. Например рассмотрим такой редекс:

$$(\lambda x y .x)\ y$$

После подстановки за счёт совпадения имён переменных мы получим тождественную функцию:

$$\lambda y .y$$

Переменная $y$ была свободной, но после подстановки стала связанной. Необходимо исключить такие случаи. Поскольку с ними получается, что имена связанных переменных в определении функции влияют на её смысл. Например смысл такого выражения

$$(\lambda x z .x)\ y$$

После подстановки будет совсем другим. Но мы всего лишь изменили обозначение локальной переменной $y$ на $z$. И смысл изменился, для того чтобы исключить такие случаи пользуются переименованием переменных или $\alpha$-преобразованием. Для корректной работы функций необходимо следить за тем, чтобы все переменные, которые были свободными в аргументе, остались свободными и после подстановки.

$\beta$-редукция

Процесс подстановки аргументов в функции называется $\beta$-редукцией. В редексе $(\lambda x .M) N$ вместо свободных вхождений $x$ в $M$ мы подставляем $N$. Посмотрим на правила подстановки:

Первые два правила определяют подстановку вместо переменных. Если переменная совпадает с той, на место которой мы подставляем терм $N$, то мы возвращаем терм $N$, иначе мы возвращаем переменную:

Подстановка применения термов равна применению термов, в которых произведена подстановка:

$$(PQ)[x=N] \Rightarrow (P[x=N]\ Q[x=N])$$

При подстановке в лямбда-функции необходимо учитывать связность переменных. Если переменная аргумента отличается от той переменной на место которой происходит подстановка, то мы заменяем в теле функции все вхождения этой переменной на $N$:

$$(\lambda y .P)[x = N] \Rightarrow (\lambda y .P[x=N]), \quad y \notin FV(N)$$

Условие $y \notin FV(N)$ означает, что необходимо следить за тем, чтобы в $N$ не оказалось свободной переменной с именем $y$, иначе после подстановки она окажется связанной. Если такая переменная в $N$ всё-таки окажется мы проведём $\alpha$-преобразование в терме $\lambda y .M$ и заменим $y$ на какую-нибудь другую переменную.

В последнем правиле мы ничего не меняем, поскольку переменная $x$ оказывается связанной. А мы проводим подстановку только вместо свободных переменных:

$$(\lambda x .P)[x = N] \Rightarrow(\lambda x .P)$$

Отметим, что не любой терм можно вычислить, например у такого терма нет нормальной формы:

$$(\lambda x .x x)(\lambda x .x x)$$

На каждом шаге редукции мы будем вновь и вновь возвращаться к исходному терму.

Стратегии редукции

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

Эти стратегии вычисления пришли из лямбда-исчисления. Если нам нужно избавиться от всех редексов в выражении, то с какого редекса лучше начать? В вычислении по значению (аппликативная стратегия) мы начинаем с самого левого редекса, который не содержит других редексов, то есть с самого маленького подвыражения. А в вычислении по имени (нормальная стратегия) мы начинаем с самого левого внешнего редекса. Левый редекс означает, что в записи выражения он находится ближе всех к началу выражения.

Теорема (Карри)

Если у терма есть нормальная форма, то последовательное сокращение самого левого внешнего редекса приводит к ней.

Эта теорема говорит о том, что стратегия вычисления по имени может вычислить все термы, которые имеют нормальную форму. В том, что вычисление по значению может не справиться с некоторыми такими термами мы можем на следующем примере:

$$(\lambda x y .x)\ z\ ((\lambda x .xx) (\lambda x .xx))$$

Этот терм имеет нормальную форму $z$ несмотря на то, что мы передаём вторым аргументом в константную функцию терм, у которого нет нормальной формы. Алгоритм вычисления по значению зависнет при вычислении второго аргумента. В то время как алгоритм вычисления по имени начнёт с самого внешнего терма и там определит, что второй аргумент не нужен.

Ещё один важный результат в лямбда-исчислении был сформулирован в следующей теореме:

Теорема (Чёрча-Россера)

Если терм $X$ редуцируется к термам $Y_1$ и $Y_2$, то существует терм $L$, к которому редуцируются и терм $Y_1$ и терм $Y_2$.

Эта теорема говорит о том, что у терма может быть только одна нормальная форма. Поскольку если бы их было две, то существовал третий терм, к которому можно было бы редуцировать эти нормальные формы. Но по определению нормальной формы, мы не можем её редуцировать. Из этого следует, что нормальные формы должны совпадать.

Теорема Чёрча-Россера указывает на способ сравнения термов. Для того чтобы понять равны термы или нет, необходимо привести их к нормальной форме и сравнить. Если термы совпадают в нормальной форме, значит они равны.

Рекурсия. Комбинатор неподвижной точки

В лямбда-исчислении все функции являются безымянными. Это означает, что мы не можем в теле функции вызвать саму функции, ведь мы не можем на неё сослаться, кажется, что у нас нет возможности строить рекурсивные функции. Однако это не так. Нам на помощь придёт комбинатор неподвижной точки. По определению комбинатор неподвижной точки решает задачу: для терма $F$ найти терм $X$ такой, что

$$F X = X$$

Существует много комбинаторов неподвижной точки. Рассмотрим $Y$-комбинатор:

$$Y\ =\ \lambda f .(\lambda x .f(xx)) (\lambda x .f(xx))$$

Убедимся в том, что для любого терма $F$, выполнено тождество: $F(YF) = YF$:

$$YF = (\lambda x .F(xx)) (\lambda x .F(xx)) = F (\lambda x .F(xx)) (\lambda x .F(xx)) = F(YF)$$

Так с помощью $Y$-комбинатора можно составлять рекурсивные функции.

Кодирование структур данных

Вы наверное заметили, что пока мы составляли лишь обобщённые функции. Эти функции комбинируют другие функции, они не выполняют никаких действий над элементами. Что если нам захочется вычислять логические значения или воспользоваться числами?

Оказывается, что логические значения, числа, пары, списки и другие конструкции могут быть закодированы с помощью термов лямбда-исчисления. Тезис Чёрча утверждает, что с помощью лямбда-терма можно представить любую вычислимую числовую функцию. В 1936 году Чёрч с помощью лямбда-исчисления доказал существование неразрешимых проблем в теории чисел. Из этого следовала неразрешимость арифметики и неразрешимость исчисления логики предикатов первого порядка. Система аксиом называется разрешимой в том случае, если существует такой алгоритм, который позволяет по виду формулы определить следует ли она из заданных аксиом или нет.

Посмотрим как с помощью термов кодируются структуры данных. Далее для сокращения записи мы будем считать, что в лямбда исчислении можно определять синонимы с помощью знака равно. Запись $N = M$ говорит о том, что мы дали обозначение $N$ терму $M$. Этой операции нет в лямбда-исчислении, но мы будем пользоваться ею для удобства.

Логические значения

Суть логических значений заключается в операторе $If$, с помощью которого мы можем организовывать ветвление алгоритма. Есть два терма $True$ и $False$, которые для любых термов $a$ и $b$, обладают свойствами:

Термы $True$, $False$ и $If$, удовлетворяющие таким свойствам выглядят так:

Проверим выполнение свойств:

$$If\ True\ a\ b \Rightarrow(\lambda b \ x \ y .b x y) (\lambda t\ f .t)\ a\ b \Rightarrow(\lambda t\ f .t)\ a\ b \Rightarrowa$$

$$If\ False\ a\ b \Rightarrow(\lambda b \ x \ y .b x y) (\lambda t\ f .f)\ a\ b \Rightarrow(\lambda t\ f .f)\ a\ b \Rightarrowb$$

Свойства выполнены. Логические константы кодируются постоянными функциями двух аргументов. Функция True возвращает первый аргумент, игнорируя второй. А функция False делает то же самое, но наоборот. В такой интерпретации логическое отрицание можно закодировать с помощью функции flip. Также мы можем выразить и другие логические операции:

Мы определили логические значения не конкретными значениями, а свойствами функций. Мы построили функции, которые ведут себя как логические значения. Этот способ определения напоминает, определение класса типов. Мы объявили три метода $True$, $False$ и $If$ и сказали, что экземпляр класса должен удовлетворять определённым свойствам, которые накладывают взаимные ограничения на методы класса. Ни один из методов не имеет смысла по отдельности, важно то как они взаимодействуют.

Натуральные числа

Оказывается, что с помощью термов лямбда исчисления можно закодировать и натуральные числа с арифметическими операциями. Мы будем кодировать числа Пеано. Для этого нам понадобится нулевой элемент и функция определения следующего элемента. Их можно закодировать так:

Как и в случае логических значений числа кодируются функциями двух аргументов. Число определяется по терму, подсчётом цепочки первых аргументов $s$. Например так выглядит число два:

$$Succ\ (Succ\ Zero) \Rightarrow(\lambda nsz .s(nsz)) (Succ\ Zero) \Rightarrow\lambda sz .s((Succ\ Zero) sz) \Rightarrow$$

$$\lambda sz .s(((\lambda ns'z' .s'(ns'z'))\ Zero)sz) \Rightarrow\lambda sz .s((\lambda s'z' .s'(Zero\ s'z'))\ sz) \Rightarrow$$

$$\lambda sz .s((\lambda s'z' .s'z')\ sz) \Rightarrow\lambda sz .s(sz)$$

И мы получили два вхождения первого аргумента в теле функции. Определим сложение и умножение. Сложение принимает две функции двух аргументов и возвращает функцию двух аргументов.

$$Add = \lambda\ m\ n\ s\ z .m\ s\ (n\ s\ z)$$

В этой функции мы применяем $m$ раз аргумент $s$ к значению, в котором аргумент $s$ применён $n$ раз, так мы и получаем $m+n$ применений аргумента $s$. Сложим 3 и 2:

$$Add\ 3\ 2 \Rightarrow\lambda s\ z .3\ s\ (2\ s\ z) \Rightarrow\lambda s\ z .3\ s\ (s\ (s\ z)) \Rightarrow\lambda s\ z .s\ (\ s\ (s\ (s\ (s\ z)))) \Rightarrow5$$

В умножении чисел $m$ и $n$ мы будем $m$ раз складывать число $n$:

$$Mul = \lambda m\ n\ s\ z .m\ (Add\ n)\ Zero$$

Конструктивная математика

В конструктивной математике существование объекта может быть доказано только описанием алгоритма, с помощью которого можно построить объект. Например доказательство методом “от противного” отвергается.

Лямбда исчисление строит конструктивное описание функции. По лямбда-терму мы можем не только вычислять значения функции, но и понять как она была построена. В классической теории, функция это множество пар $(x,\ f(x))$ аргумент-значение, которое обладает свойством:

$$x = y\ \Rightarrow\ f(x) = f(y)$$

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

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

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

В этом случае пользуются расширенным лямбда исчислением. В нём два типа примитивов это переменные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем дополнить исчисление константами:

$$+,\ *,\ 0,\ 1,\ 2,\ ...$$

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

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

$$True,\ False,\ If,\ Not,\ And,\ Or$$

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

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

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

Одновременно с лямбда-исчислением развивалась комбинаторная логика. Она отличается более компактным представлением. Есть всего лишь одно правило, это применение функции к аргументу. А функции строятся не из произвольных термов, а из набора основных функций. Набор основных функций называют базисом.

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

$$\lambda x .x, \quad \lambda y .y, \quad \lambda z .z$$

Все эти термы несут один и тот же смысл. Они представляют тождественную функцию. Они равны, но с точностью до обозначений. Эта навязчивая проблема с переобозначением аргументов была решена в комбинаторной логике. Посмотрим как строятся термы:

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

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

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

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

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

В этих правилах мы пользуемся соглашением о расстановки скобок. Также как и в лямбда исчислении в применении скобки группируются влево. Когда мы пишем $Kxy$, мы подразумеваем $((Kx)y)$. Термы в комбинаторной логике принято называть комбинаторами. Редукция происходит до тех пор пока мы можем заменять вхождения базисных комбинаторов. Так если мы видим связку $KXY$ или $SXYZ$, где $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$$

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

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

В первом уравнении $x$ – переменная. Также можно определить функцию $\psi$, которая переводит термы лямбда-исчисления в термы комбинаторной логики.

Запись $[x].T$, где $x$ – переменная, $T$ – терм, обозначает такой терм $D$, из которого можно получить терм $T$ подстановкой переменной $x$, выполнено свойство:

$$([x].T)\ x = T$$

Эта запись означает параметризацию терма $T$ по переменной $x$. Терм $[x].T$ можно получить с помощью следующего алгоритма:

В первом уравнении мы заменяем переменную на тождественную функцию, поскольку переменные совпадают. Запись $V(X)$ во втором уравнении обозначает множество всех переменных в терме $X$. Поскольку переменная по которой мы хотим параметризовать терм (или абстрагировать) не участвует в самом терме, мы можем проигнорировать её с помощью постоянной функции $K$. В последнем уравнении мы параметризуем применение.

С помощью этого алгоритма можно для любого терма $T$, все переменные которого содержатся в $\{x_1, ... x_n\}$ составить такой комбинатор $D$, что $Dx_1 ... x_n = T$. Для этого мы последовательно парметризуем терм $T$ по всем переменным:

$$[x1,...,\ x_n] .T = [x_1] .([x_2, ... ,\ x_n] .T)$$

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

$$[x_1] .[x_2] .... [x_n] .T$$

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

Комбинаторную логику открыл Моисей Шейнфинкель. В 1920 году на докладе в Гёттингене он рассказал основные положения этой теории. Комбинаторная логика направлена на выделение простейших строительных блоков математической логики. В этом докладе появилось понятие частичного применения. Шейнфинкель показал как функции многих переменных могут быть сведены к функциям одного переменного. Далее в докладе описываются пять основных функций, называемых комбинаторами:

С помощью этих функций можно избавиться в формулах от переменных, так например свойство коммутативности функции $A$ можно представить так: $TA = A$. Эти комбинаторы зависят друг от друга. Можно убедиться в том, что:

Все комбинаторы выражаются через комбинаторы $C$ и $S$. Ранее мы пользовались другими обозначениями для этих комбинаторов. Обозначения $K$ и $S$ ввёл Хаскель Карри (Haskell Curry). Независимо от Шейнфинкеля он переоткрыл комбинаторную логику и существенно развил её. В современной комбинаторной логике для обозначения комбинаторов $I$, $C$, $T$, $Z$ и $S$ (по Шейнфинкелю) принято использовать имена $I$, $K$, $C$, $B$, $S$ (по Карри).

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

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

$$T = V \ ?|\ T \rightarrowT$$

Тип может быть либо одним элементом из множества базовых типов. Либо стрелочным (функциональным) типом. Выражение “терм $M$ имеет тип $\alpha$” принято писать так: $M^{\alpha}$. Стрелочный тип $\alpha \rightarrow\beta$ как и в Haskell говорит о том, что если у нас есть значение типа $\alpha$, то с помощью операции применения мы можем из терма с этим стрелочным типом получить терм типа $\beta$.

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

• Переменные $x^\alpha$, $y^\beta$, $z^\gamma$, … являются термами.

• Если $M^{\alpha \rightarrow\beta}$ и $N^\alpha$ – термы, то $(M^{\alpha \rightarrow\beta}N^\alpha)^\beta$ – терм.

• Если $x^\alpha$ – переменная и $M^\beta$ – терм, то $(\lambda x^\alpha .M^\beta)^{\alpha \rightarrow\beta}$ – терм

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

Типизация накладывает ограничение на то, какие выражения мы можем комбинировать. В этом есть плюсы и минусы. Теперь наша система является строго нормализуемой, это означает, что любой терм имеет нормальную форму. Но теперь мы не можем выразить все функции на числах. Например мы не можем составить $Y$-комбинатор, поскольку теперь самоприменение $(e e)$ невозможно.

Мы ввели типы, но лишились рекурсии. Как нам быть? Эта проблема решается с помощью введения специальной константы $Y_\tau^{(\tau \rightarrow\tau) \rightarrow\tau}$, которая обозначает комбинатор неподвижной точки. Правило редукции для $Y$:

$$(Y_\tau f^{\tau \rightarrow\tau})^\tau = (f^{\tau \rightarrow\tau}(Y_\tau f^{\tau \rightarrow\tau}))^\tau$$

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

Краткое содержание

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

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

Упражнения

• С помощью редукции убедитесь в том, что верны формулы (в терминах Карри) :

  $B$	$=$	$S(KS)S$
  $C$	$=$	$S(BBS)(KK)$

  $Bxyz$	$=$	$xzy$
  $Cxyz$	$=$	$x(yz)$

• Попробуйте закодировать пары с помощью лямбда термов. Вам необходимо построить три функции: $Pair$, $Fst$, $Snd$, которые обладают свойствами:

  $Fst\ (Pair\ a\ b)$	$=$	$a$
  $Snd\ (Pair\ a\ b)$	$=$	$b$

• в комбинаторной логике тоже есть комбинатор неподвижной точки, найдите его с помощью алгоритма приведения термов лямбда исчисления к термам комбинаторной логики. Для краткости лучше вместо $SKK$ писать просто $I$.

• Напишите типы Lam и App, которые описывают лямбда-термы и термы комбинаторной логики в Haskell. Напишите функции перевода из значений Lam в App и обратно.