~2026-19541-98: добавил забытую

2026-03-29T18:57:21Z

добавил забытую </tt>

Новая страница

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

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

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

* {{Якорь|Аппликация}}''Аппликация'' ({{lang-lat|applicatio}} — прикладывание, присоединение) означает применение функции к заданному значению аргумента (то есть вызов функции). Её обычно обозначают <math>f\ a</math>, где <math>f</math> — функция, а <math>a</math> — аргумент. Это соответствует общепринятой в математике записи <math>f(a)</math>, которая тоже иногда используется, однако для λ-исчисления важно то, что <math>f</math> трактуется как [[алгоритм]], вычисляющий результат по заданному входному значению. В этом смысле аппликация <math>f</math> <math>a</math> может рассматриваться двояко: как результат применения <math>f</math> к <math>a</math>, или же как процесс вычисления этого результата. Последняя интерпретация аппликации связана с понятием ''β-редукции''.
* {{Якорь|Абстракция}}''Абстракция'' или ''λ-абстракция'' ({{lang-lat|abstractio}} — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если <math>t\equiv t[x]</math> — выражение, {{не переведено 5|свободная переменная|свободно|en|Free variables and bound variables}} содержащее <math>x</math>, тогда запись <math>(\lambda x.t[x])</math> означает: λ функция от аргумента <math>x</math>, которая имеет вид <math>t[x]</math>, и обозначает функцию <math>x\mapsto t[x]</math>. Здесь скобки не обязательны и использованы для ясности, так как точка является частью нотации и отделяет имя связанной переменной от тела функции. Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы <math>x</math> свободно входило в <math>t</math>, не обязательно — в этом случае <math>\ \lambda x.t</math> обозначает функцию <math>x\mapsto t</math>, то есть такую, которая игнорирует свой аргумент.

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

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

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

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

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

== β-редукция ==
Применение некой функции к некоему аргументу выражается в <math>\lambda</math>-исчислении как ''аппликация'' <math>\lambda</math>-терма, выражающего эту функцию, и <math>\lambda</math>-терма аргумента. Например, применение функции <math>f(x) = 2x+1</math> к числу 3 выражается аппликацией
: <math>(\lambda x. 2\cdot x + 1)\ 3,</math>
в которой на первом месте находится соответствующая ''абстракция''. Поскольку эта функция ставит в соответствие каждому <math>x</math> значение <math>2x+1</math>, для вычисления результата необходимо [[подстановка|заменить]] каждое свободное появление переменной <math>x</math> в терме <math>2\cdot x + 1</math> на терм 3.

В результате получается <math>2\cdot 3+1=7</math>. Это соображение в общем виде записывается как
: <math>(\lambda x.t)\ a = t[x:=a]</math>
и носит название ''β-редукция''. Выражение вида <math>(\lambda x.t)\ a</math>, то есть применение абстракции к некоему терму, называется ''редексом'' (redex). Несмотря на то, что β-редукция по сути является единственной «существенной» [[аксиома|аксиомой]] λ-исчисления, она приводит к весьма содержательной и сложной теории. Вместе с ней λ-исчисление обладает свойством [[полнота по Тьюрингу|полноты по Тьюрингу]] и, следовательно, представляет собой простейший [[язык программирования]].

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

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

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

== Каррирование (карринг) ==
Функция двух переменных <math>x</math> и <math>y</math> <math>f(x,y) = x + y</math> может быть рассмотрена как функция одной переменной <math>x</math>, возвращающая функцию одной переменной <math>y</math>, то есть как выражение <math>\ \lambda x.\lambda y.x+y</math>. Такой приём работает точно так же для функций любой [[арность|арности]]. Это показывает, что функции многих переменных могут быть выражены в λ-исчислении и являются «[[синтаксический сахар|синтаксическим сахаром]]». Описанный процесс превращения функций многих переменных в функцию одной переменной называется ''карринг'' (также: [[каррирование]]), в честь американского математика [[Карри, Хаскелл|Хаскелла Карри]], хотя первым его предложил [[Шейнфинкель, Моисей Эльевич|Моисей Шейнфинкель]] ([[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...

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

Эту трудность в начале 1970-х годов преодолел [[Скотт, Дана Стюарт|Дана Скотт]], построив понятие [[Область Скотта|области]] <math>D</math> (изначально на [[Полная решётка|полных решётках]]<ref>''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.</ref>, в дальнейшем обобщив до полного частично упорядоченного множества со [[топология Скотта|специальной топологией]]) и урезав ''<math>D \to D</math>'' до [[Непрерывность по Скотту|непрерывных в этой топологии функций]]<ref>''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.</ref>. На основе этих построений была создана {{iw|Денотационная семантика|денотационная семантика|en|Denotational semantics}} [[Язык программирования|языков программирования]], в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как [[Рекурсия#Рекурсия в программировании|рекурсия]] и [[Тип данных|типы данных]].

== Связь с рекурсивными функциями ==
{{Main|Комбинатор неподвижной точки}}

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

::: <math>fact(n) \triangleq \{ 1, \text{ if } n = 0; \text{ else } n \times fact(n - 1) \} </math>

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

:  <tt>G := λr.λn.{ 1, if n = 0; else n × (r (n-1)) }</tt>

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

:  <tt>Fact = G Fact = G (G Fact) = G (G (G (...)))</tt>

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

:  <tt>Fact n = G Fact n = G (G Fact) n = G (G (G (...))) n</tt>

Функция <math>fact</math> ссылается на саму себя посредством ссылки на своё имя, но в лямбда-исчислении у λ-термов имен нет. Разрешение ссылки по имени достигается в программировании посредством лексического связывания через глобальный контекст, но в лямбда исчислении он является неизменяемым. В отсутствие изменяемого глобального контекста, ''локальный'' контекст создаётся использованием дополнительных аргументов:

::: <math>\begin{align}
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{align}</math>

Здесь функция <math>f(h,n)</math> использует аргумент <math>h</math> и как функцию для вызова, в качестве "следующего шага вычислений", и передаёт его как дальнейший аргумент для последующего использования самой же вызванной фунцкцией <math>h</math>. Вызов функции-аргумента для выполнения остатка вычислений называется "открытой рекурсией", потому что <math>h</math> гипотетически может быть чем угодно. Вызов функции <math>f</math> с ''самой собой'' в качестве аргумента на самом верхнем уровне, <math>f(f,n)</math>, "замыкает кольцо" и позволяет функции ссылаться на ''саму себя'' внутри своего тела, таким образом создавая функцию <math>fact\text{′}</math> полностью эквивалентную оригинальной рекусивной функции <math>fact</math>.

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

В таком виде это синтаксически не-рекурсивное определение <math>fact\text{′}</math> напрямую выражается как λ-терм:

:  <tt>F := λh. λn. { 1, if n = 0; else n × ((h h) (n-1)) }</tt>
:  <tt>   = λh. (λr.λn.{ 1, if n = 0; else n × (r (n-1)) }) (h h)</tt>
:  <tt>   = λh. G (h h)</tt>
:  <tt>Fact := F F</tt>

Итак <tt>F h = G (h h)</tt>, и следовательно <tt>F F = G (F F)</tt>. λ-терм <tt>(F F)</tt> является неподвижной точкой λ-терма <tt>G</tt>, т.е. представлением рекурсивной функции <math>fact</math>, и G ссылается на него через параметр <tt>r</tt>, выполняя тождество:

:  <tt>Fact := F F = G (F F) = G Fact = G (G (G (...)))</tt>
:  <tt>      = U F =      U (λh. G (h h))</tt>
:  <tt>            = (λg. U (λh. g (h h))) G =: Y G</tt>
:  <tt>U := λh. h h</tt>

где <math>U</math> — это комбинатор самоприменения (самоаппликации), <math>U h = h\ h</math>. Так несколькими элементарными само-очевидными преобразованиями сам собой получается т.н. "комбинатор неподвижной точки" (см. ниже), <math>Y</math>,

:  <tt>Y := λg. U (λh. g (h h))</tt>
:  <tt>Fact := Y G = G (Y G)</tt>

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

:  <tt>Y g = U λh. g (h h) = g (U λh. g (h h)) = g (Y g)</tt>

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

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

Итак, <math>G</math> — это закрытый функционал, то есть λ-терм, вызывающий свой аргумент в качестве функции; его неподвижная (зафиксированная, ''неизменяемая'') точка — это функция (здесь, <math>Y G =: Fact</math>), которая передаётся ему в качестве аргумента; а вызов ''той же самой'' функции и есть ''рекурсивный'' вызов.

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

:  <tt>Fact n = Y G n = G (Y G) n = G (G (G (...))) n</tt>
:  <tt>       = { 1, if n = 0; else n × (Y G (n-1)) } = ...</tt>

Чтобы определить факториал как рекурсивную функцию, мы можем просто написать <math>\operatorname{Y} G\ n</math>, где <math>n</math> — число, для которого вычисляется факториал. Пусть <math>n = 4</math>, получаем (подразумевая [[каррирование]], <tt>(a b c) = ((a b) c)</tt>):

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

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

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

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

:  <tt>Y := λg. (λh. h h) (λh. g (h h))</tt>

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

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ми других комбинаторов неподвижной точки являются, например, комбинатор Тьюринга <math>\Theta</math> и комбинатор <math>Y\text{′}</math>:
:  <tt>Θ  := (λhg. h h g) (λhg. g (h h g))</tt>
:  <tt>    = U(B(SI)U) = SII(S(K(SI))(SII))</tt>
:  <tt>Y′ := (λhg. h g h) (λgh. g (h g h))</tt>
:  <tt>    = WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K)</tt>

== В языках программирования ==
В языках программирования под «λ-исчислением» зачастую{{Нет АИ|11|2|2025}} понимается механизм «[[анонимная функция|анонимных функций]]» — [[Callback (программирование)|callback]]-функций, которые можно определить прямо в том месте, где они используются, и которые имеют доступ ко всем [[Переменная (программирование)|переменным]], видимым в месте их вызова в текущей функции ([[Замыкание (программирование)|замыкание]]).

== См. также ==
* [[Кодирование Чёрча]]
* [[Типизированное лямбда-исчисление|Типизированное λ-исчисление]]
* [[Комбинаторная логика]]
* [[Функциональное программирование]]
* [[Теорема Чёрча — Россера]]

== Примечания ==
{{примечания}}

== Литература ==
* {{книга
|автор = [[Барендрегт, Хенк]]
|заглавие = Ламбда-исчисление. Его синтаксис и семантика
|место = М.
|издательство = [[Мир (издательство)|Мир]]
|год = 1985
|страниц = 606
|тираж = 4800
}}

{{rq|
{{оформить формулы|дата=2023-09-11}}
{{стиль статьи|дата=2023-09-11}}
{{проверить факты|дата=2023-09-11}}
{{нет сносок|дата=2023-09-11}}
}}

[[Категория:Теория алгоритмов]]
[[Категория:Лямбда-исчисление]]
[[Категория:Модели вычислений]]
[[Категория:Формальные методы]]

Лямбда-исчисление - История изменений

~2026-19541-98: добавил забытую