Учебник по Haskell

шашки, не меняя модуля Loop. Так чтобы вы сделали необходимые экземпляры для классов из преды-

дущего упражнения, а всё остальное поведение следовало из них.

Упражнения | 215

Глава 14

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

В этой главе мы узнаем о лямбда-исчислении. Лямбда-исчисление описывает понятие алгоритма. Ещё

до появления компьютеров в 30-е годы двадцатого века математиков интересовал вопрос о возможности со-

здания алгоритма, который мог бы на основе заданных аксиом дать ответ о том верно или нет некоторое

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

“или”, “для любого из”, “существует один из”, с помощью которых мы можем строить из базовых высказы-

ваний составные. Некоторые из них окажутся ложными, а другие истинными. Нам интересно узнать какие.

Но для решения этой задачи прежде всего необходимо было понять а что же такое алгоритм?

Ответ на этот вопрос дали Алонсо Чёрч (Alonso Church) и Алан Тьюринг (Alan Turing). Чёрч разработал

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

ния истинности формул в общем случае не имеет решения.

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

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

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

гументы в функции и возвращает такое выражение, в котором невозможно далее проводить подстановки

аргументов. Этот процесс проведения подстановок считается вычислением алгоритма.

В рамках теории машин Тьюринга алгоритм описывается по-другому. Машина Тьюринга имеет внут-

реннее состояние, Состояние содержит некоторое значение, которое изменяется по ходу работы машины.

Машина живёт не сама по себе, она читает ленту символов. Лента символов – это большая цепочка букв.

На каждую букву машина реагирует серией действий. Она может изменить значение состояния, обновить

букву в ленте или перейти к следующему или предыдущему символу. Есть состояния, которые обозначают

конец работы, они называются терминальными. Как только машина дойдёт до терминального состояния мы

считаем, что вычисление алгоритма закончилось. После этого мы можем считать результат из состояний

машины.

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

рить именно об этом описании алгоритма.

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

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

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

ство символов, которые считаются переменными, они что-то обозначают и неделимы. В лямбда-исчислении

программный код называется термом. Для написания программного кода у нас есть всего три правила:

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

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

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

В формальном описании добавляют ещё одно правило, оно говорит о том, что других термов нет. Первое

правило, говорит о том, что у нас есть алфавит символов, который что-то обозначает, эти символы явля-

ются базовыми строительными блоками программы. Второе и третье правила говорят о том как из базовых

элементов получаются составные. Второе правило – это правило применения функции к аргументу. В нём

M обозначает функцию, а N обозначает аргумент. Все функции являются функциями одного аргумента, но

они могут принимать и возвращать функции. Поэтому применение трёх аргументов к функции F un будет

выглядеть так:

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

((( F un Arg 1) Arg 2) Arg 3)

Третье правило говорит о том как создавать функции. Специальный символ лямбда ( λ) в выражении

( λx. M ) говорит о том, что мы собираемся определить функцию с аргументом x и телом функции M . С та-

кими функциями мы уже сталкивались. Это безымянные функции. Приведём несколько примеров функций.

Начнём с самого простого, определим тождественную функцию:

( λx. x)

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

цию:

( λx. ( λy. x))

Константная функция является функцией двух аргументов, поэтому наш терм принимает переменную

x и возвращает другой терм функцию ( λy. x). Эта функция принимает y, а возвращает x. В Haskell мы бы

написали это так:

\x -> (\y -> x)

Точка сменилась на стрелку, а лямбда потеряла одну ножку. Теперь определим композицию. Композиция

принимает две функции одного аргумента и направляет выход второй функции на вход первой:

( λf. ( λg. ( λx. ( f ( gx)))))

Переменные f и g – это функции, которые участвуют в композиции, а x это вход результирующей функ-

ции. Уже в таком простом выражении у нас пять скобок на конце. Давайте введём несколько соглашений,

которые облегчат написание термов:

Пишем

Подразумеваем

Опустим внешние скобки:

λx. x

( λx. x)

В применении группируем скобки

f ghx

(( f g) h) x

влево:

Ф функциях группируем скобки

λx. λy. x

( λx. ( λy. x))

вправо: