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

Лямбда-исчисление — лишь одно из нескольких фундаментальных исчислений, используемых для подобных целей. Пи-исчисление (pi-calculus) Милнера, Пэрроу и Уокера (Milner, Parrow, and Walker, 1992, Milner, 1991)) завоевало популярность как базовый язык для определения семантики языков параллельных вычислений с обменом сообщениями, а исчисление объектов (object calculus) Абади и Карделли (Abadi and Cardelli, 1996) выражает суть объектно-ориентированных языков. Большинство идей и методов, которые мы опишем и разработаем для лямбда-исчисления, можно без особого труда перенести и на эти другие исчисления. Один из примеров такого переноса представлен в главе 19.

Лямбда-исчисление можно расширить и обогатить  несколькими способами. Во-первых, часто  для удобства добавляют особый синтаксис  для чисел, кортежей, записей и  т. п., чье поведение, в принципе, можно смоделировать и в базовом языке. Интереснее добавить более сложные возможности, такие как изменяемые ссылочные ячейки или нелокальная обработка исключений. Эти свойства можно смоделировать на базовом языке только путем достаточно тяжеловесного перевода. Такие расширения, в конце концов, приводят к языкам вроде ML (Gordon, Milner, and Wadsworth, 1979, Milner, Tofte, and Harper, 1990, Weis, Aponte, Laville, Mauny, and Suárez, 1989, Milner, Tofte, Harper, and MacQueen, 1997), Haskell (Hudak et al., 1992) или Scheme (Sussman and Steele, 1975, Kelsey, Clinger, and Rees, 1998). Как мы увидим в последующих главах, расширения базового языка часто требуют расширения системы типов.

5.1  Основы

Процедурная (или функциональная) абстракция — ключевое свойство почти всех языков программирования. Вместо того, чтобы выписывать одно и то же вычисление раз за разом, мы пишем процедуру или функцию, которая проделывает это вычисление в общем виде, используя один или несколько именованных параметров, а затем при необходимости вызываем эту процедуру, каждый раз задавая значения параметров. К примеру, для программиста естественно взять длинное вычисление с повторяющимися частями, вроде

и переписать его в виде factorial(5) + factorial(7) - factorial(3), где

factorial(n)  =  if n=0 then 1 else n * factorial(n-1)

Для каждого неотрицательного числа n подстановка аргумента n в функцию factorial дает в результате факториал n. Используя нотацию <<λn. ...>> обозначающую <<функцию, которая для каждого n, дает …>>, определение factorial можно переформулировать как

factorial = λn. if n=0 then 1 else n * factorial(n-1)

Теперь factorial(0) означает <<функция λn. if n=0 then 1 else ..., примененная к аргументу 0>>, то есть, <<значение, которое получается, если аргумент n в теле функции (λn. if n=0 then 1 else ...) заменить на 0>>, то есть, <<if 0=0 then 1 else ...>>, то есть, 1.

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

Синтаксис лямбда-исчисления состоит из трех видов термов.¹ Переменная x сама по себе есть терм; абстракция переменной x в терме t₁, (записывается как λx.t₁), — тоже терм; и, наконец, применение терма t₁ к терму t₂ (записывается t₁ t₂) — третий вид термов. Эти способы конструирования термов выражаются следующей грамматикой:

t ::=		термы:
	x	переменная
	λx. t	абстракция
	t t	применение

 
В следующих подразделах это определение  изучается детально.

Абстрактный и конкретный синтаксис

При обсуждении синтаксиса языков программирования полезно различать два уровня² структуры. Конкретный синтаксис (concrete syntax, или surface syntax) языка относится к строкам символов, которые непосредственно читают и пишут программисты. Абстрактный синтаксис (abstract syntax) — это намного более простое внутреннее представление программ в виде помеченных деревьев (они называются абстрактными синтаксическими деревьями (abstract syntax trees) или АСД (AST)). Представление в виде дерева делает структуру термов очевидной, и поэтому его удобно использовать для сложных преобразований, которые нужны как при строгом определении языков (и доказательстве их свойств), так и внутри компиляторов и интерпретаторов.

