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

Последнее преобразование, называемое η-преобразованием, выражает тот факт, что две функции, которые при применении к одному и тому же аргументу дают один и тот же результат, эквивалентны. Формально η-преобразование может быть записано следующим образом: λx.E x эквивалентно E. Действительно, первое из этих выражений - λx.E x - представляет собой функцию, которая при задании ей в качестве аргумента некоторого значения выдает результат, эквивалентный результату применения функции E к этому аргументу. Возможность применения η-преобразования означает, что полученная функция эквивалентна функции E.

Основное назначение лямбда-исчисления состоит в том, чтобы показать, что любая вычислимая функция  может быть представлена в виде лямбда-выражения. При этом редукции и другие преобразования служат необходимым аппаратом для доказательства того, что построенная функция действительно дает нужный результат при применении ее к тем или иным аргументам. Например, легко видеть, что функция, представленная лямбда-выражением (λx.* x x) представляет собой функцию возведения в квадрат. Чтобы показать, что это действительно так, можно попробовать применить эту функцию к некоторым аргументам и посмотреть, действительно ли получается нужный результат (разумеется, это не строгое доказательство, а, скорее, процесс отладки, призванный убедить автора функции в том, что его функция "работает правильно"). Проверим, например, что функция действительно выдаст результат 36, если применить ее к аргументу 6. Для этого составим выражение ((λx.* x x) 6) и проведем его редукции. Сначала в результате применения β-редукции получится выражение (* 6 6), к которому можно, в свою очередь, применить δ-редукцию и окончательно получить в результате значение 36.

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

Как мы уже видели, в одном  и том же выражении может содержаться  несколько редексов, а значит, процесс  преобразования выражения к нормальной форме - это не однозначный процесс. Например, мы видели, что исходное выражение ((λx.+ x ((λx.* x x) 2)) 4) может быть преобразовано двумя разными способами либо к (+ 4 ((λx.* x x) 2)), либо к((λx.+ x (* 2 2)) 4). В любом случае получившееся выражение еще не находится в нормальной форме, и может быть преобразовано далее. В первом случае процесс дальнейшего преобразования выражения происходит однозначно: сначала применяется β-редукция к единственному имеющемуся в выражении редексу, а потом два раза применяется δ-редукция. В результате последовательно получим выражения (+ 4 (* 2 2)), затем (+ 4 4) и, наконец, 8. Во втором случае опять имеем два редекса в выражении - δ-редекс (* 2 2) и все выражение, представляющее собой β-редекс. Последовательно преобразуя это выражение применением δ- и β-редукций, получим сначала ((λx.+ x 4) 4), потом (+ 4 4) и, наконец 8. Как и следовало ожидать, несмотря на разные способы преобразования выражения результат - нормальная форма - получился одним и тем же.

Справедлив и более  общий факт: если у некоторого выражения  существует нормальная форма, то она  единственна, то есть какими бы способами  ни выполнять преобразования, результат  всегда будет одним и тем же, если только вообще он будет достигнут. На самом деле нормальная форма существует не всегда, так же как не любая  программа обязана завершиться  выдачей результата. Например, уже  рассматривавшееся нами ранее выражение (λx.x x)(λx.x x) не имеет нормальной формы. Действительно, само это выражение не является нормальной формой, поскольку к нему можно применить β-редукцию. Однако, при подстановке аргумента (λx.x x) вместо переменной x в тело лямбда-выражения x x, мы получим опять то же самое выражение(λx.x x)(λx.x x). Выражение, подобное только что рассмотренному, является простейшей формой "зацикливающейся" программы.

Когда мы изучали программирование на языке Haskell, нам встречались функции, которые могли выдавать значение при одном способе вычисления, и "зацикливаться" при другом способе вычисления. В качестве таких примеров можно было рассмотреть любую из функций обработки "бесконечных" списков, которые были весьма полезны и выдавали осмысленный результат при ленивом способе передачи аргументов в функцию, однако, при энергичном способе вычисления эти функции никогда не заканчивали работу. Подобные примеры выражений можно привести и для лямбда-исчисления. Например, выражение (λx.λy.y)((λx.x x)(λx.x x)) можно привести к нормальной форме, если выполнить β-редукцию, считая все выражение редексом. Действительно, выражение представляет собой применение функции (λx.λy.y) к некоторому аргументу. Однако, аргумент x не используется в теле функции - λy.y, так что независимо от того, что представляет собой этот аргумент, результатом такой β-редукции будет выражение λy.y. С другой стороны, в исходном выражении есть и еще один редекс - "зацикливающееся" выражение(λx.x x)(λx.x x). Если применять β-редукцию к нему, то вычисления никогда не закончатся.

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

