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

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)

В этом примере в конструкции letrec x = e1 in e2 выражение e1 уже находится в СЗНФ, поэтому при вычислении выражения e2 происходит просто подстановка значения e1 в выражение e2 вместо x. Однако, поскольку это выражение содержит рекурсивные обращения к определяемой переменной (в данном примере - FACT), то для дальнейшего вычисления требуется сохранить связь переменной со значением e1. Эта связь исчезает только тогда, когда в результате преобразований из выражения e2 исчезает сама переменная x.

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

Размещено на Allbest.ru