Преобразование  из конкретного в абстрактный  синтаксис происходит в два этапа. Сначала лексический анализатор (lexical analyzer) (или лексер, lexer) переводит последовательность символов, написанных программистом, в последовательность лексем (tokens) — идентификаторов, ключевых слов, комментариев, символов пунктуации, и т. п. Лексический анализатор убирает комментарии, обрабатывает пробелы, решает вопрос с заглавными и строчными буквами, а также распознает форматы числовых и символьных констант. После этого грамматический анализатор (парсер) (parser) преобразует последовательность лексем в абстрактное синтаксическое дерево. При грамматическом разборе соглашения о приоритете (precedence) и ассоциативности (associativity) операторов помогают уменьшить количество скобок в программе, явно указывающих структуру составных выражений. Например, оператор * имеет приоритет выше, чем оператор +, так что анализатор интерпретирует выражение без скобок 1+2*3 как абстрактное синтаксическое дерево, которое показано слева, а не справа:

[.+ 1 [.* 2 3 ] ]      [.* [.+ 1 2 ] 3 ]

В этой книге мы обращаем основное внимание на абстрактный, а не конкретный синтаксис. Грамматики, вроде той, что мы привели  для лямбда-термов, следует рассматривать как описания разрешенных видов деревьев, а не последовательностей лексем или символов. Разумеется, когда мы будем записывать термы в примерах, определениях, теоремах и доказательствах, нам придется выражать их с помощью конкретной, линейной записи, но мы всегда имеем в виду соответствующие абстрактные синтаксические деревья.

Чтобы избежать излишних скобок, для записи лямбда-термов в линейной форме мы следуем двум соглашениям. Во-первых, применение функции лево-ассоциативно — то есть, s t u обозначает то же дерево, что (s t) u:

[.apply [.apply s t ] u ]

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

[.λx [.λy [.apply [.apply x y ] x ] ] ]

 

Переменные и метапеременные

Еще одна тонкость в приведенном определении  синтаксиса касается использования  метапеременных. Мы будем продолжать использовать метапеременную t (а также s и u, с нижними индексами и без них), обозначающую произвольный терм.³ Аналогично, x (а также y и z) замещает произвольную переменную. Заметим, что здесь x — это метапеременная, значениями которой являются другие переменные! К сожалению, число коротких имен ограничено, и нам потребуется иногда использовать x, y и т. д. для обозначения переменных объектного языка. В таких случаях, однако, из контекста всегда будет ясно, что имеется в виду. Например, в предложении <<Терм λx. λy. x y имеет вид λz. s, где z = x, а s = λy. x y>> имеем z и s — имена метапеременных, а x и y — имена переменных объектного языка.

Область видимости

Последнее, что нам требуется разъяснить в синтаксисе лямбда-исчисления, — область видимости (scope) переменных.

Переменная x называется связанной (bound), если она находится в теле t абстракции λx.t. (Точнее, оно связано этой абстракцией. Мы можем также сказать, что λx — связывающее определение(binder) с областью видимости t.) Вхождение x свободно (free), если оно находится в позиции, в которой оно не связано никакой вышележащей абстракцией переменной x. Например, вхождения x в x y и λy. x y свободны, а вхождения x в λx. x и λz. λx. λy. x (y z) связаны. В (λx. x) x первое вхождение x связано, а второе свободно.

Терм  без свободных переменных называется замкнутым (closed); замкнутые термы называют также комбинаторами (combinators). Простейший комбинатор, называемый функцией тождества (identity function),

  id = λx.x;

не  выполняет никаких действий, а  просто возвращает свой аргумент.

Операционная семантика

В своей чистой форме лямбда-исчисление не содержит встроенных констант и  элементарных операторов — ни чисел, ни арифметических операций, ни условных выражений, ни записей, ни циклов, ни последовательного выполнения выражений, ни ввода-вывода, и т. д. Единственное средство для <<вычисления>> термов — применение функций к аргументам (которые сами являются функциями). Каждый шаг вычисления состоит в том, что в терме-применении, в котором левый член является абстракцией, связанная переменная в теле этой абстракции заменяется на правый член. Записывается это так:

(λx.t12) t2 → [x ↦ t2] t12

