Чистое лямбда-исчисление. 
Функциональное программирование

Теперь попробуем представить в виде лямбда-выражений все стандартные константы и функции, использованные нами ранее. Для этого нужно выбрать представление и разработать технику выполнения операций над целыми числами, логическими значениями и списками. Мы не различаем типы значений, поскольку все значения являются функциями, так что наши списки смогут содержать в качестве элементов значения разных типов, и мы можем кортежи представлять тоже в виде списков элементов этих кортежей. Основным критерием для выбора того или иного представления будет функциональность этого представления, т. е. нам нужно, чтобы все представляемые нами константы и стандартные функции «вели себя правильно», в соответствии с нашими представлениями о результатах выполнения операций. Конечно, при таком подходе вычислимыми окажутся и такие выражения, которые мы считаем некорректными, например, MULT TRUE NIL, где функция MULT предназначена для умножения натуральных чисел, TRUE — функция, представляющая логическое значение «истина», a NIL — функция, представляющая пустой список. Однако результаты таких вычислений чаще всего не будут иметь никакого практического смысла. Мы просто будем считать, что подобные выражения никогда не будут сконструированы, например, потому что контроль правильности использования типов произошел до того, как мы начали переводить выражения в форму чистого лямбда-исчисления.

Проще всего определить логические константы и операции над ними, поскольку таких констант всего две — «истина» и «ложь», а операции над ними подчиняются очень простым законам.

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

IF = Xp.Xt.Xe.p t e TRUE = Xx.Xy.x FALSE = Xx.Xy.y.

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

IF TRUE, А В.

(Xp.Xt.Xe.p t е) (Xx.Xy.x) А В (Xt.Хе.(Xx.Xy.x) t е) А В (Хе.(Xx.Xy.x) А е) В (Xx.Xy.x) А В (Ху.А) В, А Разумеется, совершенно аналогично выражение IF FALSE, А В будет преобразовано в В.

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

AND = Xx.Xy.x у FALSE OR = Xx.Xy.x TRUE у NOT = Xx. x FALSE TRUE.

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

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

ZERO = Xf.Xx.x.

Функция f ноль раз применяется к аргументу х, так что аргумент возвращается неизменным. Следующее за числом N число получится, если построить функцию, которая сначала применяет первый аргумент f ко второму N раз, а затем осуществляет применение функции еще один раз: (N+l) = Xf.Ax.f (N f х) Заметим, что константа ZERO определена в точности так же, как константа FALSE, однако далеко идущих выводов из этого сходства делать все же не следует. Из приведенного определения целых чисел немедленно следует определение функции следования, которая добавляет единицу к своему аргументу:

SUCC = An.Xf.Ax.f (n f х) Теперь нетрудно также определить операции сложения и умножения целых чисел. Например, для того чтобы сложить два числа тип, нужно т раз увеличить число п на единицу. Аналогично, чтобы умножить ш на п, необходимо m раз применить функцию сложения с п к нулю. Отсюда следуют определения:

PLUS = Am. An .m SUCC п.

MULT = Am.An.m (PLUS n) ZERO.

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

PRED = An.Af.Ax.n (Ag.Ah.h (g f)) (Au.x) (Au.u).

Прежде всего, проверим, что PRED ZERO действительно выдает значение ZERO. Последовательные преобразования выражения PRED ZERO дают следующий результат:

PRED ZERO.

Af.Ах.ZERO (Ag.Ah.h (g f)) (Au.x) (Au.u).

Af.Ax.(Au.x) (Au.u).

Af.Ax.x.

При проведении этих преобразований мы воспользовались тем, что функция ZERO отбрасывает первый аргумент, выдавая в качестве результата второй. Если на место аргумента ZERO подставить произвольное число п, то применение этого числа к двум аргументам приведет к n-кратному применению первого аргумента ко второму. Мы уже видели, что если функцию (Ag.Ah.h (g f)) 0 раз применить к аргументу (Аи. х), то в результате получится (Au.x). Посмотрим, что получится, если эту функцию применить один раз, два раза и т. д.

один раз: (Ag.Ah.h (g f)) (Au.x) —> Ah. h ((Au.x) f) —> Ah. h x.

два раза: (Ag.Ah.h (g f)) (Ah.h x) —>Ah.h ((Ah.h x) f) —> Ah. h (f x).

три раза: (Ag.Ah.h (g f)) (Ah.h (f x)) —" … —> Ah. h (f (f x)).

Становится очевидным, что если применить функцию PRED к некоторому натуральному числу п, большему нуля, то в результате получится выражение, в котором содержится (п-1)-кратное применение функции f к аргументу х:

Af.Ax.(Ah.h (f … {n-1 раз} … (f x))) (Xu.u).

или окончательно.

Xf .Ax. (f … {n-1 раз} … (f x))).

а это и есть число (n-1) в выбранном нами представлении.

Теперь уже нетрудно определить и функцию вычитания на множестве натуральных чисел, которая для заданных аргументов шип выдает значение (ш-п) при m >= п и выдает ноль при m < п:

MINUS = Am.An.n PRED m.

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

EQO = An. п (Ах. FALSE) TRUE.

Очевидно, что если применить функцию к значению ZERO, то функция (Ах. FALSE) не будет применена ни разу к своему аргументу, поэтому результатом применения функции будет значение TRUE. Если же значение аргумента отлично от нуля, то функция (Ах. FALSE) после первого же применения выдаст значение FALSE, и в дальнейшем, сколько бы раз ее ни использовали, выдаваемым значением так и будет оставаться FALSE.

Функцию EQ0 можно применить для еще одного определения функции уменьшения аргумента PRED:

PRED = An. n (Ag.Ak.EQO (g ONE) k (SUCC (д к))) (Av.ZERO) ZERO.

В этой формуле идентификатором ONE обозначено число SUCC ZERO — единица. Впрочем, на это место можно подставить любое ненулевое значение. Проверьте, что это определение также корректно.

Функции сравнения двух чисел с помощью операций GE («больше или равно») и LE («меньше или равно») можно определить, используя только что определенную операцию сравнения с нулем и операцию вычитания натуральных чисел MINUS:

LE = Am.An.EQO (MINUS m n).

GE = Am.An.EQO (MINUS n m).

Остальные операции сравнения легко выражаются через эти операции сравнения и уже определенные ранее логические операции:

GT = Am.An.NOT (LE т п).

LT = Am.An.NOT (GE т п).

EQ = Am.An.AND (GE т п) (LE т п).

NEQ = Am.An.NOT (EQ т п) Теперь, когда уже определены арифметика и логика, вооружившись опытом описания различных стандартных функций, построим функции для формирования составных значений, подобных кортежам или спискам. Сначала построим функции, позволяющие из двух произвольных значений создать пару (кортеж из двух элементов), а также выделить из нары первый и второй элементы. Функцию двух аргументов, создающую кортеж из своих аргументов, мы, следуя языку Lisp, будем называть CONS, а функции, выдающие по заданному кортежу первый и второй элементы кортежа, будем называть CAR и CDR соответственно.

Историческая справка. Названия функций CAR и CDR восходят к первой реализации языка Lisp, предложенной Джоном Маккарти. В этой реализации первый элемент пары при выполнении операций над нарой помещался в «адресный регистр» — address register, а второй элемент пары — в «регистр декрементации» — decrement register. Функции, выдающие первый и второй элементы пары, просто выдавали содержимое соответствующего регистра — Content of Address Register и Content of Decrement Register соответственно. Сокращенные названия этих выражений и стали именами функций.

Функция CONS может соединять в пару два своих аргумента, просто создавая функцию, которая будет применять свой аргумент к обеим частям пары как к двум своим аргументам. Другими словами, если, А и D — два произвольных значения, то их пару можно представить функцией (As. s A D). Таким образом, функция CONS получает следующее определение: CONS = Aa.Ad.As.s a d.

Для того чтобы из составного значения (As. s A D) выделить первый элемент А, нужно применить эту функцию к такому значению s, которое выдаст первый из двух своих аргументов. Таким значением является уже определенная нами ранее константа TRUE. Ясно, что результатом применения (As. s A D) TRUE будет значение А. Таким образом, функция CAR получает следующее определение:

CAR = Ар. р TRUE.

Разумеется, функция станет работать «правильно», только если ее аргументом будет пара, составленная с помощью функции CONS. Аналогичным образом определяется и функция CDR:

CDR = Ар. р FALSE.

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

Функция NULL должна выдавать в качестве результата FALSE для любой пары вида (As. s A D). Поэтому можно определить эту функцию таким образом, чтобы она применяла свой аргумент к функции, выдающей значение FALSE для любых двух аргументов: Аа. Ad. FALSE. Отсюда следует определение NULL = Ар. р (Аа. Ad. FALSE).

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

NIL = Ах. TRUE.

Проверим, что наши определения работают, на простом примере: проверим, что значением выражения NULL (CAR (CONS NIL A)) будет TRUE, каково бы ни было выражение А. Для этого будем последовательно подставлять в наше выражение определения введенных нами функций и производить редукции выражения по мере возможности. В результате получим следующую последовательность эквивалентных выражений:

NULL (CAR (CONS NIL A)).

• (Ар.р (Aa.Ad.FALSE)) (CAR (CONS NIL A))
• (CAR (CONS NIL A)) (Aa .Ad.FALSE)
• ((Ap.p TRUE) (CONS NIL A)) (Aa.Ad.FALSE)
• ((CONS NIL A) TRUE) (Aa.Ad.FALSE)
• (((Aa.Ad.As.s a d) NIL A) TRUE) (Aa.Ad.FALSE)
• ((As.S NIL A) TRUE) (Aa.Ad.FALSE)
• (TRUE NIL A) (Aa.Ad.FALSE)

NIL (Aa.Ad.FALSE).

(Ax.TRUE) (Aa.Ad.FALSE).

TRUE.

Получен ожидаемый результат.

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