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

Функции с несколькими аргументами

Заметим для начала, что в лямбда-исчислении отсутствует встроенная поддержка  функций с несколькими аргументами. Разумеется, ее было бы нетрудно добавить, однако того же самого результата проще  достичь через функции высшего порядка (higher-order functions), которые возвращают функции в качестве результата. Допустим, у нас есть терм s с двумя свободными переменными x и y, и мы хотим написать такую функцию f, которая выдавала бы для каждой пары аргументов (v,w) результат подстановки v вместо x и w вместо y. Мы пишем не f = λ(x,y).s, как мы сделали бы это в более богатом языке, а f = λx.λy.s. Это означает, что f есть функция, которая, получив значение v для параметра x, выдает функцию, которая, получив значение w для параметра y, выдает нужный результат. После этого мы поочередно применяем f к аргументам, получая запись f v w (т. е., (f v) w), которая переходит в ((λy.[x ↦ v]s) w), и далее в [y ↦ w][x ↦ v]s. Такое преобразование функций с несколькими аргументами в функции высшего порядка называется каррированием (currying) в честь Хаскелла Карри, современника Чёрча.

Булевские константы Чёрча

Еще одна языковая конструкция, легко кодируемая в лямбда-исчислении — булевские значения и условные выражения. Определим термы tru и fls таким образом:

  tru = λt. λf. t;

  fls = λt. λf. f;

(Этим  термам даны сокращенные имена,  чтобы избежать их смешения с элементарными булевскими константами true и false из главы 3.)

Можно считать, что термы tru и fls представляют собой булевские значения <<истина>> и <<ложь>> в том смысле, что с их помощью мы можем выполнять операцию проверки булевского значения на истинность. А именно, мы можем определить комбинатор test, такой, что test b v w переходит в v, если b равно tru, и в w, если b равно fls.

  test = λl. λm. λn. l m n;

Комбинатор test почти ничего не делает: test b v w просто переходит в b v w. В сущности, булевские значения являются условными выражениеми: они принимают два аргумента и выбирает из них либо первый (если это tru), либо второй (если это fls). Например, терм test tru v w редуцируется таким образом:

	test tru v w
=	(λl. λm. λn. l m b) tru v w	по определению
→	(λm. λn. tru m b) v w	редукция подчеркнутого выражения
→	(λn. tru v b) w	редукция подчеркнутого выражения
→	tru v w	редукция подчеркнутого выражения
=	(λt. λf. t) v w	по определению
→	(λf. v) w	редукция подчеркнутого выражения
→	v	редукция подчеркнутого выражения

 
Несложно также определить в виде функций такие булевские операторы, как логическая конъюнкция:

  and = λb. λc. b c fls;

То  есть, and — это функция, которая, получив два булевских значения b и c, возвращает c, если b равно tru и fls, если b равно fls; таким образом, and b c выдает tru, если и b, и c равны tru, и fls, если либо b, либо c окажутся равными fls.

  and tru tru;

 

|> (λt. λf. t)

 

  and tru fls;

 

|> (λt. λf. f)

Упражнение 1   [★]: Определите логические функции or (<<или>>) и not (<<не>>).

Пары

При помощи булевских констант мы можем  закодировать пары значений в виде термов:

  pair = λf.λs.λb. b f s;

  fst = λp. p tru;

  snd = λp. p fls;

Это означает, что pair v w — функция, которая, будучи применена к булевскому значению b, применяет b к v и w. По определению булевских констант, при таком вызове получится v, если bравняется tru, и w, если b равняется fls, так что функции первой и второй проекции fst и snd можно получить, просто подав в пару соответствующие булевские значения. Вот как проверить, что fst (pair v w) →^* v:

	fst (pair v w)
=	fst ((λf.λs.λb. b f s) v w)	по определению
→	fst ((λs.λb. b v s) w)	редукция подчеркнутого выражения
→	fst (λb. b v w)	редукция подчеркнутого выражения
=	(λp. p tru) (λb. b v w)	по определению
→	(λb. b v w) tru	редукция подчеркнутого выражения
→	tru v w	редукция подчеркнутого выражения
→*	v	как показано ранее.

Числа Чёрча

После всего, что мы видели, представление  чисел в виде лямбда-термов будет лишь ненамного сложней. Числа Чёрча (Church numerals) c_o, c₁, c₂, и т. д. можно определить таким образом:

c₀ = λs. λz. z;

c₁ = λs. λz. s z;

c₂ = λs. λz. s (s z);

c₃ = λs. λz. s (s (s z));

и т. д. Здесь каждое число n представляется комбинатором c_n, который принимает два аргумента, s и z (<<функцию следования>> и <<ноль>>), и n раз применяет s к z. Как и в случае с булевскими константами и парами, такое кодирование превращает числа в активные сущности: число n представляется в виде функции, которая что-то делает n раз — своего рода активное число по основанию 1.

