Лямбда-исчисление
Ля́мбда-исчисле́ние (λ-исчисление, лямбда-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем, для формализации и анализа понятия вычислимости.
λ-исчисление может рассматриваться как семейство прототипных языков программирования. Их основная особенность состоит в том, что они являются языками высших порядков. Тем самым обеспечивается систематический подход к исследованию операторов, аргументами которых могут быть другие операторы, а значением также может быть оператор. Языки в этом семействе являются функциональными, поскольку они основаны на представлении о функции или операторе, включая функциональную аппликацию и функциональную абстракцию.
λ-исчисление реализовано Джоном Маккарти в языке Лисп. В начале реализация идеи λ-исчисления была весьма громоздкой. Но по мере развития Лисп-технологии (прошедшей этап аппаратной реализации в виде Лисп-машины) идеи получили ясную и четкую реализацию.
Чистое λ-исчисление
Это простейший из семейства прототипных языков программирования, чистое λ-исчисление, термы которого, называемые также объектами (обами), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличия каких-либо констант не предполагается.
Аппликация и абстракция
В основу λ-исчисления положены две фундаментальные операции: аппликация и абстракция. Аппликация означает применение или вызов функции по отношению к заданному значению. Её обычно обозначают <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>, или же как процесс вычисления <math>f\ a</math>. Последняя интерпретация аппликации связана с понятием β-редукции.
Абстракция или λ-абстракция в свою очередь строит функции по заданным выражениям. Именно, если <math>t\equiv t[x]</math> — выражение, свободно содержащее <math>x</math>, тогда <math>\ \lambda x.t[x]</math> (эта запись означает: <math>\lambda</math> функция от аргумента <math>x</math>, которая имеет вид <math>t[x]</math>) обозначает функцию <math>x\mapsto t[x]</math>. Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы <math>x</math> свободно входило в <math>t</math>, не очень существенно — достаточно предположить, что <math>\lambda x.t\equiv t</math>, если это не так.
β-редукция
Поскольку выражение <math>\lambda x. 2\cdot x + 1</math> обозначает функцию, ставящую в соответствие каждому <math>x</math> значение <math>2\cdot x + 1</math>, то для вычисления выражения
в которое входят и аппликация и абстракция, необходимо выполнить подстановку числа 3 в терм <math>2\cdot x + 1</math> вместо переменной <math>x</math>. В результате получается <math>2\cdot 3+1=7</math>. Это соображение в общем виде записывается как
и носит название β-редукция. Выражение вида <math>(\lambda x.t)\ a</math>, то есть применение абстракции к некому терму, называется редексом (redex). Несмотря на то, что β-редукция по сути является единственной «существенной» аксиомой λ-исчисления, она приводит к весьма содержательной и сложной теории. Вместе с ней λ-исчисление обладает свойством полноты по Тьюрингу и, следовательно, представляет собой простейший язык программирования.
η-преобразование
η-преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применённые к любому аргументу, дают одинаковые результаты. η-преобразование переводит друг в друга формулы <math>\lambda x.\ f x</math> и <math>f</math> (в обратную сторону — только если <math>x</math> не имеет свободных вхождений в <math>f</math>: иначе свободная переменная <math>x</math> после преобразования станет связанной внешней абстракцией).
Надо отметить, что если рассматривать лямбда-термы не как функции, а именно как алгоритмы, то данное преобразование не всегда уместно: существуют случаи, когда вычисление <math>\lambda x. f\ x</math> завершается, а вычисление <math>f</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).
Семантика бестипового λ-исчисления
Тот факт, что термы λ-исчисления действуют как функции, применяемые к термам λ-исчисления (то есть, возможно, к самим себе), приводит к сложностям построения адекватной семантики λ-исчисления. Можно ли приписать λ-исчислению какой-либо смысл? Желательно иметь множество D, в которое вкладывалось бы его пространство функций D → D. В общем случае такого D не существует по соображениям ограничений на мощности этих двух множеств, D и функций из D в D: второе имеет большую мощность, чем первое.
Эту трудность преодолел Д. С. Скотт, построив понятие области D (полной решётки[1] или, более общо, полного частично упорядоченного множества со специальной топологией) и урезав D → D до непрерывных (в имеющейся топологии) функций[2]. После этого также стало понятно, как можно строить денотационную семантику языков программирования. Это произошло благодаря тому, что с помощью конструкций Скотта можно придать значение также двум важным конструкциям языков программирования — рекурсии и типам данных.
Связь с рекурсивными функциями
См. также
- Аппликативные вычислительные системы
- Типизированное λ-исчисление
- Комбинаторная логика
- Функциональное программирование
Ссылки
- ↑ 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.
Литература
- Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика: Пер. с англ. — М.: Мир, 1985. — 606 с.
| Информатика | Это незавершённая статья по информатике. Вы можете помочь проекту, исправив и дополнив её. |
ar:حسابات اللامدا bn:ল্যাম্ডা ক্যালকুলাস ca:Càlcul lambda cs:Lambda kalkul de:Lambda-Kalkül el:Λογισμός λάμδα en:Lambda calculus eo:Lambda-kalkulo es:Cálculo lambda fr:Lambda-calcul he:תחשיב למבדא hr:Lambda račun hu:Lambda-kalkulus it:Lambda calcolo ja:ラムダ計算 ko:람다 대수 nl:Lambdacalculus pl:Rachunek lambda pt:Cálculo lambda sh:Lambda račun simple:Lambda calculus sk:Lambda kalkul sv:Lambdakalkyl ta:லம்டா நுண்கணிதம் uk:Лямбда-числення vi:Giải tích lambda zh:Λ演算
Если вам нравится SbUP.com Сайт, вы можете поддержать его - BTC: bc1qppjcl3c2cyjazy6lepmrv3fh6ke9mxs7zpfky0 , TRC20 и ещё....
