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

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

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

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

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

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

Шаблон:ЯкорьАппликация (Шаблон:Lang-lat — прикладывание, присоединение) означает применение функции к заданному значению аргумента (то есть вызов функции). Её обычно обозначают $f a$ , где $f$ — функция, а $a$ — аргумент. Это соответствует общепринятой в математике записи $f (a)$ , которая тоже иногда используется, однако для λ-исчисления важно то, что $f$ трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация $f$ $a$ может рассматриваться двояко: как результат применения $f$ к $a$ , или же как процесс вычисления этого результата. Последняя интерпретация аппликации связана с понятием β-редукции.
Шаблон:ЯкорьАбстракция или λ-абстракция (Шаблон:Lang-lat — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если $t \equiv t [x]$ — выражение, Шаблон:Не переведено 5 содержащее $x$ , тогда запись $(λ x . t [x])$ означает: λ функция от аргумента $x$ , которая имеет вид $t [x]$ , и обозначает функцию $x \mapsto t [x]$ . Здесь скобки не обязательны и использованы для ясности, так как точка является частью нотации и отделяет имя связанной переменной от тела функции. Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы $x$ свободно входило в $t$ , не обязательно — в этом случае $λ x . t$ обозначает функцию $x \mapsto t$ , то есть такую, которая игнорирует свой аргумент.

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

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

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

Для абстракций, терм $λ y . t [y]$ $α$ -эквивалентен $λ x . t [x]$ , если $t [y]$ это $t [x]$ в котором все свободные появления $x$ заменены на $y$ , при условии, что 1.) $y$ не входит свободно в $t [x]$ , и 2.) $x$ не входит свободно ни в одну абстракцию $λ y$ внутри $t [x]$ (если такие есть).

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

Второе требование необходимо, чтобы предотвратить случаи, подобные тому, когда, например, $λ y . x$ является частью $t [x]$ . Тогда необходимо произвести $α$ -преобразование такой абстракции, например, в данном случае, в $λ z . x$ .

β-редукция

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

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

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

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

(λ x . t) a = t [x : = a]

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

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

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

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

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

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

Функция двух переменных $x$ и $y$ $f (x, y) = x + y$ может быть рассмотрена как функция одной переменной $x$ , возвращающая функцию одной переменной $y$ , то есть как выражение $λ x . λ 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]. На основе этих построений была создана Шаблон:Iw языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.

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

Шаблон:Main

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

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

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

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

U := λh. h h

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

где $U$ — это комбинатор самоприменения (самоаппликации), $U h = 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))} )

Последнее выражение полностью эквивалентно исходному. Оно состоит из аппликации двух независимых λ-термов, где второй терм в выражении (ниже, $G$ ) — это просто лямбда-выражение рекурсивной функции без изменений, но с абстрагированным рекурсивным вызовом $(λ 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$ создает рекурсивную функцию из аргумента, являющегося закрытым (то есть в котором нет свободных переменных) λ-термом исходного выражения функции (то есть без удвоения параметра). Таким образом,

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

то есть $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$ — это закрытый функционал, то есть λ-терм, вызывающий свой аргумент в качестве функции; его неподвижная (зафиксированная, неизменяемая) точка — это функция (здесь, $F$ ), которая передаётся ему в качестве аргумента; а вызов той же самой функции и есть рекурсивный вызов.

Комбинатором называют замкнутое лямбда-выражение, не содержащее свободных переменных и ссылающееся исключительно на свои аргументы. При этом оно может использовать комбинаторы из ограниченного набора базовых, считающихся примитивными. Существуют различные базисы комбинаторной логики, среди которых наиболее известны $S, K, I$ и $B, C, W, K$ . Эти базисы являются взаимно выразимыми, то есть любой комбинатор из одного базиса можно представить через комбинаторы другого. В частности, комбинаторы $U$ и $Y$ , как и любые другие, могут быть выражены в обеих системах.

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

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 (CBU g)
    = BU(CBU) g
    = SSI(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ми других комбинаторов неподвижной точки являются, например, комбинатор Тьюринга $Θ$ и комбинатор $Y^{'}$ :

Θ := (λhg. g (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)

Итак, чтобы определить факториал как рекурсивную функцию, мы можем просто написать $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

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

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

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

См. также

Примечания

Шаблон:Примечания

Литература

Шаблон:Книга

Шаблон:Rq

↑ 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.

[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]

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

Содержание

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

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

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

β-редукция

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

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

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

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

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

См. также

Примечания

Литература

Навигация

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

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

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

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

β-редукция

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

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

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

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

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

См. также

Примечания

Литература

Навигация

Поиск