Кубенский А.А. Функциональное программирование

Подождите немного. Документ загружается.

144

Аналогично можно определить и другие операции над логическими

значениями, и, по существу, этим и исчерпываются все необходимые

средства для работы с логическими значениями. Теперь приступим к

определению арифметических значений и функций в терминах чистого

лямбда-исчисления.

Мы ограничимся только арифметикой натуральных чисел, все

остальные числа – рациональные, вещественные, комплексные и др.

можно получить, комбинируя натуральные числа и определяя

соответствующие операции над такими числами. Натуральные же числа

представляют собой абстракцию подсчета тех или иных объектов. Для

построения модели счета нужно выбрать, что мы будем считать. Вообще

говоря, считать можно что угодно, при этом можно получить весьма

различные модели арифметики, мы, однако, следуя Тьюрингу

, будем

подсчитывать, сколько раз некоторая функция применяется к своему

аргументу. Это приводит нас к следующему определению натурального

числа N. Число N представляется функцией с двумя аргументами, которая

выполняет N-кратное применение своего первого аргумента ко второму.

Более точно, сначала запишем определение для функции ZERO,

представляющей число нуль, а затем покажем,

как определяется число

N+1, если число N уже определено. Тем самым будет возможно построить

определение любого натурального числа N.

ZERO = λf.λx.x

функция f ноль раз применяется к аргументу x, так что аргумент

возвращается неизменным

(N+1) = λf.λx.f (N f x)

тело функции (N+1) представляет собой однократное применение

аргумента 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

К сожалению, определить операции вычитания в представленной

нами арифметике совсем не так просто. Прежде всего, определим функцию

145

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)

Теперь, когда уже определена арифметика и логика, давайте,

вооруженные опытом описания различных стандартных функций,

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

кортежам или спискам. Представляемые нами составные значения будут

146

больше всего напоминать списки, как они определены в языке 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

Давайте проверим, что наши определения работают, на простом

примере: проверим, что значением выражения

147

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, так как в выражении

аргумента e1 могут встречаться обращения

к связанной переменной x.

Эквивалентное выражение в чистом лямбда-исчислении может быть

получено путем применения Y-комбинатора.

148

Рассмотрим правила редукций, применяемые в условиях

существования рекурсивных определений, на примере преобразования

выражения

letrec FACT = λn.IF(EQ0 n) 1 (MULT n (FACT(PRED n))) in

FACT 2