Ламбда–исчисление как формальная система. Синтаксис и семантика λ–исчисления

Ламбда–исчисление Желтая река течет тысячи миль на север…

Затем поворачивает на восток и течет непрерывно,

Не важно, как она изгибается и поворачивается,

Её воды выходят из источника на горе Кунь–Лунь.

Железная флейта

1 Ламбда–исчисление как формальная система

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

Ламбда–исчисление было изобретено Алонзом Чёрчем (Alonzo Church, американ-ский логик и математик, 1903–1995) около 1930 г. Чёрч первоначально строил λ–исчисление как часть общей системы функций, которая должна стать основанием матема-тики. Но из–за найденных парадоксов эта система оказалась противоречивой. Книга Чёрча [¹] содержит непротиворечивую подтеорию его первона-чальной системы, имеющую дело только с функциональ-ной частью. Эта теория и есть λ–исчисление.

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

Что значит «функция 5x³+2»? Если кто–то хочет быть точным, он вводит по этому поводу функциональ-ный символ, например f, и говорит: «функция f: R → R, определенная соотношением f(x) = 5x³+2». При этом, оче-видно, что переменную x можно здесь, не меняя смысла, заменить на другую переменную y. Ламбда–запись устраняет произвольность в выборе f в качестве функционального символа. Она предлагает вместо f выражение «λx.5x³+2».

Кроме того, обычная запись f(x) может обозначать как имя функции f, так и вызов функции с аргументом x. Для более строгого подхода это необходимо различать. В лам-бда–обозначениях вызов функции с аргументом x выглядит как (λx. 5x³+2)x.

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

Ламбда–исчисление представляет класс (частичных) функций (λ–определимые функции), который в точности характеризует неформальное понятие эффективной вычис-лимости. Другими словами, λ–исчисления, наряду с другими подходами формализует по-нятие алгоритма. И в настоящее время лямбда-исчисление является основной формализа-

  Алонсо Чёрч

¹ Church A. The Calculi of Lambda Conversion. Princeton University Press, Princeton, 1941.

1 цией. Одной из причин этого является следующий факт – это единственная формализация, которая, хотя и с некоторыми неудобствами, действительно может быть непосредственно использована для написания программ.

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

Функциональные языки являются в основном удобной формой синтаксической за-писи для конструкций различных вариантов лямбда-исчисления (соответствующие откло-нения в языке от синтаксиса лямбда-выражений называется «синтаксическим сахаром»). Некоторые современные языки (Haskell, Clean) имеют 100% соответствие своей семанти-ки с семантикой подразумеваемых конструкций лямбда-исчисления. Причем, λ–выражения используются в качестве промежуточного кода, в который можно транслиро-вать исходную программу. Функциональные языки «улучшают» нотацию λ–исчисления в прагматическом смысле, но при этом, в какой–то мере, теряется элегантность и простота последнего.

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

Язык ламбда–исчисления является сейчас одним из важнейших выразительных средств в логике, информатике, математической лингвистике, искусственном интеллекте и когнитивной науке.

Синтаксис и семантика λ–исчисления

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

Определение λ–выражений (λ–термов)

Имеется три вида λ–выражений: •

  Переменные: x, y и т. д.

  • Функциональная аппликация: если M и N есть произвольные λ–термы, то можно по-строить новый λ–терм (MN) (обозначающий применение, или аппликацию, оператора M к аргументу N). Например, если (<m>, <n>) обозначает функцию, представляющую пару чисел