(Читатель  мог уже заметить, что c₀ и fls записываются одним и тем же термом. Такие <<каламбуры>> часто встречаются в языках ассемблера, где одна и та же комбинация битов может представлять собой множество разных значений — целое число, число с плавающей точкой, адрес, четыре символа и т. п., — в зависимости от того, как интерпретируются биты. Аналогичная ситуация в низкоуровневых языках вроде C, где 0 и false тоже представляются одинаково.)

Функцию следования на числах Чёрча можно  определить так:

  scc = λn. λs. λz. s (n s z);

Терм scc — это комбинатор, который принимает число Чёрча n и возвращает другое число Чёрча, — то есть, возвращает функцию, которая принимает аргументы s и z, и многократно применяет s кz. Нужное число применений s к z мы получаем, сначала передав s и z в качестве аргументов n, а затем явным образом применив s еще раз к результату.

Упражнение 2   [★★]: Найдите ещё один способ определения функции следования на числах Чёрча.

Похожим образом, сложение на числах Чёрча можно  осуществлять с помощью терма plus, который принимает в качестве аргументов два числа Чёрча, m и n, и возвращает еще одно число Чёрча — т. е., функцию, которая принимает аргументы s и z, применяет s к z n раз (передавая s и z в качестве аргументов n), а потом применяет s еще m раз к результату:

  plus = λm. λn. λs. λz. m s (n s z);

Для реализации умножения используется еще один трюк: поскольку plus принимает аргументы по одному, применение его к одному аргументу n дает функцию, которая добавляет n к любому данному ей аргументу. Можно передать эту функцию в качестве первого аргумента m, а в качестве второго дать c₀, и это будет означать <<применить функцию, добавляющую n к своему аргументу, к нулю и повторить m раз>>, т. е., <<сложить m копий числа n>>.

  times = λm. λn. m (plus n) c₀;

Упражнение 3   [★★]: Можно ли определить умножение на числах Чёрча без использования plus?

Упражнение 4   [Рекомендуется,★★]: Определите терм для возведения чисел в степень.

Чтобы проверить, является ли число Чёрча  нулем, нужно найти какую-то подходящую для этой цели пару аргументов, — а именно, нужно применить указанное число к паре термов zz и ss, таких чтобы применение ss к zz один или более раз давало fls, а отсутствие применения давало tru. Понятно, что в качестве zz нужно просто взять tru. Для ss же мы используем функцию, которая игнорирует свой аргумент и всегда возвращает fls:

  iszro = λm. m (λx. fls) tru;

 

  iszro c₁;

 

|> (λt. λf. f)

 

  iszro (times c₀ c₂);

 

|> (λt. λf. t)

Как ни странно, определить вычитание на числах Чёрча намного сложнее, чем  сложение. Для этого можно воспользоваться  следующей довольно хитрой <<функцией предшествования>>, которая возвращает c₀, если передать в качестве аргумента c₀, и возвращает c_i, если передать в качестве аргумента c_i+1,:

  zz = pair c₀ c₀;

  ss = λp. pair (snd p) (plus c₁ (snd  p));

  prd = λm. fst (m ss zz);

Это определение работает так: мы используем m в качестве функции и применяем с ее помощью m копий функции ss к начальному значению zz. Каждая копия ss принимает в качестве аргумента пару чисел pair c_i c_j и выдает в результате пару pair c_j c_j+1 (см. рис. 5.1). Таким образом, при m-кратном применении ss к pair c₀ c₀ получается pair c₀ c₀, если m = 0, и pair c_m-1 c_m при положительном m. В обоих случаях, в первом компоненте пары находится искомый предшественник.

 

@C=.2em @R=1.5ex **[r] pair @/_2em/[dd]_ss c₀c₀ [ddl]_копия [dd]^+1 
 
**[r] pair @/_2em/[dd]_ss c₀c₁ [ddl]_копия [dd]^+1 
 
**[r] pair @/_2em/[dd]_ss c₁c₂ [ddl]_копия [dd]^+1 
 
**[r] pair @/_2em/[dd]_ss c₂c₃ [ddl]_копия [dd]^+1 
 
**[r] pair c₃c₄ 
**[r] ⋮

Figure 5.1: <<Внутренний цикл>> функции предшествования.

 

Упражнение 5   [★★]: Определите функцию вычитания при помощи prd .

Упражнение 6   [★★]: Сколько примерно шагов вычисления (в зависимости от n) требуется, чтобы получить prd c_n?

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

  equal c₃ c₃

 

|> (λt. λf. t)

 

  equal c₃ c₂

 

