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

Ля́мбда-исчисле́ние (λ-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости.

Чистое λ-исчислениеПравить

Чистое λ-исчисление, термы которого, называемые также объектами («обами»), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличие каких-либо констант не предполагается.

Аппликация и абстракцияПравить

В основу λ-исчисления положены две фундаментальные операции:

Аппликация (лат. applicatio — прикладывание, присоединение) означает применение функции к заданному значению аргумента (т.е. вызов функции). Её обычно обозначают $f\ a$ , где $f$ — функция, а $a$ — аргумент. Это соответствует общепринятой в математике записи $f(a)$ , которая тоже иногда используется, однако для λ-исчисления важно то, что $f$ трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация $f$ $a$ может рассматриваться двояко: как результат применения $f$ к $a$ , или же как процесс вычисления этого результата. Последняя интерпретация аппликации связана с понятием β-редукции.

Абстракция или λ-абстракция (лат. abstractio — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если $t\equiv t[x]$ — выражение, свободно^[en] содержащее $x$ , тогда запись $(\lambda x.t[x])$ означает: λ функция от аргумента $x$ , которая имеет вид $t[x]$ , и обозначает функцию $x\mapsto t[x]$ . Здесь скобки не обязательны и использованы для ясности, так как точка является частью нотации и отделяет имя связанной переменной от тела функции. Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы $x$ свободно входило в $t$ , не обязательно — в этом случае $\ \lambda x.t$ обозначает функцию $x\mapsto t$ , т.е. такую, которая игнорирует свой аргумент.

α-эквивалентностьПравить

Основная форма эквивалентности, определяемая в лямбда-термах, это альфа-эквивалентность. Например, $\lambda x.x$ и $\lambda y.y$ это альфа-эквивалентные лямбда-термы которые оба представляют одну и ту же функцию - а именно, функцию тождества $x\mapsto x$ . Термы $x$ и $y$ не являются альфа-эквивалентными, так как они не находятся в лямбда-абстракции.

По определению, $\lambda x.t[x]$ $\alpha$ -эквивалентно $\lambda y.t[y]$ если $y$ не входит свободно в $t[x]$ , и $t[y]$ это $t[x]$ в котором все свободные появления $x$ заменены на $y$ .

Требование, чтобы $y$ не была свободной переменной в $t[x]$ - существенно, т.к. иначе она окажется "захваченной" абстракцией $\lambda y$ , и, после $\alpha$ -преобразования, из свободной переменной в $\lambda x.t[x]$ превратится в связанную переменную в $\lambda y.t[y]$ .

β-редукцияПравить

Применение некой фунции к некоему аргументу выражается в $\lambda$ -исчислении как аппликация $\lambda$ -терма, выражающего эту функцию, и $\lambda$ -терма аргумента. Например, применение функции $f(x)=2x+1$ к числу 3 выражается аппликацией

(\lambda x.2\cdot x+1)\ 3,

в которой на первом месте находится соответствующая абстракция. Поскольку эта функция ставит в соответствие каждому $x$ значение $2x+1$ , для вычисления результата необходимо заменить каждое свободное появление переменной $x$ в терме $2\cdot x+1$ на терм 3.

В результате получается $2\cdot 3+1=7$ . Это соображение в общем виде записывается как

(\lambda x.t)\ a=t[x:=a]

и носит название β-редукция. Выражение вида $(\lambda x.t)\ a$ , то есть применение абстракции к некоему терму, называется редексом (redex). Несмотря на то, что β-редукция по сути является единственной «существенной» аксиомой λ-исчисления, она приводит к весьма содержательной и сложной теории. Вместе с ней λ-исчисление обладает свойством полноты по Тьюрингу и, следовательно, представляет собой простейший язык программирования.

η-преобразованиеПравить

$\eta$ -преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применёнными к любому аргументу, дают одинаковые результаты.

$\eta$ -преобразование переводит друг в друга формулы $\lambda x.f\ x$ и $f$ , но только если $x$ не появляется свободно в $f$ . Иначе, свободная переменная $x$ в $f$ после преобразования стала бы связанной внешней абстракцией $\lambda x$ , и наоборот; и тогда применение этих двух выражений сводилось бы $\beta$ -редукцией к разным результатам.

Перевод $\lambda x.f\ x$ в $f$ называют $\eta$ -редукцией, а перевод $f$ в $\lambda x.f\ x$ - $\eta$ -экспансией.

Каррирование (карринг)Править

Функция двух переменных $x$ и $y$ $f(x,y)=x+y$ может быть рассмотрена как функция одной переменной $x$ , возвращающая функцию одной переменной $y$ , то есть как выражение $\ \lambda x.\lambda y.x+y$ . Такой приём работает точно так же для функций любой арности. Это показывает, что функции многих переменных могут быть выражены в λ-исчислении и являются «синтаксическим сахаром». Описанный процесс превращения функций многих переменных в функцию одной переменной называется карринг (также: каррирование), в честь американского математика Хаскелла Карри, хотя первым его предложил Моисей Шейнфинкель (1924).

Соответственно, аппликация n-арных функций это на самом деле аппликация вложенных унарных функций, одна за другой. Например, для бинарных функций:

  (λxy.    ...x...y... )  a  b   =
  (λx.λy.  ...x...y... )  a  b   =
  (λx.(λy. ...x...y... )) a  b   =
(((λx.(λy. ...x...y... )) a) b)  =
      (λy. ...a...y... )     b   =
           ...a...b...

Семантика бестипового λ-исчисленияПравить

Тот факт, что термы λ-исчисления действуют как функции, применяемые к термам λ-исчисления (то есть, возможно, к самим себе), приводит к сложностям построения адекватной семантики λ-исчисления. Чтобы придать λ-исчислению какой-либо смысл, необходимо получить множество $D$ , в которое вкладывалось бы его пространство функций $D\to D$ . В общем случае такого $D$ не существует по соображениям ограничений на мощности этих двух множеств, $D$ и функций из $D$ в $D$ : второе имеет бо́льшую мощность, чем первое.

Эту трудность в начале 1970-х годов преодолел Дана Скотт, построив понятие области $D$ (изначально на полных решётках^[1], в дальнейшем обобщив до полного частично упорядоченного множества со специальной топологией) и урезав $D\to D$ до непрерывных в этой топологии функций^[2]. На основе этих построений была создана денотационная семантика^[en] языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.

Связь с рекурсивными функциямиПравить

Рекурсия — это определение функции через саму себя; на первый взгляд, лямбда-исчисление не позволяет этого, но это впечатление обманчиво. Например, рассмотрим рекурсивную функцию, вычисляющую факториал:

f(n) = 1, if n = 0; else n × f(n - 1).

Мы не можем выразить эту функцию λ-термом (λn.(1, if n = 0; else n × (f (n-1)))), так как в нём f окажется свободной переменной. Эта функция ( $f$ ) ссылается на саму себя посредством ссылки на своё имя (f), но в лямбда-исчислении у λ-термов имен нет.

Тем не менее, λ-термы могут быть переданы как аргумент, в том числе и самим себе. Терм-функция может получить сам себя как аргумент, который окажется связанным с его параметром. Как правило, этот параметр стоит на первом месте. Связав его с функцией, мы получаем новый λ-терм, выражающий уже рекурсивную функцию. Для этого параметр, ссылающийся на себя (здесь обозначен как $h$ ), обязательно должен быть передан явным образом как аргумент при рекурсивном вызове (как $h\ h$ ):

U := λh. h h

f := U (λh. λn. (1, if n = 0; else n × (h h (n-1))))

где $U$ - это комбинатор само-аппликации, $Uh=h\ h$ .

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

     U (λh.      λn. (1, if n = 0; else n × (h h (n-1))))
     U (λh. (λr. λn. (1, if n = 0; else n × (r   (n-1)))) (h h))
(λg. U (λh. g (h h))) (λr. λn. (1, if n = 0; else n × (r (n-1))))

Это эквивалентое выражение состоит из аппликации двух независимых λ-термов, где второй - это просто лямбда-выражение рекурсивной функции без изменений, но с абстрагированным рекурсивным вызовом $(\lambda r)$ . А первый это некий комбинатор, называемый $Y$ :

g :=                  (λr. λn. (1, if n = 0; else n × (r (n-1))))
Y := λg. U (λh. g (h h)) 
   = λg. (λh. g (h h)) (λh. g (h h))

Этот комбинатор создает рекурсивную функцию из аргумента, являющегося закрытым (т.е. в котором нет свободных переменных) λ-термом исходного выражения функции. Таким образом,

Y g = (λh. g (h h)) (λh. g (h h))
    = g ((λh. g (h h)) (λh. g (h h)))
    = g (Y g)

т.е. $\operatorname {Y}$ - это комбинатор неподвижной точки: он вычисляет неподвижную точку своего аргумента. Для закрытого λ-терма с подходящей арностью, его неподвижная точка выражает рекурсивную функцию, так как $Y\ g\ n=g\ (Y\ g)\ n$ , т.е. аргумент который здесь создаётся для рекурсивного вызова внутри $g$ - это та же самая функция $Y\ g\$ !

f = Y (λr. λn. (1, if n = 0; else n × (r (n-1))))
  = Y g
  = g (Y g)
  = (λr. λn. (1, if n = 0; else n × (r (n-1)))) (Y g)
  = (    λn. (1, if n = 0; else n × (Y g (n-1)))) 
  = (    λn. (1, if n = 0; else n × (f   (n-1)))) 
  = g f

Итак, $g$ - это закрытый функционал, т.е. λ-терм, вызывающий свой аргумент в качестве функции; его неподвижная точка - это функция, которая передаётся ему же в качестве аргумента; а вызов той же самой функции и есть рекурсивный вызов, по определению.

Существует несколько определений комбинаторов неподвижной точки. Вышеуказанное - самое простое:

Y := λg. (λh. g (h h)) (λh. g (h h))

Используя стандартные комбинаторы $B$ и $C$ ,

Y g = U (λh. g (U h)) = U (λh. B g U h)
    = U (B g U) = U (C B U g) 
    = B U (C B U) g

Indeed,

U (B g U) = B g U (B g U)
    = g (U (B g U))
    = g (Y g)

Итак, чтобы определить факториал как рекурсивную функцию, мы можем просто написать $\operatorname {Y} g\ n$ , где $n$ — число, для которого вычисляется факториал. Пусть $n=4$ , получаем:

Y g 4
Y (λrn.(1, if n = 0; else n·(r (n-1)))) 4
(λrn.(1, if n = 0; else n·(r (n-1)))) (Y g) 4
(λn.(1, if n = 0; else n·(Y g (n-1)))) 4
1, if 4 = 0; else 4·(Y g (4-1))
4·(Y g 3)
4·(g (Y g) 3)
4·((λrn.(1, if n = 0; else n·(r (n-1)))) (Y g) 3)
4·(1, if 3 = 0; else 3·(Y g (3-1)))
4·(3·(g (Y g) 2))
4·(3·(1, if 2 = 0; else 2·(Y g (2-1))))
4·(3·(2·(g (Y g) 1)))
4·(3·(2·(1, if 1 = 0; else 1·(Y g (1-1)))))
4·(3·(2·(1·(g (Y g) 0))))
4·(3·(2·(1·(1, if 0 = 0; else 0·(Y g (0-1))))))
4·(3·(2·(1·(1))))
24

Итак, каждое определение рекурсивной функции может быть представлено как неподвижная точка соответствующего закрытого функционала описывающего "один вычислительный шаг" рекурсивной функции. Следовательно, используя $\operatorname {Y}$ , каждое рекурсивное определение может быть выражено как лямбда-выражение (λ-терм). В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно, и выразить их как λ-термы.

В языках программированияПравить

В языках программирования под «λ-исчислением» зачастую понимается механизм «анонимных функций» — callback-функций, которые можно определить прямо в том месте, где они используются, и которые имеют доступ к локальным переменным текущей функции (замыкание).

См. такжеПравить

ПримечанияПравить

↑ Scott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311—372.
↑ Scott D.S. Lattice-theoretic models for various type-free calculi. — In: Proc. 4th Int. Congress for Logic, Methodology, and the Philosophy of Science, Bucharest, 1972.

ЛитератураПравить

Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика: Пер. с англ. — М.: Мир, 1985. — 606 с.

[1] Scott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311—372.

[2] Scott D.S. Lattice-theoretic models for various type-free calculi. — In: Proc. 4th Int. Congress for Logic, Methodology, and the Philosophy of Science, Bucharest, 1972.

[1]

[2]