Функциональные языки программирования появились в качестве средства для написания программ, не содержащих в явном виде понятий ячеек памяти для хранения значений (переменных) и последовательности вычислений как процесса изменения состояния памяти. Тем не менее, основа для создания таких языков была предложена еще в середине 30-х годов 20-го века Алонзо Черчем (Alonzo Church) и Стефаном Клини (Stephen Kleene). Мы рассмотрим теорию Черча, названную им лямбда-исчислением, в качестве теоретической основы и "минимального" функционального языка программирования. В конечном итоге любую программу, написанную на языке Haskell или любом другом функциональном языке программирования, можно сравнительно несложными преобразованиями свести к формуле лямбда-исчисления.

Разумеется, ни Черч, ни Клини не создавали язык программирования. Вопрос, которым они интересовались - это вопрос о формализации понятия вычислимой функции и создания универсального математического аппарата для определения и работы с вычислимыми функциями. В то время эта область математики активно развивалась в трудах уже упомянутых Черча и Клини, а также Тьюринга (Alan Turing), Поста (Emil Post) и других. Во многих работах предлагался следующий подход к формализации понятия функции: в качестве основы берется некоторый "минимальный" набор базовых функций и предлагаются способы построения из них более сложных функций с помощью тех или иных комбинаторов (функций высшего порядка). Таков, например, подход, использованный Геделем при создании им теории рекурсивных функций. Напротив, в созданном им лямбда-исчислении Черч сумел построить такую систему, при которой базовых функций нет вовсе, а вместо способов построения сложных функций из простых (комбинаторов) используются правила преобразований, с помощью которых можно получать из одних функций другие, эквивалентные им. Такой процесс преобразования формул напоминает процесс вычисления функции, происходящий при исполнении программы, написанной на функциональном языке программирования. Рассмотрим теорию Черча более подробно.

Основным понятием в лямбда-исчислении является понятие выражения или формулы. Его можно определить рекурсивно. Прежде всего, зафиксируем набор идентификаторов, которые в дальнейшем будем называть переменными. Мы будем использовать в качестве имен латинские буквы x, y, f и др. В формулах переменные обычно обозначают аргументы функций, задаваемых лямбда-выражениями, однако сама по себе переменная является простейшим видом выражения. Два других вида выражений - это определение безымянной функции (лямбда-выражение) и применение функции.

Лямбда-выражение имеет вид (лx.e), где x - имя переменной, а e - выражение. Семантически такое выражение обозначает функцию с аргументом x и телом e. Применение функции записывается в виде (e1 e2), где e1 и e2 - выражения (e1 - функция, а e2 - ее аргумент). Приведем несколько примеров.

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

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

Многие примитивные функции уже хорошо нам знакомы по языку Haskell и многим другим языкам программирования. Это обычные арифметические операции сложения, умножения и другие, операции сравнения величин "больше", "меньше", "равны" и другие, операции над логическими значениями "и", "или" и другие. Мы будем пользоваться ими без какого-либо объяснения. Единственное отличие от стандартного использования этих и других операций от их использования в других языках программирования будет заключаться в том, что мы всегда будем использовать только префиксную запись операций, то есть вместо привычного 3+5 будем записывать выражение + 3 5. Конечно, все функции в нашем расширенном лямбда-исчислении будут карринговыми, то есть выражение + 3 также имеет смысл и представляет собой применение функции + к константе 3, в результате которого получается функция увеличения целого аргумента на 3.

Следует заметить также и то, что если в классическом лямбда-исчислении применение любой функции к любому аргументу всегда осмысленно, поскольку любой "объект" - как аргумент, так и результат - всегда представляет собой функцию одного аргумента, то в нашем расширенном лямбда-исчислении примитивные функции можно применять только к "правильным" аргументам. Так, бессмысленным будет выражение + TRUE 0, поскольку невозможно выполнить сложение логического значения TRUE с числом 0. Также бессмысленным будет выражение / 3 0, поскольку результат деления числа 3 на число 0 не определен. Мы не будем рассматривать бессмысленные выражения.

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

Система вывода результатов

Прежде, чем рассматривать преобразования выражений, введем важное понятие свободной и связанной переменной. Неформально говоря, вхождение переменной в некоторое выражение будет связанным, если оно находится внутри некоторого лямбда-выражения, в заголовке которого эта переменная упомянута в качестве аргумента. Другими словами, если имеется выражение, в которое в качестве подвыражения входит лx.e, то все вхождения переменной x в выражении e будут связанными. Если переменная не является связанной в некотором выражении, то она в нем будет свободной. Можно определить понятия свободных и связанных переменных и более формально. Для этого рассмотрим понятие "множества свободных переменных" некоторого выражения. Те переменные, которые не будут входить в это множество, будут в этом выражении связанными.

