Учебник по Haskell

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

λ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, то она становится свя-

занной. Например в терме λx.λy.x$ Переменная x является связанной, но в терме λy.x, она уже не связана.

Такие переменные называют свободными. Множество связанных переменных терма M мы будем обозначать

BV ( M )$ от англ. bound variables, а множество свободных переменных мы будем обозначать F V ( M ) от англ.

free variables.

На интуитивном уровне процесс абстракции заключается в том, что мы смотрим на несколько частных

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

стями. Например мы видим выражения:

λx. + xx,

λx. ∗ xx

И в том и в другом у нас есть функция двух аргументов + или ∗ и мы делаем из неё функцию одного

аргумента. Мы можем абстрагировать (параметризовать) это поведение в такую функцию:

λb. λx. bxx

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

\b -> \x -> b x x

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

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

( λx. M ) N

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

M [ x = N ]

Эта запись означает, что в терме M все вхождения x заменяются на терм N. Этот процесс называется

редукцией терма. А выражения вида ( λx. M) N называются редексами. Проведём к примеру редукцию терма:

( λb. λx. bxx) ∗

Для этого нам нужно в терме ( λx. bxx) заменить все вхождения переменной b на переменную ∗. После

этого мы получим терм:

λx. ∗ xx

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

α-преобразование

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

Например рассмотрим такой редекс:

( λxy. x) y

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

λy. y

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

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

её смысл. Например смысл такого выражения

( λxz. x) y

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

ной y на z. И смысл изменился, для того чтобы исключить такие случаи пользуются переименованием пе-

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

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

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

β-редукция

Процесс подстановки аргументов в функции называется β-редукцией. В редексе ( λx. M) N вместо свобод-

ных вхождений x в M мы подставляем N. Посмотрим на правила подстановки:

x[ x = N ]

⇒ N

y[ x = N ]

⇒ y

( P Q)[ x = N ]

⇒ ( P [ x = N] Q[ x = N])

( λy. P )[ x = N ] ⇒ ( λy. P [ x = N ]) ,

y /

∈ F V ( N)

( λx. P )[ x = N ] ⇒ ( λx. P )

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

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

x[ x = N ] ⇒ N

y[ x = N ] ⇒ y

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

( P Q)[ x = N ] ⇒ ( P [ x = N ] Q[ x = N ])

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

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

функции все вхождения этой переменной на N:

( λy. P )[ x = N ] ⇒ ( λy. P [ x = N ]) ,

y /

∈ F V ( N)

Условие y / ∈ F V ( N) означает, что необходимо следить за тем, чтобы в N не оказалось свободной пере-