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

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

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

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

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

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

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

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

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

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

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

${\displaystyle (\lambda x.2\cdot x+1)\ 3,}$

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

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

${\displaystyle (\lambda x.t)\ a=t[x:=a]}$

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

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

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

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

Функция двух переменных ${\displaystyle x}$ и ${\displaystyle y}$ ${\displaystyle f(x,y)=x+y}$ может быть рассмотрена как функция одной переменной ${\displaystyle x}$, возвращающая функцию одной переменной ${\displaystyle y}$, то есть как выражение ${\displaystyle \ \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...

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

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

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

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

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

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

U := λh. h h

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

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

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

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

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

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

Итак, ${\displaystyle G}$ — это закрытый функционал, то есть λ-терм, вызывающий свой аргумент в качестве функции; его неподвижная (зафиксированная, неизменяемая) точка — это функция (здесь, ${\displaystyle F}$), которая передаётся ему в качестве аргумента; а вызов той же самой функции и есть рекурсивный вызов.

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

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

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

Используя стандартные комбинаторы ${\displaystyle B}$ и ${\displaystyle 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ми других комбинаторов неподвижной точки являются, например, комбинатор Тьюринга ${\displaystyle \Theta }$ и комбинатор ${\displaystyle 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)

Итак, чтобы определить факториал как рекурсивную функцию, мы можем просто написать ${\displaystyle \operatorname {Y} G\ n}$, где ${\displaystyle n}$ — число, для которого вычисляется факториал. Пусть ${\displaystyle 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

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

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

• Типизированное λ-исчисление
• Комбинаторная логика
• Функциональное программирование
• Теорема Чёрча — Россера

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

У этой статьи есть несколько проблем, помогите их исправить: В этой статье есть формулы, которые необходимо оформить. Пожалуйста, помогите улучшить их отображение. (11 сентября 2023) Стиль этой статьи неэнциклопедичен или нарушает нормы литературного русского языка. Статью следует исправить согласно стилистическим правилам Википедии. (11 сентября 2023) Достоверность этой статьи поставлена под сомнение. Необходимо проверить точность фактов и достоверность сведений, изложенных в этой статье. Соответствующую дискуссию можно найти на странице обсуждения. (11 сентября 2023) В статье есть список источников, но не хватает сносок. Без сносок сложно определить, из какого источника взято каждое отдельное утверждение. Вы можете улучшить статью, проставив сноски на источники, подтверждающие информацию. Сведения без сносок могут быть удалены. (11 сентября 2023) Пожалуйста, после исправления проблемы исключите её из списка параметров. После устранения всех недостатков этот шаблон может быть удалён любым участником.