Итак, если выражение E представляет собой переменную x, то множество свободных переменных этого выражения F(E) содержит только эту переменную: F(E) = { x }. Если выражение представляет собой одну из стандартных констант нашего расширенного лямбда-исчисления, то оно не содержит ни свободных, ни связанных вхождений переменных, F(c) = {}. Если выражение является применением функции к аргументу и имеет вид E = e1 e2, то множество свободных переменных этого выражения является объединением множеств свободных переменных выражений e1 и e2: F(E) = F(e1) ? F(e2). Наконец, если выражение имеет вид лямбда-выражения E = лx.e, то его множество свободных переменных получится, если из множества свободных переменных выражения e убрать переменную x: F(E) = F(e) \ { x }.

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

Мы рассмотрим четыре способа преобразования выражений в лямбда-исчислении. Первое из рассматриваемых преобразований называется переименованием переменных или б-преобразованием. Смысл этого преобразования состоит в том, что суть функции не меняется, если заменить имя ее формального аргумента. Формально б-преобразование заключается в замене в выражении лx.e имени переменной x на любое другое имя с одновременной заменой всех свободных вхождений этой переменной в выражение e. Преобразование возможно, если только новая переменная уже не входит свободно в выражение e, а также если при этом свободное вхождение переменной не окажется связанным. Так, например, в выражении лx.лf.f x y можно заменить переменную x, скажем, на переменную z. В результате получится выражение лz.лf.f z y. Разумеется, новое выражение эквивалентно исходному и имеет тот же смысл. Однако, в том же выражении переменную x нельзя заменить на y, поскольку переменная y входит в тело лямбда-выражения свободно, так что получившееся после замены выражение лy.лf.f y y уже будет иметь другой смысл - в нем оба вхождения переменной y оказываются связанными. Нельзя также произвести и замену x на f, поскольку это приведет к тому, что в теле лямбда-выражения свободное вхождение переменной x превратится в связанное вхождение переменной f, и получившееся выражение лf.лf.f f y также будет иметь уже другой смысл.

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

Преобразование, называемое д-редукцией, соответствует применению "встроенной" функции к константным аргументам. Правило д-редукции имеет следующий вид. Пусть имеется выражение e e1 e2... ek, где e - константа, представляющее имя "встроенной" функции с k аргументами, а e1, e2,... ek - значения, могущие служить аргументами этой функции. Тогда такое выражение можно заменить на эквивалентное ему выражение, представленное значением, получающимся как результат применения функции к заданным значениям аргумента. Так, например, если константа + представляет функцию арифметического сложения целых, а константа OR - функцию логического "или", то в результате д-редукции выражение + 1 4 может быть преобразовано к выражению 5, а выражение OR TRUE FALSE - к выражению TRUE. Теоретически д-редукция обратима, то есть можно действовать и наоборот, представляя константы в виде применения встроенных функций к аргументам-константам. Однако на практике желание представить константу 5 в виде + 2 3 никогда не возникает.

Преобразование, называемое в-редукцией, соответствует применению функции, представленной лямбда-выражением, к аргументу. Если исходное выражение имело вид (лx.e) a, то в результате применения в-редукции оно будет преобразовано в e{x|a} - выражение e, в котором все свободные вхождения переменной x заменены на выражение a. Например, выражение ((лx.+ x x) 3) в результате применения в-редукции будет преобразовано в (+ 3 3), которое, в свою очередь, может быть преобразовано в (6) с помощью применения д-редукции.

Если в некоторое выражение входит в качестве подвыражения такое выражение, к которому можно применить одну из редукций, то такое подвыражение называется редуцируемым или сокращенно редексом (от redex - reducible expression). Таким образом, процесс преобразования выражения сводится, в основном, к применению в- и д-редукций к редексам, содержащимся в исходном выражении.

Заметим, что при применении в-редукции замене подлежат именно свободные переменные тела лямбда-выражения. Рассмотрим, например, следующее выражение: ((лx.+ x ((лx.* x x) 2)) 4). В этом выражении имеются два подвыражения-редекса, к которым можно применить в-редукцию. Первый из этих редексов - это само выражение целиком, второй - подчеркнутое подвыражение. Если применить в-редукцию к первому из этих редексов - внешнему, - то получится выражение (+ 4 ((лx.* x x) 2)). Здесь при применении редукции свободное вхождение переменной x было заменено константой 4, а связанное вхождение этой переменной во внутреннем редексе осталось неизменным. Мы можем, однако, применить в-редукцию к внутреннему редексу, тогда исходное выражение будет преобразовано в выражение ((лx.+ x (* 2 2)) 4).