Пусть в некотором выражении  имеется несколько редексов. Заметим прежде всего, что любые два редекса могут быть расположены только таким образом, что они либо совсем не пересекаются, либо один из них содержится внутри другого. Так, например, в выражении (λx.λy.y)((λx.x x)(λx.x x)) имеются два редекса, при этом один из них - это полностью все выражение, а другой, содержащийся в нем, представляет собой аргумент вызова. Назовем редекс самым внешним, если он не содержится ни в каком другом из редексов в рассматриваемом выражении. Так, в рассматриваемом выражении редекс, представляющий собой все выражение, является самым внешним. Напротив, назовем редекс самым внутренним, если внутри него не содержится редексов. Второй из рассматриваемых в нашем выражении редексов - аргумент вызова - является самым внутренним. Конечно, может оказаться, что в выражении есть несколько самых внутренних и несколько самых внешних редексов, причем одни и те же редексы могут быть как самыми внешними, так и самыми внутренними. Разумеется, если редекс содержится внутри другого и при этом внутри себя также содержит редексы, то он не будет ни самым внешним, ни самым внутренним.

Рассмотрим следующий  канонический порядок редукций: пусть  преобразования происходят таким образом, что редукция всегда применяется  к самому левому из самых внутреннихредексов. При этом может оказаться, что в некоторый момент выражение окажется в нормальной форме, и тогда "вычисления" будут закончены. Может, конечно,  оказаться и так, что этот процесс никогда не будет закончен. В выражении (λx.λy.y)((λx.x x)(λx.x x)) самым внутренним является "зацикливающийся" редекс (λx.x x)(λx.x x), поэтому наш "канонический" порядок вычислений не сможет привести выражение к нормальной форме. Этот описанный порядок редукций называется аппликативным, сокращенно - АПР (аппликативный порядок редукций). Аппликативный порядок редукций можно представлять себе как порядок, при котором в каждом вызове функции прежде всего "вычисляется" значение аргумента вызова, а потом уже происходит подстановка этого значения в тело вызываемой функции. Таким образом, этот порядок редукций соответствует энергичному способу вычисления значения функций в функциональном программировании.

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

Рассмотрим, например, следующее  выражение, представляющее собой применение функции возведения в квадрат  к результату сложения двух чисел: (λx.* x x)(+ 3 4). Все выражение представляет собой самый внешний редекс, а выражение аргумента - самый внутренний редекс. Поэтому при аппликативном порядке редукций выражение будет приведено к нормальной форме с помощью следующих трех шагов преобразования. Сначала, после применения δ-редукции к выражению аргумента получим (λx.* x x) 7, потом β-редукция преобразует это выражение к (* 7 7) и, наконец, последнее применение δ-редукции приведет выражение к нормальной форме 49. При нормальном порядке редукций первой будет применена β-редукция ко всему выражению, в результате чего получится выражение (* (+ 3 4) (+ 3 4)), представляющее собой применение функции умножения к двум одинаковым аргументам, представляющим собой сдублированное выражение, которое в исходном выражении было представлено лишь в одном экземпляре. Теперь для получения окончательного результата потребуются еще три шага δ-редукции, после которых будут последовательно получены выражения (* 7 (+ 3 4)), затем (* 7 7) и, наконец, 49.

Приведенный пример показывает, что при применении НПР для  приведения выражения к нормальной форме может потребоваться больше шагов, чем при применении АПР, однако, НПР более "надежен", так как он позволяет получить нормальную форму выражения всегда, если только такая форма вообще существует. Так, например, уже рассмотренное нами ранее выражение(λx.λy.y)((λx.x x)(λx.x x)) может быть приведено к нормальной форме за один шаг при применении НПР, однако, АПР не позволит найти эту нормальную форму ни за какое конечное число шагов

