Ru.Wikipedia.Org - Лямбда-исчисление

Меню
Главная
Случайная статья
Настройки

Лямбда-исчисление
Материал из https://ru.wikipedia.org

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

Содержание

Чистое -исчисление

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

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

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

Аппликация (лат. applicatio — прикладывание, присоединение) означает применение функции к заданному значению аргумента (то есть вызов функции). Её обычно обозначают $f\ a$ , где $f$ — функция, а $a$ — аргумент. Это соответствует общепринятой в математике записи $f(a)$ , которая тоже иногда используется, однако для -исчисления важно то, что $f$ трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация $f$ $a$ может рассматриваться двояко: как результат применения $f$ к $a$ , или же как процесс вычисления этого результата. Последняя интерпретация аппликации связана с понятием -редукции.
Абстракция или -абстракция (лат. abstractio — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если $t\equiv t[x]$ — выражение, свободно^[англ.] содержащее $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

не являются альфа-эквивалентными, так как являются свободными переменными.

Вообще говоря,

\alpha

-преобразование — это переименование связанных переменных, не меняющее «смысла» терма. Структурно, два -терма

\alpha

-эквивалентны если это один и тот же терм, либо если какие-либо их составляющие термы соответственно

\alpha

-эквивалентны.

Для абстракций, терм

\lambda y.t[y]

\alpha

-эквивалентен

\lambda x.t[x]

, если

t[y]

это

t[x]

в котором все свободные появления

x

заменены на

y

, при условии, что 1.)

y

не входит свободно в

t[x]

, и 2.)

x

не входит свободно ни в одну абстракцию

\lambda y

внутри

t[x]

(если такие есть).

Требование, чтобы

y

не была свободной переменной в

t[x]

— существенно, так как иначе она окажется «захваченной» абстракцией

\lambda y

после

\alpha

-преобразования, и из свободной переменной в

\lambda x.t[x]

превратится в связанную переменную в

\lambda y.t[y]

.

Второе требование необходимо, чтобы предотвратить случаи, подобные тому, когда, например,

\lambda y.x

является частью

t[x]

. Тогда необходимо произвести

\alpha

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

\lambda z.x

.

-редукция

Применение некой функции к некоему аргументу выражается в

\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]. На основе этих построений была создана денотационная семантика^[англ.] языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.

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

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

fact

, вычисляющую факториал:

fact(n)\triangleq \{1,{\text{ if }}n=0;{\text{ else }}n\times fact(n-1)\}

Эта функция не может быть выражена -термом n.{ 1, if n = 0; else n (fact (n-1)) }, так как в нём переменная fact является свободной, т.е. нигде не определённой. Эквивалентное выражение (G fact), где

G := r.n.{ 1, if n = 0; else n (r (n-1)) }

оставляет открытым вопрос, что такое fact. Чтобы найти ответ на этот вопрос, необходимо прежде всего понять что G выражает собой один шаг вычисления факториала в парадигме "открытой рекурсии", вызывая полученную функцию r для выполнения "остатка вычислений". Рекурсивная функция — это, по определению, такая, которая использует саму себя для проведения остатка вычислений. То есть, должно выполняться:

Fact = G Fact = G (G Fact) = G (G (G (...)))

Таким образом, Fact является "неподвижной точкой" функционала G: вся работа выполняется повторением "шага вычислений" G неограниченное количество раз, как это продиктовано значением аргумента n:

Fact n = G Fact n = G (G Fact) n = G (G (G (...))) n

Функция

fact

ссылается на саму себя посредством ссылки на своё имя, но в лямбда-исчислении у -термов имен нет. Разрешение ссылки по имени достигается в программировании посредством лексического связывания через глобальный контекст, но в лямбда исчислении он является неизменяемым. В отсутствие изменяемого глобального контекста, локальный контекст создаётся использованием дополнительных аргументов:

{\begin{aligned}fact{\text{}}(n)\ &\triangleq f(f,n)\\&where\\&f(h,n)\triangleq \{1,{\text{ if }}n=0;{\text{ else }}n\times h(h,n-1)\}\\\end{aligned}}

Здесь функция

f(h,n)

использует аргумент

h

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

h

. Вызов функции-аргумента для выполнения остатка вычислений называется "открытой рекурсией", потому что

h

гипотетически может быть чем угодно. Вызов функции

f

с самой собой в качестве аргумента на самом верхнем уровне,

f(f,n)

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

fact{\text{}}

полностью эквивалентную оригинальной рекусивной функции

fact

.

Действительно, рекурсивная функция вызывает саму себя, и само-применяемая функция

f

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

f

описывает один шаг вычисления факториала, повторное использование её снова и снова, по мере необходимости, описывает весь процесс вычисления факториала целиком.

В таком виде это синтаксически не-рекурсивное определение

fact{\text{}}

напрямую выражается как -терм:

F := h. n. { 1, if n = 0; else n ((h h) (n-1)) }

= h. (r.n.{ 1, if n = 0; else n (r (n-1)) }) (h h)

= h. G (h h)

Fact := F F

Итак F h = G (h h), и следовательно F F = G (F F). -терм (F F) является неподвижной точкой -терма G, т.е. представлением рекурсивной функции

fact

, и G ссылается на него через параметр r, выполняя тождество:

Fact := F F = G (F F) = G Fact = G (G (G (...)))

= U (h. G (h h)) = (g. U h. g (h h)) G =: Y G

U := h. h h

где

U

— это комбинатор самоприменения (самоаппликации),

Uh=h\ h

. Так несколькими элементарными само-очевидными преобразованиями сам собой получается т.н. "комбинатор неподвижной точки" (см. ниже),

Y

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

Fact := Y G = G (Y G)

Комбинатор

Y

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

\operatorname {Y}

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

Y\ g\ n=g\ (Y\ g)\ n

, то есть аргумент который здесь создаётся для вызова внутри

g

— это та же самая функция

Y\ g\

Y g = U h. g (h h) = g (U h. g (h h)) = g (Y g)

Действительно,

Fact = 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  (Fact  (n-1))})
     = G Fact

Итак,

G

— это закрытый функционал, то есть -терм, вызывающий свой аргумент в качестве функции; его неподвижная (зафиксированная, неизменяемая) точка — это функция (здесь,

YG=:Fact

), которая передаётся ему в качестве аргумента; а вызов той же самой функции и есть рекурсивный вызов.

Используя

Y

, выписывать F явным образом становится излишним. Все что нужно это "функционал одного шага" G, и его повторение неограниченное число раз достигается автоматически:

Fact n = Y G n = G (Y G) n = G (G (G (...))) n

= { 1, if n = 0; else n (Y G (n-1)) } = ...

Чтобы определить факториал как рекурсивную функцию, мы можем просто написать

\operatorname {Y} G\ n

, где

n

— число, для которого вычисляется факториал. Пусть

n=4

, получаем (подразумевая каррирование, (a b c) = ((a b) c)):

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}

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

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

S,K,I

B,C,W,K

. Эти базисы являются взаимно выразимыми, то есть любой комбинатор из одного базиса можно представить через комбинаторы другого. В частности, комбинаторы

U

Y

, как и любые другие, могут быть выражены в обеих системах.

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

Y := g. (h. 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) = BU (CBU) g
    = S(KU)(SB(KU)) g
    = SS(S(S(KS)K))(K(SII)) g

В самом деле:

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

Примерaми других комбинаторов неподвижной точки являются, например, комбинатор Тьюринга

\Theta

и комбинатор

Y{\text{}}

:= (hg. h h g) (hg. g (h h g))

= U(B(SI)U) = SII(S(K(SI))(SII))

Y := (hg. h g h) (gh. g (h g h))

= WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K)

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

В языках программирования под «-исчислением» зачастую^{[источник не указан 212 дней]} понимается механизм «анонимных функций» — 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.

Литература

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