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

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

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

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

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

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

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

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

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

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

Поскольку выражение $\lambda x. 2\cdot x + 1$ обозначает функцию, ставящую в соответствие каждому $x$ значение $2\cdot x + 1$ , то для вычисления выражения

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

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

$(\lambda x.t)\ a = t[x:=a],$

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

[править] η-преобразование

η-преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применённые к любому аргументу, дают одинаковые результаты. η-преобразование переводит друг в друга формулы $\lambda x.\ f x$ и $f$ (в обратную сторону в только если $x$ не имеет свободных вхождений в $f$ : иначе свободная переменная $x$ после преобразования станет связанной внешней абстракцией).

[править] Каррирование (карринг)

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

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

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

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

[править] Связь с рекурсивными функциями

Основная статья: Комбинатор неподвижной точки

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

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

В лямбда-исчислении, функция не может непосредственно ссылаться на себя. Тем не менее, функции может быть передан параметр, связанный с ней. Как правило, этот аргумент стоит на первом месте. Связав его с функцией, мы получаем новую, уже рекурсивную функцию. Для этого, аргумент, ссылающийся на себя (здесь обозначен как r), обязательно должен быть передан в тело функции.

g := λr. λn.(1, if n = 0; else n × (r r (n-1)))

f := g g

Это решает специфичную проблему вычисления факториала, но решение в общем виде также возможно. Получив лямбда-терм, представляющий тело рекурсивной функции или цикл, передав себя в качестве первого аргумента, комбинатор неподвижной точки возвратит необходимую рекурсивную функцию или цикл. Функции не нуждаются в явной передаче себя каждый раз. Так как существует несколько определений комбинаторов неподвижной точки. Самый простой из них:

Y = λg.(λx.g (x x)) (λx.g (x x))

В лямбда-исчислении, Y g в неподвижная точка g; продемонстрируем это:

Y g

λh.((λx.h (x x)) (λx.h (x x))) g

(λx.g (x x)) (λx.g (x x))

g ((λx.g (x x)) (λx.g (x x)))

g (Y g).

Теперь, чтобы определить факториал, как рекурсивную функцию, мы можем просто написать g (Y g) n, где n в число, для которого вычисляется факториал. Пусть n = 4, получаем:

   g (Y g) 4
   (λfn.(1, if n = 0; and n·(f(n-1)), if n>0)) (Y g) 4
   (λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0)) 4
   1, if 4 = 0; and 4·(g(Y g) (4-1)), if 4>0
   4·(g(Y g) 3)
   4·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 3)
   4·(1, if 3 = 0; and 3·(g(Y g) (3-1)), if 3>0)
   4·(3·(g(Y g) 2))
   4·(3·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 2))
   4·(3·(1, if 2 = 0; and 2·(g(Y g) (2-1)), if 2>0))
   4·(3·(2·(g(Y g) 1)))
   4·(3·(2·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 1)))
   4·(3·(2·(1, if 1 = 0; and 1·((Y g) (1-1)), if 1>0)))
   4·(3·(2·(1·((Y g) 0))))
   4·(3·(2·(1·((λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 0))))
   4·(3·(2·(1·(1, if 0 = 0; and 0·((Y g) (0-1)), if 0>0))))
   4·(3·(2·(1·(1))))
   24

Каждое определение рекурсивной функции может быть представлено как неподвижная точка соответствующей функции, следовательно, используя Y, каждое рекурсивное определение может быть выражено как лямбда-выражение. В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно.

[править] В языках программирования

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

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

[править] Примечания

в‘ 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 с.
Чечулин В. Л. О непротиворечивости лямбда-исчисления // В мире научных открытий, серия Математика. Механика. Информатика, 2011, в„– 1, сс. 203в206

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

[0] в‘ 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.

[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.

[1]

[2]

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

Содержание

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

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

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

[править] η-преобразование

[править] Каррирование (карринг)

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

[править] Связь с рекурсивными функциями

[править] В языках программирования

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

[править] Примечания

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

Личные инструменты

Пространства имён

Варианты

Просмотры

Действия

Поиск

Навигация

Участие

Печать/экспорт

Инструменты

На других языках