Функциональное программирование. Основы (Файлы для подготовки к экзамену), страница 2

Кроме того, лямбда-нотация позволяет формализоватьпрактически все виды математической нотации. Если начать с константи переменных и строить выражения только с помощью лямбда-выражений и применений функции к аргументам, то можно представить оченьсложные математические выражения.Применение функции f к аргументу x мы будем обозначать как f x,т.е., в отличие от того, как это принято в математике, не будем использовать скобки2 . По причинам, которые станут ясны позднее, будем считать, что применение функции к аргументу ассоциативно влево, т.е. f x y2Заметим, что и в математике такие выражения, как sin x записываются без скобок.5означает (f (x))(y).

В качестве сокращения для выражений вида λx.λy.Eбудем использовать запись λx y.E (аналогично для большего числа аргументов). Также будем считать, что «область действия» лямбда-выражения простирается вправо насколько возможно, т.е., например, λx.x yозначает λx.(x y), а не (λx.x)y.На первый взгляд кажется, что нам необходимо ввести специальноеобозначение для функций нескольких аргументов. Однако существуетоперация каррирования3 , позволяющая записать такие функции в обычной лямбда-нотации. Идея заключается в том, чтобы использовать выражения вида λx y.x + y. Такое выражение можно рассматривать какфункцию R → (R → R), т.е. если его применить к одному аргументу,результатом будет функция, которая затем принимает другой аргумент.Таким образом:(λx y.x + y) 1 2 = (λy.1 + y) 2 = 1 + 2.Переменные в лямбда-выражениях могут быть свободными и связанными. В выражении вида x2 + x переменная x является свободной; егозначение зависит от значения переменной x и в общемPn случае Rееx нельзяпереименовать.

Однако в таких выражениях какi=1 i или 0 sin y dyпеременные i и y являются связанными; если вместо i везде использовать обозначение j, значение выражения не изменится.Следует понимать, что в каком-либо подвыражении переменная может быть свободной (как в выражении под интегралом), однако во всемвыражении она связана какой-либо операцией связывания переменной,такой как операция суммирования. Та часть выражения, которая находится «внутри» операции связывания, называется областью видимостипеременной.В лямбда исчислении выражения λx.E[x] и λy.E[y] считаются эквивалентными (это называется α-эквивалентностью, и процесс преобразования между такими парами называют α-преобразованием).

Разумеется,необходимо наложить условие, что y не является свободной переменнойв E[x].3от фамилии известного логика Хаскелла Карри, в честь которого назван языкпрограммирования Haskell63Лямбда-исчисление как формальная системаЛямбда-исчисление основано на формальной нотации лямбда-терма,составляемого из переменных и некоторого фиксированного набора констант с использованием операции применения функции и лямбда-абстрагирования. Сказанное означает, что все лямбда-выражения можно разделить на четыре категории:1.

Переменные: обозначаются произвольными строками, составленными из букв и цифр.2. Константы: также обозначаются строками; отличие от переменныхбудем определять из контекста.3. Комбинации:, т.е. применения функции S к аргументу T ; и S и Tмогут быть произвольными лямбда-термами. Комбинация записывается как S T .4. Абстракции произвольного лямбда-терма S по переменной x, обозначаемые как λx.S.Таким образом, лямбда-терм определяется рекурсивно и его грамматику можно определить в виде следующей формы Бэкуса-Наура:Exp = Var | Const | Exp Exp | λ Var .

ExpВ соответствие с этой грамматикой лямбда-термы представляются в виде синтаксических деревьев, а не в виде последовательности символов.Отсюда следует, что соглашения об ассоциативности операции применения функции, эквивалентность выражений вида λx y.S и λx.λy.S, неоднозначность в именах констант и переменных проистекают только изнеобходимости представления лямбда-термов в удобном человеку виде,и не являются частью формальной системы.3.1Свободные и связанные переменныеВ данном разделе мы формализуем данное ранее интуитивное представление о свободных и связанных переменных. Множество свободных7переменных F V (S) лямбда-терма S можно определить рекурсивно следующим образом:F V (x)F V (c)F V (S T )F V (λx.S)===={x}∅F V (S) ∪ F V (T )F V (S)\{x}Аналогично множество связанных переменных BV (S) определяется следующими формулами:BV (x)BV (c)BV (S T )BV (λx.S)====∅∅BV (S) ∪ BV (T )BV (S) ∪ {x}Здесь предполагается, что c — некоторая константа.Пример.

