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

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

• константа c (в том числе - одна из встроенных функций);
• переменная x;
• лямбда-выражение λx.e, где e - выражение, находящееся в нормальной форме;
• f e1 e2... ek, где f - встроенная функция с n аргументами, e1, e2,... ek - выражения в нормальной форме, причем k < n.

Последний вид нормальной формы выражения - это применение встроенной функции с недостаточным  числом переданных ей аргументов, например, (+ 1). Заметим, что этот последний вид нормальной формы выражения эквивалентен некоторому лямбда-выражению, находящемуся в нормальной форме. Так, например, выражение (+ 1) эквивалентно выражению (λx.+ 1 x). Теперь сходным образом можно определить и СЗНФ. Будем говорить, что выражение находится в СЗНФ, если оно имеет один из следующих видов:

• константа c (в том числе - одна из встроенных функций);
• переменная x;
• лямбда-выражение λx.e, где e - произвольное выражение;
• f e1 e2... ek, где f - встроенная функция с n аргументами, e1, e2,... ek - выражения в СЗНФ, причем k < n.

Теперь можно определить процесс "вычисления" выражения  как процесс приведения его к  СЗНФ с помощью β- и δ-редукций, применяемых в нормальном порядке. При таком процессе никогда не потребуется применять α-преобразований для "безопасного" переименования переменных. Таким образом можно считать, что у нас имеется достаточно простой и формальный процесс преобразования выражений лямбда-исчисления в простую форму с помощью только β- и δ-редукций. Такой процесс преобразования примерно соответствует исполнению программы в некотором простом языке функционального программирования. В дальнейшем мы покажем, как можно сравнительно простыми преобразованиями свести программу, написанную на языке, подобном языкуHaskell, к вычислению выражения, записанного средствами лямбда-исчисления, поэтому можно считать, что лямбда-исчисление является основой для реализации исполнения функциональных программ.

Выше мы уже отмечали, что процесс преобразования формы  выражения при аппликативном  порядке редукций напоминает процесс  выполнения функциональной программы  при энергичном способе исполнения, то есть при таком способе вызова функций, когда перед началом  работы тела функции происходит вычисление фактических аргументов и передача полученных значений в функцию для  вычисления. Напротив, при нормальном порядке применения редукций вычисления происходят таким образом, что подстановка  аргументов происходит до того, как  будут вычислены их значения, что  примерно соответствует ленивой  схеме исполнения функциональной программы. Однако, имеется и существенная разница  между ленивыми вычислениями и текстовыми преобразованиями выражений так, как  это принято в лямбда-исчислении. При исполнении функциональной программы даже если при вызове функции ее аргумент и не вычисляется сразу же, он все же будет вычисляться не более одного раза - при первом обращении к этому аргументу из тела функции, когда он передается одной из встроенных функций или производится сопоставление этого аргумента с некоторым образцом. В случае же преобразований выражений с помощью редукций вычисление аргументов будет происходить при каждом обращении к аргументу в теле вычисляемой функции. Поясним сказанное примером.

Пусть требуется привести к СЗНФ выражение (λx.* x x)(+ 2 3). В этом выражении имеются два редекса, однако, если мы используем НПР, то прежде всего выполняется β-редукция, при которой выражение аргумента (+ 2 3) подставляется вместо свободного вхождения переменной x в тело лямбда-выражения, при это получается выражение (* (+ 2 3) (+ 2 3)). После этого выражение (+ 2 3) придется вычислить два раза применением к нему δ-редукции, и только затем уже будет получено окончательное значение 25. С точки зрения получения правильного результата не имеет значения то, сколько раз будет применяться редукция к одним и тем же выражениям, поэтому отмеченная нами "неэффективность" вычислений несущественна с точки зрения построения теории вычислимых функций, однако для того, чтобы строить адекватную модель вычислений, средств, предложенных нами в качестве описания преобразования выражений, недостаточно.

Расширим наше лямбда-исчисление, введя еще одну дополнительную конструкцию  в качестве допустимого выражения. Новая конструкция будет иметь  вид let x=e1 in e2, где x - переменная, а e1 и e2 - произвольные выражения. Новый вид выражения будет полностью эквивалентен выражению (λx.e2) e1, однако процесс его редуцирования будет происходить в соответствии с правилами ленивых вычислений, а именно, следующим образом. Данное выражение считается эквивалентным выражению e2, однако, если при его преобразовании потребуется произвести δ-редукцию, в которой одним из операндов встроенной функции является переменная x, упомянутая в заголовке выражения, то прежде всего выражение e1 приводится к СЗНФ, после чего результат подставляется вместо всех свободных вхождений переменной x в текущее выражение, после чего вычисления производятся обычным образом. Теперь модифицируем правило выполнения β-редукции: теперь при β-редукции выражение (λx.e) a будет преобразовываться в let x=a in e. Посмотрим, как теперь будут выполняться вычисления в НПР.

