Unknown - haskell-notes

машины.

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

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

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

вправо:

Пишем функции нескольких

λxy. x

( λx. ( λy. x ))

аргументов с одной лямбдой:

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

λf gx. f ( gx )

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

\f g x ->f (g x)

Выражения очень похожи. Haskell иногда называют засахаренной версией лямбда исчисления. В лямбда-

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

все имена однобуквенные. При этом переменные мы будем писать с маленькой буквы, а составные термы с

большой.

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

λf xy. f yx

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

λf. λxy. f yx

Определим функцию on, она принимает функцию двух аргументов ∗ и функцию одного аргумента f , а

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

передаются в функцию ∗ :

λ ∗ f. λx. ∗ ( f x )( f x )

В лямбда-исчислении есть только префиксное применение поэтому мы написали ∗ ( fx )( fx ) вместо при-

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

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

Абстракция

Функции в лямбда-исчислении называют абстракциями. Мы берём терм M и параметризуем его по пе-

ременной x в выражении λx.M . При этом если в терме M встречается переменная x , то она становится свя-