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

Рекурсия

Вспомним, что терм, который не может продвинуться дальше согласно отношению вычисления, называется нормальной формой (normal form). Любопытно, что некоторые термы не могут быть вычислены до нормальной формы. Например, расходящийся комбинатор (divergent combinator)

  omega = (λx. x x) (λx. x x);

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

Комбинатор omega можно обобщить до полезного терма, который называется комбинатором неподвижной точки (fixed-point combinator),⁶ с помощью которого можно определять рекурсивные функции, например, factorial.⁷

  fix = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y));

Как и omega, комбинатор fix имеет сложную структуру с повторами; глядя на определение, трудно понять, как он работает. Вероятно, получить интуитивное представление о его поведении удобнее всего, рассмотрев его действие на конкретном примере.⁸ Допустим, мы хотим написать рекурсивное определение функции вида h = ⟨тело, содержащее h⟩ — т. е., построить такое определение, в котором правая часть использует саму функцию, которую мы определяем (например, как в определении факториала на с. ??). Идея состоит в том, чтобы рекурсивное определение <<разворачивалось>> там, где оно встретится. Например, факториалу интуитивно соответствует определение:

  if n=0 then 1

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

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

                          else (n-2) * …))

или, в терминах чисел Чёрча,

  if realeq n c₀ then c₁

  else times n (if realeq (prd n) c₀ then c₁

                else times (prd n)

                           (if realeq (prd (prd n)) c₀ then c₁

                            else times (prd (prd n)) …))

Такого  эффекта можно добиться при помощи комбинатора fix, сначала определив g = ⟨тело, содержащее f⟩, а затем h = fix g. Например, функцию факториала можно определить через

  g = λfct. λn. if realeq n c₀ then c₁ else (times n (fct (prd n)));

  factorial = fix g;

На рис. 5.2 показано, что происходит при вычислении с термом factorial c₃. Ключевое свойство, которое обеспечивает работу этого вычисления, — это fct n →^* g fct n. Таким образом, fct — своего рода <<самовоспроизводящийся автомат>>, который, будучи применен к аргументу n, передает самого себя и n в качестве аргументов g. Там, где первый аргумент встречается в теле g, мы получим еще одну копию fct, которая, будучи применена к аргументу, опять передаст самое себя и аргумент внутрь g, и т. д. При каждом рекурсивном вызове с помощью fct мы разворачиваем очередную копию g и снабжаем ее очередными копиями fct, готовыми развернуться еще дальше.

 

	factorial c3
=	fix g c3
→	h h c3
	где h = λx. g (λy. x x y)
→	g fct c3
	где fct = λy. h h y
→	(λn. if realeq n c0
	then c1
	else times n (fct (prd n)))
	c3
→	if realeq c3 c0
	then c1
	else times c3 (fct (prd c3)))
→*	times c3 (fct (prd c3))
→*	times c3 (fct c′2)
	где c′2 поведенчески эквивалентен c2
→*	times c3 (g fct c′2)
→*	times c3 (times c′2 (g fct c′1))
	где c′1 поведенчески эквивалентен c1
	(те же шаги повторяются для g fct c′2)
→*	times c3 (times c′2 (times c′1 (g fct c′0)))
	где c′0 поведенчески эквивалентен c0
	(аналогично)
→*	times c3 (times c′2 (times c′1 (if realeq c′0 c0 then c1
	else …)))
→*	times c3 (times c′2 (times c′1 c1))
→*	c′6
	где c′6 поведенчески эквивалентен c6

Figure 5.2: Вычисление factorial c3

 

Упражнение 9   [★]: Почему в определении g мы использовали элементарную форму if, а не функцию test, работающую с Чёрчевыми булевскими значениями? Покажите, как определить функциюfactorial при помощи test вместо if.

Упражнение 10   [★★]: Напишите функцию churchnat, переводящую элементарное натуральное число в представление Чёрча.

Упражнение 11   [Рекомендуется,★★]: При помощи fix и кодирования списков из упражнения 8 напишите функцию, суммирующую список, состоящий из чисел Чёрча.

Представление

Прежде  чем закончить рассмотрение примеров и заняться формальным определением лямбда-исчисления, следует задаться еще одним, последним вопросом: что, строго говоря, означает утверждение, что числа Чёрча представляют обыкновенные числа?

