Unknown - haskell-notes

занной. Например в терме λ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 не оказалось свободной пере-

менной с именем y , иначе после подстановки она окажется связанной. Если такая переменная в N всё-таки

окажется мы проведём α -преобразование в терме $ λy. M и заменим y на какую-нибудь другую переменную.

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