34. Рекурсивные функции
(от позднелатинского recursio — возвращение), название, закрепившееся за одним из наиболее распространённых вариантов уточнения общего понятия арифметического алгоритма, т.е. такого алгоритма, допустимые исходные данные которого представляют собой системы натуральных чисел, а возможные результаты применения являются натуральными числами. Р. ф. были введены в 30-х гг. 20 в. С. К. Клини, в свою очередь основывавшимся на исследованиях К. Гёделя, Ж. Эрбрана и др. математиков.
  Каждая Р. ф. задаётся конечной системой равенств точно охарактеризованного типа в том смысле, что её значения вычисляются с помощью этой системы равенств по точно формулируемым правилам, причём таким образом, что в итоге для вычисления значений заданной Р. ф. получается алгоритм определённого типа.
  Арифметические функции, для вычисления значений которых имеются какие-либо алгоритмы, принято называть вычислимыми. Вычислимые функции играют в математике важную роль. Вместе с тем, если понятию алгоритма здесь не будет придан точный смысл, то и само понятие вычислимой функции окажется несколько расплывчатым. Р. ф. уже в силу самого характера своего определения оказываются вычислимыми. В известном смысле верно и обратное: имеются серьёзные основания считать, что математическое по своему характеру понятие рекурсивности является точным эквивалентом несколько расплывчатого понятия вычислимости. Предложение считать понятие вычислимости совпадающим по объёму с понятием рекурсивности известно в теории Р. ф. под названием тезиса Чёрча по имени американского математика А. Чёрча, впервые (в 30-х гг. 20 в.) сформулировавшего и обосновавшего это предложение. Принятие тезиса Чёрча позволяет придать понятию вычислимой арифметической функции точный математический смысл и подвергнуть это понятие изучению при помощи точных методов.
  Р. ф. являются частичными функциями, т. е. функциями, не обязательно всюду определёнными. Чтобы подчеркнуть это обстоятельство, часто в качестве синонима используют термин «частично рекурсивные функции». Р. ф., определённые при любых значениях аргументов, называют общерекурсивными функциями.
  Определению Р. ф. может быть придана следующая форма. Фиксируется небольшое число чрезвычайно простых исходных функций, вычислимых в упомянутом выше интуитивном смысле (функция, тождественно равная нулю, функция прибавления единицы и функции, выделяющие из системы натуральных чисел член с данным номером); фиксируется небольшое число операций над функциями, переводящих вычислимые функции снова в вычислимые (операторы подстановки, примитивной рекурсии и минимизации). Тогда Р. ф. определяются как такие функции, которые можно получить из исходных в результате конечного числа применений упомянутых выше операций.
  Оператор подстановки сопоставляет функции f от n переменных и функциям g1, . . ., gn от m переменных функцию h от m переменных такую, что для любых натуральных чисел x1, .., xm
h(x1, .., xm)  f (g1(x1, .., xm), ..., gm(x1, .., xm))
(здесь и ниже условное равенство  означает, что оба выражения, связываемые им, осмыслены одновременно и в случае осмысленности имеют одно и то же значение).
  Оператор примитивной рекурсии сопоставляет функциям f от n переменных и g от n + 2 переменных функцию h от n + 1 переменных такую, что для любых натуральных чисел x1, .. .., xn, y
h(x1, .., xn ,0)  f(x1, .., xn),
h(x1, .., xn, y + 1)  g(x1, .., xn, y, h(x1, .., xn, y )).
  Оператор минимизации сопоставляет функции f от n переменных функцию h от n переменных такую, что для любых натуральных чисел x1, .., xn
h(x1, .., xn)  f(x1, .., xn-1, y)
где у таково, что f(x1, .., xn-1, y-1) определены и отличны от xn, а f(x1, .., xn, y) определена и равна xn, если же у с указанными свойствами не существует, то значение h(x1, .., xn) считается не определённым.
  Важную роль в теории Р. ф. играют т. н. примитивно рекурсивные функции — Р. ф., получающиеся из исходных функций в результате конечного числа применений одних лишь операторов подстановки и примитивной рекурсии. Они образуют собственную часть класса общерекурсивных функций. В силу известной теоремы Клини о нормальной форме Р. ф. могут быть указаны такие конкретные примитивно рекурсивные функции U от одной переменной и Tn от n + 2 переменных, что для любой Р. ф.  от n переменных и для любых натуральных чисел x1, . . ., xn имеет место равенство (x1, ..., xn)  U(y), где у есть наименьшее из чисел z таких, что Tn(, x1, ..., xn,z) = 0 (здесь  представляет собой т. н. геделев номер функции  — число, которое эффективно строится по системе равенств, задающей функцию ). Из этой теоремы, в частности, вытекает, что для Р. ф. от п переменных может быть построена универсальная Р. ф. от n+1 переменных, т. е. такая Р. ф. Фn, что для любой Р. ф.  от n переменных и для любых натуральных чисел x1, . . ., xn имеет место условное равенство