Для терма S = (λx y.x) (λx.z x) можно показать, что F V (S) = {z} иBV (S) = {x, y}.3.2ПодстановкиИнтуитивно ясно, что применение терма λx.S как функции к аргументу T дает в результате терм S, в котором все свободные вхожденияпеременной x заменены на T . Как ни странно, формализовать это интуитивное представление оказывается нелегко.Будем обозначать операцию подстановки терма S вместо переменной x в другом терме T как T [x := S]. Также, как и в определениесвободных и связанных переменных, правила подстановки также можноопределить рекурсивно.

Трудность состоит в том, что необходимо наложить дополнительные ограничения, позволяющие избегать конфликта вименах переменных.x[x := T ]y[x := T ]c[x := T ](S1 S2 )[x := T ](λx.S)[x := T ](λy.S)[x := T ](λy.S)[x := T ]=======Ty, если x 6= ycS1 [x := T ] S2 [x := T ]λx.Sλy.(S[x := T ]), если x 6= y и x ∈/ F V (S), либо y ∈/ F V (T )λz.(S[y := z][x := T ]) иначе, где z ∈/ F V (S) ∪ F V (T )83.3КонверсияЛямбда-исчисление основано на трех операциях конверсии, которыепозволяют переходить от одного терма к другому, эквивалентному ему.По сложившейся традиции эти конверсии обозначают греческими буквами α, β и η. Они определяются следующим образом:α• α-конверсия: λx.S −→ λy.S[x := y] при условии, что y ∈/ F V (S).αНапример, λu.u v −→ λw.w u.β• β-конверсия: (λx.S) T →− S[x := T ].ηη• η-конверсия: λx.T x −→ T , если x ∈/ F V (T ).

Например, λu.v u −→ v.Для нас наиболее важна β-конверсия, поскольку она соответствует вычислению значения функции от аргумента. α-конверсия являетсявспомогательным механизмом для того, чтобы изменять имена связанных переменных, а η-конверсия интересна в основном при рассмотрениилямбда-исчисления с точки зрения логики, а не программирования.3.4Равенство лямбда-термовИспользуя введенные правила конверсии, можно формально определить понятие равенства лямбда-термов.

Два терма равны, если от одногоиз них можно перейти к другому с помощью конечной последовательности конверсий. Определим понятие равенства следующими выражениями, в которых горизонтальные линии следует понимать как «еслиутверждение над чертой выполняется, то выполняется и утверждение9под ней»:βαηS−→ T или S −→ T или S −→TS=TT =TS=TT =SS=T иT =US=US=TSU =T US=TU S=U TS=Tλx.S = λx.TСледует отличать понятие равенства, определяемое этими формулами, от понятия синтаксической эквивалентности, которую мы будем обозначать специальным символом ≡. Например, λx.x 6≡ λy.y, но λx.x =λy.y. Часто можно рассматривать синтаксическую эквивалентность термов с точностью до α-конверсий.

Такую эквивалентность будем обозначать символом ≡α . Это отношение определяется так же, как равенстволямбда-термов, за тем исключением, что из всех конверсий допустимытолько α-конверсии. Таким образом, λx.x ≡α λy.y.3.5Экстенсиональностьη-конверсия в лямбда-исчислении выражает собой принцип экстенсиональности. В общефилософском смысле два свойства называютсяэкстенсионально эквивалентными, если они принадлежат в точности одним и тем же объектам. В математике, например, принят экстенсиональный взгляд на множества, т.е. два множества считаются одинаковыми,если они содержат одни и те же элементы. Аналогично мы говорим, чтодве функции равны, если они имеют одну и ту же область определения, идля любых значений аргумента из этой области определения вычисляютодин и тот же результат.10Вследствие наличия η-конверсии определенное нами выше отношениеравенства лямбда-термов экстенсионально.