Снова рассмотрим исходное выражение (λx.* x x)(+ 2 3). Теперь, однако, выполнение β-редукции приведет нас к выражению let x = + 2 3 in (* x x). Теперь требуется преобразовывать выражение (* x x), однако, здесь перед проведением δ-редукции потребуется сначала привести к СЗНФ выражение (+ 2 3). После того, как будет получен результат вычисления - выражение 5, - этот результат будет подставлен в выражение (* x x) вместо переменной x. В результате мы получим выражение (* 5 5), которое превратится в результат вычислений - число 25 уже в результате обычной δ-редукции. На этом примере хорошо видно, что вычисления происходят именно так, как это было описано при описании схемы ленивых вычислений, так что "лишних" вычислений не производится, однако, с чисто формальной точки зрения только что описанный способ преобразования выражений, конечно же, гораздо сложнее и сложнее поддается анализу.

3.3. Чистое лямбда-исчисление

По сравнению с языками  функционального программирования, подобным Haskell, в лямбда-исчислении не хватает чисто практических средств, позволяющих удобно записывать функции. Прежде всего бросается в глаза отсутствие средств описания рекурсивных функций. Действительно, рекурсивные обращения всегда происходят с использованием имени функции, однако лямбда-исчисление - это язык для описания безымянных функций! Конечно, иногда мы можем обойтись и без использования рекурсии, если имеется достаточно богатый набор встроенных функций. Так, например, имея функцию высшего порядка foldr в качестве одной из встроенных функций, мы можем написать функцию вычисления факториала натурального числа и без использования рекурсии. Аналогично, функция свертки дерева foldTree позволила нам написать без использования рекурсии функцию разглаживания дерева flatten. На самом деле можно показать, что имея достаточно богатый набор мощных функций высшего порядка, можно всегда обойтись без использования рекурсивных вызовов (такой стиль программирования называется программированием с помощью комбинАторов или комбинАторным программированием). Однако, чистое лямбда-исчисление не предполагает использования встроенных функций вообще! Возникает вопрос: достаточно ли средств лямбда-исчисления для того, чтобы выразить в нем всевозможные вычислимые функции, если в нем невозможно обычным образом задавать рекурсивные функции, а встроенных функций, позволяющих обойти эту проблему, нет вообще?

В этом разделе мы постепенно построим чистое лямбда-исчисление, последовательно  выразив в виде лямбда-выражений  все имевшиеся у нас ранее  константы и встроенные функции, и задав с помощью тех же лямбда-выражений все управляющие  конструкции языков функционального  программирования, включая рекурсию, условное вычисление и др. Начнем мы именно с выражения прямой и косвенной  рекурсии в чистом лямбда-исчислении.

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

fact n = if n == 0 then 1 else n * fact(n-1)

Прежде всего, зададим  эту функцию с помощью конструкций  лямбда-исчисления, считая, что у  нас имеются встроенные функции  для вычитания (функция '-'), умножения (функция '*') и сравнения с нулем (функция 'eq0'), кроме того, считаем, что у нас также есть функция 'if' для условного вычисления и константы '0' и '1'. Тогда определение функции будет выглядеть следующим образом.

fact = λn.if (eq0 n) 1 (* n (fact (- n 1)))

Здесь мы пока по-прежнему использовали задание имени для функции fact для того, чтобы выразить рекурсию. Построим теперь новую функцию, в которой вызываемая функция factбудет аргументом:

sFact = λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))

Конечно, эта новая функция не будет тем факториалом, который мы пытаемся построить хотя бы потому, что ее аргументом является не целое число, а некоторая функция, однако она некоторым вполне определенным образом связана с той функцией вычисления факториала, которую мы пытаемся построить. Зададимся задачей найти такую функцию f, что она являетсянеподвижной точкой определенной нами функции sFact, то есть такую f, что выполнено равенство f = sFact f. Очевидно, что если такую неподвижную точку удастся найти, то найденная функция f как раз и будет тем самым факториалом, который мы ищем, поскольку будет выполнено равенство

f = sFact f = λn.if (eq0 n) 1 (* n (f (- n 1)))

Итак, задача нахождения функции, эквивалентной заданной рекурсивной  функции, свелась к задаче построения неподвижной точки для некоторой  другой функции. Кажется, что эту  задачу - задачу нахождения неподвижной  точки - в общем виде решить не удастся. A priori вообще не ясно, всегда ли такая неподвижная точка существует. Однако оказывается, что удается построить функцию, которая для заданного аргумента вычисляет его неподвижную точку. Если обозначить через Y такую функцию нахождения неподвижной точки, то для любой функции f должно быть справедливо равенство Y f = f(Y f). Другими словами, результатом применения функции Y к функции f должно быть такое значение x, что x = f(x). Одну из таких функций предложил Хаскелл Карри, которая в его честь называется Y-комбинатором Карри. Вот запись этой функции в нотации лямбда-исчисления:

