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

Материал из Википедии — свободной энциклопедии

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

λ-исчисление может рассматриваться как семейство прототипных языков программирования. Их основная особенность состоит в том, что они являются языками высших порядков. Тем самым обеспечивается систематический подход к исследованию операторов, аргументами которых могут быть другие операторы, а значением также может быть оператор. Языки в этом семействе являются функциональными, поскольку они основаны на представлении о функции или операторе, включая функциональную аппликацию и функциональную абстракцию.

Содержание 1 Чистое λ-исчисление 2 Аппликация и абстракция 3 β-редукция 4 Карринг 5 Модели бестипового λ-исчисления 6 См. также 7 Ссылки 8 Литература

[править] Чистое λ-исчисление

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

[править] Аппликация и абстракция

В основу λ-исчисления положены две фундаментальные операции: аппликация и абстракция. Аппликация означает применение или вызов функции по отношению к заданному значению. Её обычно обозначают как f.a, где f — функция, а a — значение, или же просто как конкатенацию fa. Это соответствует общепринятой в математике записи f(a), которая тоже иногда используется, однако для λ-исчисления важно то, что f трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация f к a может рассматриваться двояко: как результат применения f к a, или же как процесс вычисления fa. Последняя интерпретация аппликации связана с понятием β-редукции.

Абстракция или λ-абстракция в свою очередь строит функции по заданным выражениям. Именно, если — выражение, свободно содержащее x, λx.t[x] обозначает функцию . Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы x свободно входило в t, не очень существенно — достаточно предположить, что , если это не так.

[править] β-редукция

Поскольку выражение обозначает функцию, ставящую в соответствие каждому x значение , то для вычисления выражения

,

в которое входят и аппликация и абстракция, необходимо выполнить подстановку числа 3 в терм . В результате получается . Это соображение в общем виде записывается как

(λx.t)a = t[a / x],

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

[править] Карринг

Функция двух переменных x и y f(x,y) = x + y может быть рассмотрена как функция одной переменной x, возвращающая функцию одной переменной y, то есть как выражение λx.λy.x + y. Такой приём работает точно также для функций любой арности. Это показывает, что функции многих переменных могут быть без проблем выражены в λ-исчислении и являются «синтаксическим сахаром». Описанный процесс превращения функций многих переменных в функцию одной переменной называется карринг (также: каррирование), в честь американского математика Хаскелла Карри, хотя первым его предложил М. И. Шейнфинкель (1924).

[править] Модели бестипового λ-исчисления

Применение бестипового λ-исчисления вызывало теоретические трудности, которые удалось преодолеть Д.С. Скотту. Им была разработана модель бестипового λ-исчисления ^[1], для чего предварительно была развита теория аппроксимационных решеток^[2].

[править] См. также

• Аппликативные вычислительные системы
• λ-исчисление с типами
• Комбинаторная логика
• Функциональное программирование
• Категориальная абстрактная машина
• Декартово-замкнутая категория
• Модели вычислений
• Теория вычислений
• Суперкомбинаторы
• Подстановка

[править] Ссылки

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

[править] Литература

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

Это незавершённая статья по информатике. Вы можете помочь проекту, исправив и дополнив её.