Чтобы ответить на этот вопрос, вспомним, что  такое обыкновенные числа. Существует много (эквивалентных) определений; в  этой книге мы выбрали такое (рис. 3.2):

• константа 0,
• операция iszero, отображающая числа на булевские значения, и
• две операции, succ и pred, отображающие числа на числа.

Поведение арифметических операций определяется правилами вычисления из рис. 3.2. Эти правила говорят нам, например, что 3 следует за 2, и что iszero 0 истинно.

Кодирование по Чёрчу представляет каждый из этих элементов в виде лямбда-терма (то есть, функции):

• Терм c₀ представляет число 0.

Как мы видели на с. ??, имеются также <<неканонические представления>> чисел в виде термов. Например, терм λs. λz. (λx. x) z, который поведенчески эквивалентен c₀, также представляет число 0.

• Термы scc и prd представляют арифметические операции succ и pred, в том смысле, что, если t является представлением числа n, то scc t дает при вычислении представление числа n + 1, аprd t дает представление n - 1 (или 0, если n равно 0).
• Терм iszro представляет операцию iszero, в том смысле, что, если t является представлением 0, то iszro t дает при вычислении true,⁹ а если t представляет ненулевое число, то iszro tдает false.

Учитывая  всё вышеизложенное, представим, что  у нас есть программа, которая  проделывает некоторые сложные  численные вычисления и выдает булевский  результат. Если мы заменим все числа  и арифметические операции лямбда-термами, которые их представляют, и запустим получившуюся программу, мы получим тот же самый результат. Таким образом, с точки зрения окончательного результата программ, нет никакой разницы между настоящими числами и их представлениями по Чёрчу.

5.3  Формальности

В оставшейся части главы мы даем точное определение синтаксиса и операционной семантики лямбда-исчисления. По большей  части, всё устроено так же, как  в главе 3 (чтобы не повторять всё заново, мы здесь определяем только чистое лямбда-исчисление, без булевских значений и чисел). Однако операция подстановки терма вместо переменной связана с неожиданными сложностями.

Синтаксис

Как и в главе 3, абстрактную грамматику, определяющую термы (на с. ??) следует рассматривать как сокращенную запись индуктивно определенного множества абстрактных синтаксических деревьев.

Определение 1   [Термы]: Пусть имеется счетное множество имен переменных V. Множество термов — это наименьшее множество T такое, что

1. x ∈ T для всех x ∈ V;
2. Если t₁ ∈ T и x ∈ V, то λx.t₁ ∈ T;
3. Если t₁ ∈ T и t₂ ∈ T, то t₁ t₂ ∈ T.

Размер (size) терма t можно определить точно так же, как мы это сделали для арифметических выражений в определении 2. Интереснее тот факт, что можно дать простое индуктивное определение множества свободных переменных, встречающихся в терме.

Определение 2   Множество свободных переменных (free variables) терма t записывается как FV(t) и определяется так:

FV(x) = {x} FV(λx. t1) = FV(t1) \ {x} FV(t1 t2) = FV(t1) ⋃ FV(t2)

Упражнение 3   [★★]: Постройте строгое доказательство утверждения: |FV(t)| ≤ size(t) для любого терма t.

Подстановка

Операция  подстановки при подробном рассмотрении оказывается довольно непростой. В  этой книге мы будем использовать два разных определения, каждое из которых  удобно для своих целей. В этом разделе мы введем первое из них, краткое  и интуитивно понятное. Оно хорошо работает в примерах, в математических определениях и доказательствах. Второе, рассматриваемое в главе 6, использует более сложную нотацию и зависит от альтернативного <<представления де Брауна>> для термов, где именованные переменные заменяются на числовые индексы. Это представление оказывается более удобным для конкретных реализаций на ML, которые обсуждаются в последующих главах.

Поучительно прийти к определению подстановки, сделав пару неудачных попыток. Проверим сначала самое наивное рекурсивное  определение. (С формальной точки  зрения, мы определяем функцию [x ↦ s] индукцией по аргументу t.):