Действительно, если f x иg x равны для любого x, то в частности f y = g y, где y не являетсясвободной переменной ни в f , ни в g. Следовательно, по последнемуправилу в определении равенства лямбда-термов, имеем λy.f y = λy.g y.Теперь, если несколько раз применить η-конверсию, можно получить, чтоf = g. И обратно, экстенсиональность дает то, что каждое применениеη-конверсии действительно приводит к равенству, поскольку по правилуβ-конверсии (λx.T x) y = T y для любого y, если x не свободна в T .3.6Редукция лямбда-термовОтношение равенства лямбда-термов, разумеется, симметрично. Хотяоно хорошо отражает понятие эквивалентности лямбда-термов, с вычислительной точки зрения более интересно будет рассмотреть асимметричный вариант.

Определим отношение редукции (обозначаемое символом→) следующим образом:αβηS−→ T или S →− T или S −→TS→TT →TS→T иT →US→US→TSU →T US→TU S→U TS→Tλx.S → λx.TНесмотря на то, что термин «редукция» подразумевает уменьшениеразмера лямбда-терма, в действительности это может быть не так, что11показывает следующий пример:(λx.x x x) (λx.x x x) → (λx.x x x) (λx.x x x) (λx.x x x)→ (λx.x x x) (λx.x x x) (λx.x x x) (λx.x x x)→ ...Тем не менее отношение редукции соответствует систематическим попыткам вычислить терм, последовательно вычисляя комбинации f (x),где f -некоторая лямбда-абстракция.

Когда для терма невозможно сделать никакую редукцию, за исключением α-преобразования, будем говорить, что терм находится в нормальной форме.3.7Редукционные стратегииДавайте отвлечемся от теоретических рассуждений и вспомним важность рассматриваемых вопросов для функционального программирования. Функциональная программа представляет собой выражение, и выполнение ее означает вычисление этого выражения. Употребляя введенные термины, можно сказать, что мы начинаем с соответствующего терма и последовательно применяем редукции до тех пор, пока это возможно.

Но какую же именно редукцию применять на каждом конкретномшаге? Отношение редукции не детерминистично, т.е. для некотороготерма t существует несколько различных ti , таких что t → ti . Иногдавыбор между ними означает выбор между конечной и бесконечной последовательности редукций, т.е. между завершением и зацикливаниемпрограммы. Например, если мы начнем редукцию с самого внутреннегоредекса4 в следующем примере, мы получим бесконечную последовательность редукций:(λx.y) ((λx.x x x) (λx.x x x))→ (λx.y) ((λx.x x x) (λx.x x x) (λx.x x x))→ (λx.y) ((λx.x x x) (λx.x x x) (λx.x x x) (λx.x x x))→ ...Однако если мы начнем с самого внешнего редекса, то мы сразу получим:(λx.y) ((λx.x x x) (λx.x x x)) → y,и больше нельзя применить никакую редукцию.Следующая теорема утверждает, что наблюдение, сделанное в предыдущем примере, верно и в более общем смысле.4От англ.

redex (REDucible EXpression)12Теорема 1. Если S → T , где T находится в нормальной форме, топоследовательность редукций, начинающаяся с S, и заключающаяся в том, что для редукции всегда выбирается самый левый и самыйвнешний редекс, гарантированно завершится и приведет терм в нормальную форму.Понятие «самого левого и самого внешнего» редекса можно определить индуктивно: для терма (λx.S) T это будет сам терм; для любогодругого терма S T это будет самый левый и самый внешний редекс в S,и для абстракции λx.S это будет самый левый самый внешний редексв S.