Последнее преобразование, называемое з-преобразованием, выражает тот факт, что две функции, которые при применении к одному и тому же аргументу дают один и тот же результат, эквивалентны. Формально з-преобразование может быть записано следующим образом: л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. Итак, видим, что иногда применение в-редукции без предварительного переименования переменных может привести к ошибке.

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

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

· константа 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 уже в результате обычной д-редукции. На этом примере хорошо видно, что вычисления происходят именно так, как это было описано при описании схемы ленивых вычислений, так что "лишних" вычислений не производится, однако, с чисто формальной точки зрения только что описанный способ преобразования выражений, конечно же, гораздо сложнее и сложнее поддается анализу.

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

По сравнению с языками функционального программирования, подобным 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))

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

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

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

f₁ = F₁(f₁, f₂,... f_n)

f₂ = F₂(f₁, f₂,... f_n)

...

f_n = F_n(f₁, f₂,... f_n)

где все F_i - выражения, в которых встречаются рекурсивные обращения к определяемым функциям f₁, f₂,... f_n. Прежде всего образуем новое выражение, представляющее собой кортеж, в котором собраны все определения функций:

T = TUPLE-n F₁(f₁, f₂,... f_n) F₂(f₁, f₂,... f_n)... F_n(f₁, f₂,... f_n)

каждая из определяемых функций f₁, f₂,... f_n может быть теперь выражена с помощью выделения соответствующего элемента этого кортежа:

f_i = ELEM i T

поэтому если мы теперь подставим в определение кортежа T вместо всех вхождений f_i их выражения в виде элемента кортежа, то мы получим рекурсивное определение для кортежа T с прямой рекурсией:

T = TUPLE-n F₁((ELEM 1 T),... (ELEM n T))... F_n((ELEM 1 T),... (ELEM n T))

Кортеж T теперь может быть представлен как и раньше с помощью Y-комбинатора

Y (лT.TUPLE-n F₁((ELEM 1 T),... (ELEM n T))... F_n((ELEM 1 T),... (ELEM n T)))

а каждая из отдельно взятых функций может быть получена в виде элемента этого кортежа.

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

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

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

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

Тогда реализация констант TRUE и FALSE, а также функция IF получают следующее представление.

IF = лp.лt.лe.p t e

TRUE = лx.лy.x

FALSE = лx.лy.y

Проверим, что каковы бы ни были выражения A и B, выражение IF TRUE A B эквивалентно выражению A, а выражение IF FALSE A B - эквивалентно B. Действительно, при подстановке наших лямбда-выражений после преобразований в НПР последовательно получаем:

IF TRUE A B

(лp.лt.лe.p t e) (лx.лy.x) A B

(лt.лe.(лx.лy.x) t e) A B

(лe.(лx.лy.x) A e) B

(лx.лy.x) A B

(лy.A) B

A

Разумеется, совершенно аналогично выражение IF FALSE A B будет преобразовано в B.

Над логическими значениями TRUE и FALSE можно выполнять обычные операции логического сложения, умножения, отрицания и пр. Разумеется, их надо определить так, чтобы при их применении получались правильные результаты. Это нетрудно сделать; вот как могут выглядеть, например, операции AND, OR и NOT:

AND = лx.лy.x y FALSE

OR = лx.лy.x TRUE y

NOT = лx.x FALSE TRUE

Здесь в определении новых операций использованы уже определенные ранее константы TRUE и FALSE. Сами операции определены совершенно естественным образом "по МакКарти". Аналогично можно определить и другие операции над логическими значениями, и, по существу, этим и исчерпываются все необходимые средства для работы с логическими значениями. Теперь приступим к определению арифметических значений и функций в терминах чистого лямбда-исчисления.

Мы ограничимся только арифметикой натуральных чисел, все остальные числа - рациональные, вещественные, комплексные и др. можно получить, комбинируя натуральные числа и определяя соответствующие операции над такими числами. Натуральные же числа представляют собой абстракцию подсчета тех или иных объектов. Для построения модели счета нужно выбрать, что мы будем считать. Вообще говоря, считать можно что угодно, при этом можно получить весьма различные модели арифметики, мы, однако, следуя Тьюрингу, будем подсчитывать, сколько раз некоторая функция применяется к своему аргументу. Это приводит нас к следующему определению натурального числа N. Число N представляется функцией с двумя аргументами, которая выполняет N-кратное применение своего первого аргумента ко второму. Более точно, сначала запишем определение для функции ZERO, представляющей число нуль, а затем покажем, как определяется число N+1, если число N уже определено. Тем самым будет возможно построить определение любого натурального числа N.