( x1, . . ., xn)  Фn( , x1, . . ., xn).
  Это — один из центральных результатов общей теории Р. ф.
  Теория Р. ф., являясь частью алгоритмов теории, представляет собой разветвленную математическую дисциплину с собственной проблематикой и с приложениями в др. разделах математики. Понятие «Р. ф.» может быть положено в основу конструктивного определения исходных математических понятий. Широкое применение теория Р. ф. нашла в математической логике. В частности, понятие примитивно рекурсивной функции лежит в основе первоначального доказательства знаменитой теоремы Гёделя о неполноте формальной арифметики, а понятие «Р. ф.» в его полном объёме было использовано С. К. Клини для интерпретации интуиционистской арифметики (исследование это составило целую эпоху в области семантики). Аппарат теории Р. ф. используется также в теории вычислительных машин и программирования.
  Исследования показали, что все известные уточнения общего понятия алгоритма, в том числе Р. ф., взаимно моделируют друг друга и, следовательно, ведут к одному и тому же понятию вычислимой функции. Это обстоятельство служит серьёзным доводом в пользу тезиса Чёрча.
                                                  Лямбда – исчисление Черча
По сравнению с языками функционального программирования, подобным 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 - не натуральное или превосходит число элементов кортежа, заданного вторым аргументом, то результат работы функции не определен.
Теперь пусть имеются определения взаимно-рекурсивных функций
f1 = F1(f1, f2,... fn)
f2 = F2(f1, f2,... fn)
...
fn = Fn(f1, f2,... fn)
где все Fi - выражения, в которых встречаются рекурсивные обращения к определяемым функциям f1, f2,... fn. Прежде всего образуем новое выражение, представляющее собой кортеж, в котором собраны все определения функций:
T = TUPLE-n F1(f1, f2,... fn) F2(f1, f2,... fn)... Fn(f1, f2,... fn)
каждая из определяемых функций f1, f2,... fn может быть теперь выражена с помощью выделения соответствующего элемента этого кортежа:
fi = ELEM i T
поэтому если мы теперь подставим в определение кортежа T вместо всех вхождений fi их выражения в виде элемента кортежа, то мы получим рекурсивное определение для кортежа T с прямой рекурсией:
T = TUPLE-n F1((ELEM 1 T),... (ELEM n T))... Fn((ELEM 1 T),... (ELEM n T))
Кортеж T теперь может быть представлен как и раньше с помощью Y-комбинатора
Y (λT.TUPLE-n F1((ELEM 1 T),... (ELEM n T))... Fn((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.
ZERO = λf.λx.x    -- функция f ноль раз применяется к аргументу x, так что аргумент возвращается неизменным
(N+1) = λf.λx.f (N f x)
Заметим, кстати, что константа ZERO определена в точности так же, как константа FALSE, однако далеко идущих выводов из этого сходства делать все же не следует. Из приведенного определения целых чисел немедленно следует определение функции следования, которая добавляет единицу к своему аргументу:
SUCC = λn.λf.λx.f (n f x)
Теперь нетрудно также определить операции сложения и умножения целых чисел. Так, например, можно сказать, что для того, чтобы сложить два числа m и n, надо m раз увеличить число n на единицу. Аналогично, чтобы умножить m на n, надо m раз применить функцию увеличения на n к нулю. Отсюда следуют определения:
PLUS = λm.λn.m SUCC n
MULT = λm.λn.m (PLUS n) ZERO
К сожалению, определить операции вычитания в представленной нами арифметике совсем не так просто. Прежде всего определим функцию PRED, которая выдает предыдущее натуральное число для всех чисел, больших нуля, а для аргумента, равного нулю, выдает также ноль. Одно из возможных определений такой функций выглядит следующим образом:
PRED = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
Проверьте, что применение этой функции к значению ZERO действительно выдает в качестве результата ZERO, а применение этой функции к, скажем, значению 2 (представленному функцией λf.λx.f (f x)) может быть преобразовано к значению 1 (функции λf.λx.f x). Такое упражнение позволит вам понять, как происходит уменьшение количества применений функции f к аргументу. Теперь уже нетрудно определить и функцию вычитания на множестве натуральных чисел, которая для заданных аргументов m и n выдает значение (m-n) при m  n и выдает ноль при m < n.
MINUS = λm.λn.n PRED m
Арифметику целых чисел можно теперь связать с логическими значениями, определив функции сравнения чисел. Проще всего определить функцию сравнению числа с нулем. Вот одно из возможных определений для такой функции.
EQ0 = λn.n (λx.FALSE) TRUE
Очевидно, что если применить функцию к значению ZERO, то функция (λx.FALSE) не будет применена ни разу к своему аргументу, поэтому результатом применения функции будет значение TRUE. Если же значение аргумента отлично от нуля, то функция (λx.FALSE) после первого же применения выдаст значение FALSE, и в дальнейшем, сколько бы раз ее ни применять, выдаваемым значением так и будет оставаться FALSE. Теперь можно определить функции сравнения двух чисел с помощью операций GE ("больше или равно") и LE ("меньше или равно"), используя только что определенную операцию сравнения с нулем и операцию вычитания натуральных чисел MINUS.
GE = λm.λn.EQ0 (MINUS m n)
LE = λm.λn.EQ0 (MINUS n m)
Остальные операции сравнения легко выражаются через эти операции сравнения и уже определенные ранее логические операции:
GT = λm.λn.NOT (LE m n)
LT = λm.λn.NOT (GE m n)
EQ = λm.λn.AND (GE m n) (LE m n)
NEQ = λm.λn.NOT (EQ m n)
Теперь, когда уже определена арифметика и логика, давайте, вооруженные опытом описания различных стандартных функций построим функции для формирования составных значений, подобных кортежам или спискам. Представляемые нами составные значения будут больше всего напоминать списки, как они определены в языке LISP, то есть списки элементов самого разного типа (элементом такого списка может быть любое значение, в том числе другой список, число, логическое значение или, вообще говоря, любая функция). Для создания таких списков необходимо определить одно базовое значение - пустой список - и функции, позволяющие из двух заданных значений создавать их пару (функция CONS), а также выделять первый и второй элемент пары (функции HEAD  и TAIL). Для того, чтобы можно было исследовать списки в программах, требуется определить также по крайней мере одну логическую функцию NULL, которая выдает значение TRUE или FALSE в зависимости от того, является ли ее аргумент пустым списком или нет.
Функция CONS может соединять в пару два своих аргумента, просто создавая функцию, которая будет применять свой аргумент к обеим частям пары как к двум своим аргументам. Другими словами, если H и T - два произвольных значения, то их пару можно представить функцией (λs.s H T). Таким образом, функция CONS получает следующее определение:
CONS = λh.λt.λs.s h t
Для того, чтобы из составного значения (λs.s H T) выделить первый элемент H, надо применить эту функцию к такому значению s, которое выдаст первый из двух своих аргументов. Таким значением является уже определенная нами ранее константа TRUE. Ясно, что результатом применения (λs.s H T) TRUE будет значение H. Таким образом, функция HEAD получает следующее определение:
HEAD = λl.l TRUE
Разумеется, функция будет работать "правильно", только если ее аргументом будет пара, скажем, составленная с помощью функции CONS. Аналогичным образом определяется и функция TAIL.
TAIL = λl.l FALSE
Функция NULL должна выдавать в качестве результата FALSE для любой пары вида (λs.s H T). Поэтому можно определить эту функцию таким образом, чтобы она применяла свой аргумент к функции, выдающей значение FALSE для любых двух аргументов: λh.λt.FALSE. Отсюда следует определение
NULL = λl.l (λh.λt.FALSE)
Однако, та же функция должна выдавать в качестве результата TRUE, если ее аргументом будет пустой список. Отсюда можно легко вывести простой способ представления пустого списка NIL:
NIL = λx.TRUE
Давайте проверим, что наши определения работают, на простом примере: проверим, что значением выражения NULL (HEAD (CONS NIL A)) будет TRUE, каково бы ни было выражение A. Для этого будем последовательно подставлять в наше выражение определения введенных нами функций и производить редукции выражения по мере возможности. В результате получим следующую последовательность эквивалентных выражений.
NULL (HEAD (CONS NIL A))
(λl.l (λh.λt.FALSE)) (HEAD (CONS NIL A))
(HEAD (CONS NIL A)) (λh.λt.FALSE)
((λl.l TRUE) (CONS NIL A)) (λh.λt.FALSE)
((CONS NIL A) TRUE) (λh.λt.FALSE)
(((λh.λt.λs.s h t) NIL A) TRUE) (λh.λt.FALSE)
((λs.s NIL A) TRUE) (λh.λt.FALSE)
(TRUE NIL A) (λh.λt.FALSE)
NIL (λh.λt.FALSE)
(λx.TRUE) (λh.λt.FALSE)
TRUE
Мы получили ожидаемый результат. Подобным же образом можно представить в чистом лямбда-исчислении любое выражение, в том числе содержащее рекурсивные вызовы (применяя преобразование, использующее Y-комбинатор). Таким образом, можно сказать, что мы получили возможность эквивалентного представления любой функциональной программы, написанной в нашем расширенном лямбда-исчислении, с помощью лишь средств чистого лямбда-исчисления.
На самом деле использовать чистое лямбда-исчисление в практических целях, конечно же, неудобно. Даже для того, чтобы сложить числа 2 и 5, потребуется выполнить огромное количество редукций, а реализация рекурсии в виде применения Y-комбинатора - это тоже далеко не самый простой способ выполнения рекурсивных функций. Поэтому в дальнейшем мы будем использовать только расширенное лямбда-исчисление, содержащее встроенные константы и функции, а также конструкцию let для эффективной реализации механизма ленивых вычислений. Более того, мы еще расширим наше лямбда-исчисление для того, чтобы явно представить в нем рекурсию, что позволит нам обойтись без применения Y-комбинатора. Новая конструкция по виду и по действию будет напоминать конструкцию let, разница будет состоять только в том, что в новой конструкции letrec x = e1 in e2 в выражении e1 допускаются рекурсивные обращения к переменной x. Это, в частности, приводит к тому, что новая конструкция уже не может быть представлена в виде эквивалентного выражения (λx.e2) e1, так как в выражении аргумента могут встречаться обращения к связанной переменной x. Эквивалентное выражение в чистом лямбда-исчислении может быть получено путем применения Y-комбинатора.
Рассмотрим правила редукций, применяемые в условиях существования рекурсивных определений, на примере преобразования выражения
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in FACT 2
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in (λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n)))) 2
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in IF (EQ0 2) 1 (MULT 2 (FACT (PRED 2)))
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in MULT 2 (FACT 1)
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in MULT 2 ((λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n)))) 1)
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in MULT 2 (IF (EQ0 1) 1 (MULT 1 (FACT (PRED 1))))
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in MULT 2 (MULT 1 (FACT 0))
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in MULT 2 (MULT 1 ((λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n)))) 0))
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in MULT 2 (MULT 1 (IF (EQ0 0) 1 (MULT 0 (FACT (PRED 0)))))
letrec FACT = λn.IF (EQ0 n) 1 (MULT n (FACT (PRED n))) in MULT 2 (MULT 1 1)
MULT 2 (MULT 1 1)
2
В этом примере в конструкции letrec x = e1 in e2 выражение e1 уже находится в СЗНФ, поэтому при вычислении выражения e2 происходит просто подстановка значения e1 в выражение e2 вместо x. Однако, поскольку это выражение содержит рекурсивные обращения к определяемой переменной (в данном примере - FACT), то для дальнейшего вычисления требуется сохранить связь переменной со значением e1. Эта связь исчезает только тогда, когда в результате преобразований из выражения e2 исчезает сама переменная x.
В следующей главе мы будем использовать наше расширенное лямбда-исчисление в роли простого языка функционального программирования для того, чтобы более точно исследовать семантику исполнения функциональных программ. При этом мы не будем заниматься чисто текстовыми преобразованиями выражений, как мы это проделывали на протяжении всей этой главы. Вместо этого мы будем использовать более традиционные для программирования способы хранения и преобразования значений.