[x ↦ s]x	=	s
[x ↦ s]y	=	y	если x ≠ y
[x ↦ s](λy. t1)	=	λy. [x ↦ s]t1
[x ↦ s](t1 t2)	=	([x ↦ s]t1) ([x ↦ s]t2)

 

Такое определение в большинстве случаев  работает правильно. Например, оно дает

[x ↦ (λz. z w)](λy. x) = λy. λz. z w

что соответствует нашему интуитивному представлению о том, как должна себя вести подстановка. Однако при  неудачном выборе имен связанных  переменных это определение не работает. Например:

[x ↦ y](λx.x) = λx.y

Это противоречит базовой интуитивной  идее функциональной абстракции: имена связанных переменных не должны ни на что влиять — функция тождества остается самой собой, будь она записана в виде λx.x, λy.y или λfranz.franz. Если эти термы ведут себя по-разному при подстановке, они поведут себя по-разному и при редукции, а это явно неправильно.

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

[x ↦ s]x	=	s
[x ↦ s]y	=	y	если y ≠ x
[x ↦ s](λy. t1)	=	{ λy. t1  λy. [x ↦ s]t1	если y = x если y ≠ x
[x ↦ s](t1 t2)	=	([x ↦ s]t1)   ([x ↦ s]t2)

 

Это уже лучше, но все-таки еще не вполне правильно. Посмотрим, например, что  получается, когда мы пытаемся подставить терм z вместо переменной x в терме λz.x:

[x ↦ z](λz.x) = λz. z

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

Ситуация, в которой свободные переменные терма s становятся связанными при их наивной подстановке в терм t, называется захватом переменных (variable capture). Чтобы избежать его, нужно убедиться в том, что имена связанных переменных в t отличаются от имен свободных переменных в s. Операция подстановки, которая работает именно так, называется подстановкой, свободной от захвата (capture-avoiding substitution). (Обычно, когда просто говорят <<подстановка>>, именно такую подстановку и имеют в виду.) Мы можем добиться требуемого эффекта, если добавим ко второму варианту еще одно условие при подстановке в терм-абстракцию:

[x ↦ s]x	=	s
[x ↦ s]y	=	y	если y ≠ x
[x ↦ s](λy. t1)	=	{ λy. t1  λy. [x ↦ s]t1	если y = x если y ≠ x и y ∉ FV(s)
[x ↦ s](t1 t2)	=	([x ↦ s]t1)   ([x ↦ s]t2)

 

Теперь  почти все правильно: наше определение  подстановки делает то, что требуется, когда оно вообще что-то делает. Проблема заключается в том, что последнее изменение превратило подстановку из полной функции в частичную. Например, новое определение не выдает никакого результата для [x ↦ y z](λy. x y): связанная переменная y терма, в который производится подстановка, не равна x, но она встречается как свободная в терме (y z), и ни одна строка определения к ней не применима.

Распространенное  решение этой проблемы в литературе по системам типов и лямбда-исчислению состоит в том, что термы рассматриваются <<с точностью до переименования переменных>>. (Чёрч называл операцию последовательного переименования переменных в терме альфа-конверсией (alpha-conversion). Этот термин употребляется и до сих пор — мы могли бы сказать, что рассматриваем термы <<с точностью до альфа-конверсии>>.)

Соглашение 4   Термы, отличающиеся только именами связанных переменных, взаимозаменимы во всех контекстах.

На  практике это означает, что имя  любой λ-связанной переменной можно заменить на другое (последовательно проведя это переименование в теле λ) всегда, когда это оказывается удобным. Например, если мы хотим вычислить [x ↦ y z](λy. x y), мы сначала переписываем (λy. x y) в виде, скажем, (λw. x w). Затем мы вычисляем [x ↦ y z](λw. x w), что дает нам (λw. y z w).

Это соглашение делает наше определение <<практически  полным>>, поскольку каждый раз, как  мы пытаемся его применить к аргументам, к которым оно неприменимо, мы можем исправить дело переименованием, так, чтобы все условия выполнялись. В сущности, приняв это соглашение, мы можем сформулировать определение  подстановки чуть короче. Мы можем  отбросить первый вариант в определении  для абстракций, поскольку всегда можно предположить (применяя, если надо, переименование), что связанная  переменная y отличается как от x, так и от свободных переменных s. Определение принимает окончательный вид.