|> (λt. λf. f)

Подобными же методами можно определить другие распространенные типы данных: списки, деревья, массивы, записи с вариантами, и т. п.

Упражнение 8   [Рекомендуется,★★★]: Список можно представить в лямбда-исчислении через его функцию свертки fold. (В OCaml эта функция называется fold_left; ее иногда еще называютreduce.) Например, список [x, y, z] становится функцией, которая принимает два аргумента c и n, и возвращает c x (c y (c z n)). Как будет выглядеть представление nil? Напишите функцию cons, которая принимает элемент h и список (то есть, функцию свертки) t, и возвращает подобное представление списка, полученного добавлением h в голову t. Напишите функции isnilи head, каждая из которых принимает список в качестве параметра. Наконец, напишите функцию tail для такого представления списков (это намного сложнее; придется использовать трюк, аналогичный тому, что использовался при определении prd для чисел).

Расширенное исчисление

Мы  убедились, что булевские значения, числа и операции над ними могут  быть закодированы средствами чистого  лямбда-исчисления. Строго говоря, все  нужные нам программы мы можем  писать, не выходя за рамки этой системы. Однако при работе с примерами  часто бывает удобно включить в нее  элементарные булевские значения и  числа (а может быть, и другие типы данных). Если нам нужно совершенно точно указать, с какой системой мы в данный момент работаем, то для  чистого лямбда-исчисления, определяемого  на рис. 5.3, мы будем использовать обозначение λ, а для системы, в которую добавлены булевские и арифметические выражения с рис. 3.1 и 3.2 — обозначение λNB.

В λNB по сути есть две разные реализации булевских значений и две реализации чисел: настоящие и закодированные методом, описанным в этой главе. Мы можем выбирать между ними при написании программ. Разумеется, эти две реализации нетрудно преобразовать друг в друга. Чтобы перевести булевское значение по Чёрчу в элементарное булевское значение, нужно применить его к значениям true и false:

  realbool = λb. b true false;

Для обратного преобразования используется условное выражение:

  churchbool = λb. if b then tru else fls;

Можно встроить эти преобразования в операции высшего порядка. Вот проверка на равенство для чисел Чёрча, возвращающая настоящее логическое значение:

  realeq = λm. λn. (equal m n) true false;

Аналогично  мы можем преобразовать число  Чёрча в соответствующее элементарное число, применив его к succ и 0:

  realnat = λm. m (λx. succ x) 0;

Мы  не можем напрямую применить m к succ, поскольку сама по себе запись succ не имеет синтаксического смысла: мы определили арифметические выражения так, что succ всегда должен к чему-то применяться. Это требование мы обходим, обернув succ в маленькую функцию, которая всегда возвращает succ от своего аргумента.

Причины, по которым элементарные булевские  и числовые значения оказываются  полезны при работе с примерами, в основном связаны с порядком вычислений. Рассмотрим, например, терм scc c₁. Исходя из приведенного выше обсуждения, мы могли бы ожидать, что он должен при вычислении давать число Чёрча c₂. На самом деле этого не происходит:

  scc c₁;

 

|> (λs. λz. s ((λs'. λz'. s' z') s z))

Этот  терм содержит в себе редекс, который  при вычислении привел бы нас (за два  шага) к c₂, однако согласно правилам вызова по значению мы ещё не можем сделать это, поскольку редекс находится внутри лямбда-абстракции.

Никакой фундаментальной проблемы здесь  нет: терм, получающийся при вычислении scc c₁, очевидным образом поведенчески эквивалентен (behaviorally equivalent) c₂, в том смысле, что применение этого терма к паре аргументов v и w всегда даст тот же результат, что и применение c₂ к тем же аргументам. Однако, необходимость доделать вычисление затрудняет проверку того, что наша функцияscc ведет себя как надо. В случае более сложных арифметических вычислений трудность еще возрастает. Например, times c₂ c₂ дает в результате не c₄, а такое чудовищное выражение:

  times c₂ c₂;

 

|> (λs.

     λz.

       (λs'. λz'. s' (s' z')) s

       ((λs'.

          λz'.

            (λs''. λz''. s'' (s'' z'')) s'

            ((λs''. λz''.z'') s' z'))

       s

       z))

Можно убедиться, что этот терм ведет себя так же, как c₄, с помощью проверки на равенство:

  equal c₄ (times c₂ c₂);

 

|> (λt. λf. t)

Однако  более прямой способ — взять times c₂ c₂ и преобразовать в элементарное число:

  realnat (times c₂ c₂);

 

|> 4

Функция преобразования передает выражению times c₂ c₂ два дополнительных аргумента, которых оно ожидает, и заставляет выполнить все задержанные вычисления в его теле.