До сих пор мы преобразовывали  выражения, используя только β- и  δ-редукции. В применении α- и η-преобразований просто не было необходимости. Рассмотрим, однако, следующее выражение: λy.(λy.+ 2 y)(+ 1 y). В этом выражении имеется функция, тело которой представляет собой применение некоторой простой функции аргументу (+ 1 y). К сожалению, формальные аргументы обеих функций представлены переменной с одним и тем же именем - y. Это может привести к ошибке, если подстановку производить неправильно. Пусть, например, описанное выражение применяется к константе 1. При применении НПР в выражение (λy.+ 2 y)(+ 1 y) надо подставить единицу вместо свободного вхождения переменной y. В результате получится выражение (λy.+ 2 y)(+ 1 1), которое в результате следующих шагов будет преобразовано последовательно в (+ 2 (+ 1 1)), затем в (+ 2 2) и, наконец, в 4. Если, однако, ошибочно выполнить подстановку вместо всех вхождений переменной y в тело функции, то мы получим выражение (λy.+ 2 1)(+ 1 1), которое в результате дальнейших преобразований примет вид сначала (+ 2 1) и после следующего шага - 3. Это, очевидно, неправильно, но для того, чтобы такой ошибки избежать, надо при каждой подстановке определять, какие вхождения переменной являются свободными, а какие связанными. Если выражения достаточно сложные, то это не так-то просто.

Можно, однако, с самого начала постараться избежать подобных ошибок, выполнив α-преобразование перед применением редукций. Так, если сначала преобразовать исходное выражение к виду λz.(λy.+ 2 y)(+ 1 z), то при применении его к константе 1 ошибку сделать будет уже гораздо труднее. Правда, ошибиться можно и при выполнении начального α-преобразования.

В вышеописанном примере  α-преобразование использовалось только для того, чтобы облегчить применение редукций; если преобразование происходит автоматически, и программа, выполняющая преобразование, достаточно "интеллектуальна", чтобы отличать свободные вхождения переменных от связанных, то переименование можно было и не производить. Однако, бывают случаи, когда без переименования переменных не обойтись. Рассмотрим, например, следующее выражение: λy.(λx.λy.+ x y) y. Здесь также имеются два лямбда-выражения, имеющих одну и ту же переменную - y. Соответственно, во внешнем лямбда-выражении одно вхождение переменной y является свободным, а другое - связанным. В этом выражении имеется единственный редекс, представляющий собой тело функции, определенной внешним лямбда-выражением. Попытка применить β-редукцию без предварительного проведения α-преобразования приведет к ошибке: мы получим выражение λy.(λy.+ y y), в котором свободное вхождение переменной y попало в позицию, где переменная y связана.

Очевидно, что полученное выражение не эквивалентно исходному. Чтобы убедиться в этом, можно попробовать применить исходную и результирующую функцию к одним и тем же аргументам, например, к аргументам 1 и 2. Для исходного выражения, применяя β-редукции в нормальном порядке, последовательно получим следующие выражения: ((λy.(λx.λy.+ x y) y) 1 2), затем (((λx.λy.+ x y) 1) 2), ((λy.+ 1 y) 2), (+ 1 2), и, наконец, 3. Для выражения, полученного в результате неправильного применения редукции, получим: ((λy.(λy.+ y y)) 1 2), ((λy.+ y y) 2), (+ 2 2) и, наконец, 4. Итак, видим, что иногда применение β-редукции без предварительного переименования переменных может привести к ошибке.

Можно высказать и более  общее утверждение: β-редукция может привести к ошибке тогда, когда выражение, имеющее в своем составе свободную переменную, подставляется в качестве аргумента в выражение, имеющее в своем составе связанную переменную с тем же именем. Заметим, что необходимость в такой подстановке возникает лишь в определенном случае, а именно, тогда, когда редукции производятся внутри лямбда-выражения, то есть преобразованию подвергается тело определяемой функции. Если имеется некоторое лямбда-выражение, содержащее внутри себя редексы, то при применении АПР редукции в теле лямбда-выражения всегда будут производиться до того, как это лямбда-выражение будет применено к аргументу. Однако, при применении НПР необходимость в выполнении редукций внутри лямбда-выражения может возникнуть только тогда, когда это лямбда-выражение не применяется уже ни к каким аргументам, в противном случае, сначала будет произведена подстановка аргумента, а затем уже будет производиться редукция полученного выражения. Это означает, что мы можем избежать необходимости переименования переменных в выражении, если будем применять НПР, оставляя редексы внутри лямбда-выражений без преобразования. Следуя этому правилу, мы в результате последовательного применения β- и δ-редукций не получим нормальной формы выражения, однако, получим довольно близкий ее эквивалент - так называемую слабую заголовочную нормальную форму (сокращенно - СЗНФ).