где [x ↦ t₂] t₁₂ означает <<терм, получаемый из t₁₂ путем замены всех свободных вхождений x на t₂>>. Например, терм (λx. x) y за один шаг вычисления переходит в y, а терм (λx. x (λx. x)) (u r) переходит в u r (λx. x). Вслед за Чёрчем, терм вида (λx. t₁₂) t₂ называется редексом (redex) (reducible expression (redex), <<сокращаемое выражение>>), а операция переписывания редекса в соответствии с указанным правилом называется бета-редукцией (beta-reduction).

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

• При полной бета-редукции (full beta-reduction) в любой момент может сработать любой редекс. На каждом шаге мы выбираем какой-нибудь редекс где-то внутри вычисляемого терма, и проводим шаг редукции. Рассмотрим, например, терм

    (λx.x) ((λx.x) (λz. (λx.x) z))

который можно записать для удобства чтения в виде id (id (λz. id z)). В этом терме содержится три редекса:

    id (id (λz. id z))

    id (id (λz. id z))

    id (id (λz. id z))

При полной бета-редукции можно, например, начать с самого внутреннего редекса, затем обработать промежуточный, а затем — внешний:

	id (id (λz. id z))
→	id (id (λz.z))
→	id (λz.z)
→	λz.z
¬→

• При стратегии нормального порядка вычислений (normal order) всегда сначала сокращается самый левый, самый внешний редекс. При такой стратегии указанный терм обрабатывался бы так:

	id (id (λz. id z))
→	id (λz. id z)
→	λz. id z
→	λz.z
¬→

•  
  При такой стратегии (а также всех перечисленных ниже) отношение вычисления на самом деле является частичной функцией: каждый терм t за шаг переходит не более чем в один терм t′.
• Стратегия вызова по имени (call by name) еще более строга: она не позволяет проводить редукцию внутри абстракций. Начиная с того же самого терма, первые две редукции мы проведем так же, как и при нормальном порядке вычислений, но потом остановимся и будем считать λz. id z нормальной формой:

	id (id (λz. id z))
→	id (λz. id z)
→	λz. id z
¬→

•  
  Варианты вызова по имени использовались в некоторых хорошо известных языках, в том числе в Алголе-60 (Naur et al., 1963) и Haskell (Hudak et al., 1992). В Haskell, на самом деле, используется оптимизированная версия, известная как вызов по необходимости (call by need) (Wadsworth, 1971; Ariola et al., 1995), в которой вместо того, чтобы перевычислять аргумент при каждом использовании, при первом вычислении все вхождения аргумента заменяются значением, и таким образом пропадает необходимость вычислять его заново в следующий раз. При такой стратегии требуется во время выполнения совместно использовать структуры данных между представлениями термов — в сущности, получается отношение редукции на графах (graphs) абстрактного синтаксиса, а не на синтаксических деревьях.
• В большинстве языков используется стратегия вызова по значению (call by value). В соответствии с ней, сокращаются только самые внешние редексы, и, кроме того, редекс срабатывает только в том случае, если его правая часть уже сведена к значению (value) — замкнутому терму, который уже вычислен и не может быть редуцирован далее.⁵ При такой стратегии наш пример будет редуцироваться так:

	id (id (λz. id z))
→	id (λz. id z)
→	λz. id z
¬→

•  
  Стратегия вызова по значению строга в том смысле, что аргументы функции всегда вычисляются, независимо от того, используются они в теле функции или нет. С другой стороны, нестрогие(non-strict) (или ленивые, lazy) стратегии вычисления — вызов по имени или по необходимости, — вычисляют только те аргументы, которые действительно используются.

Выбор стратегии вычисления почти ни на что не влияет в контексте обсуждения систем типов. Вопросы, которые ведут  к использованию тех или иных свойств типов, и методы, используемые для ответа на эти вопросы, для  всех стратегий практически одинаковы. В этой книге мы используем вызов  по значению: во-первых, потому что именно так работает большинство широко известных языков; и, во-вторых, потому что при этом легче всего ввести такие механизмы, как исключения (глава 14) и ссылки (глава 13).

5.2  Программирование на языке лямбда-исчисления

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