Y = λh.(λx.h (x x))(λx.h (x x))

Проверим, действительно  ли для этой функции выполнено  равенство Y f = f(Y f). Для этого запишем выражение Y f и попробуем привести его к СЗНФ. После того, как вместо Yбудет подставлено соответствующее лямбда-выражение, мы сможем выполнить один шаг β-редукции, и получим выражение (λx.f (x x))(λx.f (x x)). Это выражение еще не находится в СЗНФ, так что мы можем выполнить еще один шаг и с помощью β-редукции привести его к виду f ((λx.f (x x))(λx.f (x x))). Это выражение также не находится в СЗНФ, более того, теперь видно, что привести это выражение к СЗНФ вообще никогда не удастся, так как каждый следующий шаг редукции приводит только к увеличению длины выражения. Однако, из проведенных шагов хорошо видно, что выражение Y f действительно эквивалентно выражению f(Y f), поскольку второе получается из первого за один шаг редукции.

Итак, мы получили, что выражение  для рекурсивной функции можно  получить, если построить некоторое  вспомогательное выражение, а затем  применить к нему Y-комбинатор Карри. Получившееся при этом выражение  не может быть приведено к СЗНФ, однако оно все же будет работать как соответствующая рекурсивная  функция. Давайте убедимся в этом, построив описанным способом функцию  для вычисления факториала заданного  числа, а затем применим ее к конкретному  числу, скажем, числу 2, и проверим, как  получается результат вычисления - число 2, равноеfact(2). Для этого попробуем привести к СЗНФ выражение (Y sFact) 2, где Y обозначает Y-комбинатор Карри, а sFact - функцию, приведенную выше, полученную из рекурсивного определения факториала. Последовательные шаги по преобразованию выражения к СЗНФ показаны ниже.

Y sFact 2

sFact (Y sFact) 2

(λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 2

(λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 2

if (eq0 2) 1 (* 2 ((Y sFact) (- 2 1)))

(* 2 (Y sFact 1))

Остановимся пока здесь. Мы видим, что последовательное выполнение β- и δ-редукций привело нас от выражения Y sFact 2 к выражению (* 2 (Y sFact 1)). Это уже показывает, что преобразование выражения происходит именно так, как ведет себя рекурсивное вычисление факториала. Однако, давайте продолжим преобразования.

Y sFact 2

sFact (Y sFact) 2

(λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 2

(λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 2

if (eq0 2) 1 (* 2 ((Y sFact) (- 2 1)))

(* 2 (Y sFact 1))

(* 2 (sFact (Y sFact) 1)

(* 2 (λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 1)

(* 2 (λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 1)

(* 2 (if (eq0 1) 1 (* 1 ((Y sFact) (- 1 1)))))

(* 2 (* 1 (Y sFact 0)))

(* 2 (* 1 (sFact (Y sFact) 0)))

(* 2 (* 1 ((λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 0)))

(* 2 (* 1 ((λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 0)))

(* 2 (* 1 (if (eq0 0) 1 (* 0 ((Y sFact) (- 0 1))))))

(* 2 (* 1 1))

2

Преобразования закончились  вполне предсказуемым результатом, так что можно заключить, что  применение Y-комбинатора Карри действительно  приводит к нужному результату. Существенно, что мы использовали при вычислениях нормальный порядок редукций, так как при аппликативном порядке редукций вычисления просто никогда не были бы закончены. Существуют и другие формы Y-комбинаторов, в частности, такие, которые применимы и при АПР, однако, все известные другие выражения для Y-комбинаторов выглядят сложнее, чем Y-комбинатор Карри.

Если несколько функций  определяются таким образом, что  в теле каждой из них имеются вызовы других функций из этого набора, то говорят, что мы имеем дело со взаимно-рекурсивными функциями. На самом деле этот случай можно свести к прямой рекурсии и, тем самым, выразить в лямбда-исчислении не только прямую, но и взаимную рекурсию. Для того, чтобы свести взаимную рекурсию к прямой, нам потребуются некоторые дополнительные встроенные функции. Во-первых, введем серию функций кортежирования, которые составляют кортеж из своих аргументов. Будем считать, что если k - некоторое натуральное число, то функция TUPLE-k имеет k аргументов и выдает в качестве результата кортеж из k элементов. Еще одна функция нужна для того, чтобы, наоборот, выделять элемент с заданным номером из кортежа. Назовем эту функцию ELEM. Функция ELEM имеет два аргумента: n - номер элемента кортежа - натуральное число, не превосходящее длины кортежа T, который является вторым аргументом этой функции. Результатом работы функции служит n-ый элемент кортежа T. Если число n - не натуральное или превосходит число элементов кортежа, заданного вторым аргументом, то результат работы функции не определен.

Теперь пусть имеются  определения взаимно-рекурсивных  функций