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

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.

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.

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

 

 

 

 

http://starling.rinet.ru/~goga/tapl/tapl007.html

 

 

   

Chapter 5  Бестиповое лямбда-исчисление

В этой главе мы вспомним определение  и некоторые базовые свойства бестипового (untyped), или чистого (pure), лямбда-исчисления (lambda-calculus). Бестиповое лямбда-исчисление служит вычислительной основой, <<почвой>>, из которой появилось большинство систем типов, описываемых в оставшейся части книги.¹

В середине 60-х годов Питер Ландин отметил, что сложный язык программирования можно изучать, сформулировав его  ядро в виде небольшого базового исчисления, которое выражает самые существенные механизмы языка, и дополнив его набором удобных производных форм (derived forms), поведение которых можно выразить путем перевода на язык базового исчисления (Landin (1964),Landin (1965), Landin (1966); см. также Tennent (1981)). В качестве базового языка Ландин использовал лямбда-исчисление (lambda-calculus) — формальную систему, изобретенную в 1920-е годы Алонсо Чёрчем (Church, 1936, Church, 1941), где все вычисление сводится к элементарным операциям — определению функции и ее применению. Под влиянием идей Ландина, а также новаторских работ Джона Маккарти по языку Lisp (McCarthy, Russell, Edwards, et al., 1959, McCarthy, 1981) лямбда-исчисление стало широко использоваться для спецификации конструкций языков программирования, в разработке и реализации языков, а также в исследовании систем типов. Важность этого исчисления состоит в том, что его можно одновременно рассматривать как простой язык программирования,на котором можно описывать вычисления, и как математический объект, о котором можно доказывать строгие утверждения.