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

Ламбда-исчисление было изобретено Алонсом Чёрчем около 1930 г. Чёрч первоначально строил l-исчисление как часть общей системы функций, которая должна стать основанием математики. Но из-за найденных парадоксов эта система оказалась противоречивой. Книга Чёрча [2] содержит непротиворечивую подтеорию его первоначальной системы, имеющую дело только с функциональной частью. Эта теория и есть l-исчисление.

Ламбда-исчисление - это безтиповая теория, рассматривающая функции как правила, а не как графики. В противоположность подходу (вводимому функции как множество пар, состоящих из аргумента и значения) более старое понятие определяет функцию как процесс перехода от аргумента к значению. С первой точки зрения x²-4 и (x+2)(x-2) - разные обозначения одной и той же функции; со второй точки зрения это разные функции.

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

Ламбда-исчисление представляет класс (частичных) функций (l-определимые функции), который в точности характеризует неформальное понятие эффективной вычислимости. Другими словами, l-исчисления, наряду с другими подходами формализует понятие алгоритма [7, с. 143-146].

Ламбда-исчисление стало объектом особенно пристального внимания в информатике после того, как выяснилось, что оно представляет собой удобную теоретическую модель современного функционального программирования [32].

Большинство функциональных языков программирования, например, Лисп, используют l-исчисление в качестве промежуточного кода, в который можно транслировать исходную программу. Функциональные языки "улучшают" нотацию l-исчисления в прагматическом смысле, но при этом, в какой-то мере, теряется элегантность и простота последнего.

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