Русская Википедия:Лямбда-исчисление
Ля́мбда-исчисле́ние (λ-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости.
Чистое λ-исчисление
Чистое λ-исчисление, термы которого, называемые также объектами («обами»), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличие каких-либо констант не предполагается.
Аппликация и абстракция
В основу λ-исчисления положены две фундаментальные операции:
- Аппликация (Шаблон:Lang-lat — прикладывание, присоединение) означает применение функции к заданному значению аргумента (т.е. вызов функции). Её обычно обозначают <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 — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если <math>t\equiv t[x]</math> — выражение, Шаблон:Не переведено 5 содержащее <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> (изначально на полных решётках[1], в дальнейшем обобщив до полного частично упорядоченного множества со специальной топологией) и урезав <math>D \to D</math> до непрерывных в этой топологии функций[2]. На основе этих построений была создана Шаблон:Iw языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.
Связь с рекурсивными функциями
Рекурсия — это определение функции через саму себя; на первый взгляд, лямбда-исчисление не позволяет этого, но это впечатление обманчиво. Например, рассмотрим рекурсивную функцию <math>f</math>, вычисляющую факториал:
- f(n) = 1, if n = 0; else n × f(n - 1).
Эта функция не может быть выражена λ-термом (λn.(1, if n = 0; else n × (f (n-1)))), так как в нём f является свободной переменной. Функция <math>f</math> ссылается на саму себя посредством ссылки на своё имя, но в лямбда-исчислении у λ-термов имен нет.
Тем не менее, λ-термы могут быть переданы как аргумент, в том числе и самим себе. Терм-функция может получить сам себя как аргумент, который окажется связанным с его параметром. Как правило, этот параметр стоит на первом месте. Когда он связан с самой функцией, получается новый λ-терм, выражающий уже саму рекурсивную функцию. Для этого параметр, ссылающийся на себя (здесь обозначен как <math>h</math>), обязательно должен быть передан явным образом как аргумент при рекурсивном вызове (как <math>h\ h</math>):
- U := λh. h h
- F := U (λh. λn. (1, if n = 0; else n × ((h h) (n-1))))
где <math>U</math> - это комбинатор само-аппликации, <math>U h = h\ h</math>.
Этот приём позволяет решить каждую конкретную проблему, как вычисление факториала здесь, создавая рекурсивную функцию через изменение λ-терма, для его явной передачи самому себе как добавочного аргумента. Но решение в общем виде также возможно. Несколькими несложными преобразованиями получается (подразумевая каррирование):
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))))
Это эквивалентое выражение состоит из аппликации двух независимых λ-термов, где второй - это просто лямбда-выражение рекурсивной функции без изменений, но с абстрагированным рекурсивным вызовом <math>(\lambda r)</math>. А первый это некий комбинатор, называемый <math>Y</math>:
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)
т.е. <math>\operatorname{Y}</math> - это комбинатор неподвижной точки: он вычисляет неподвижную точку своего аргумента. Для закрытого λ-терма с соотвествующей арностью, его неподвижная точка выражает рекурсивную функцию, так как <math>Y\ g\ n = g\ (Y\ g)\ n</math>, т.е. аргумент который здесь создаётся для вызова внутри <math>g</math> - это та же самая функция <math>Y\ g\ </math>.
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
Итак, <math>G</math> - это закрытый функционал, т.е. λ-терм, вызывающий свой аргумент в качестве функции; его неподвижная точка - это функция (здесь, <math>F</math>), которая передаётся ему в качестве аргумента; а вызов той же самой функции и есть рекурсивный вызов.
Существует несколько определений комбинаторов неподвижной точки. Вышеуказанное - самое простое:
- Y := λg. (λh. g (h h)) (λh. g (h h))
Используя стандартные комбинаторы <math>B</math> и <math>C</math>,
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)
Итак, чтобы определить факториал как рекурсивную функцию, мы можем просто написать <math>\operatorname{Y} G\ n</math>, где <math>n</math> — число, для которого вычисляется факториал. Пусть <math>n = 4</math>, получаем:
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>, каждое рекурсивное определение может быть выражено как лямбда-выражение (λ-терм). В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно, и выразить их как λ-термы.
В языках программирования
В языках программирования под «λ-исчислением» зачастую понимается механизм «анонимных функций» — callback-функций, которые можно определить прямо в том месте, где они используются, и которые имеют доступ ко всем переменным видимым в месте их вызова в текущей функции (замыкание).
См. также
- Аппликативные вычислительные системы
- Типизированное λ-исчисление
- Комбинаторная логика
- Функциональное программирование
- Теорема Чёрча — Россера
- Анонимная функция
Примечания
Литература
- Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика: Пер. с англ. — М.: Мир, 1985. — 606 с.
- ↑ 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.
