Функции

Вспомним функции в школьной математике. Они определялись следующим образом:

\[f(x) = 3x - 2\]

Чтобы вычислить значение функции при конкретном \(x\), значение подставлялось в определение функции, после чего вычислялся результат:

\[\begin{split}\begin{aligned} f(1) &= 3 - 2 = 1 \\ f(5) &= 15 - 2 = 13 \end{aligned}\end{split}\]

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

Сначала нам необходимо отделить процесс вычисления от равенства значений. Пусть \({\color{red}u}\) и \({\color{red}v}\) это термы. Запись \({\color{red}u} \longrightarrow {\color{red}v}\) означает, что результатом применения шага вычисления к терму \({\color{red}u}\) является терм \({\color{red}v}\). Запись \({\color{red}u} \xrightarrow{\;*\;} {\color{red}v}\) же означает, что результатом применения произвольного количества шагов вычисления (включая нуль, поэтому \({\color{red}u} \xrightarrow{\;*\;} {\color{red}u}\)) к терму \({\color{red}u}\) является терм \({\color{red}v}\).

Теперь введём понятие вычислимой функции. Под вычислимой функцией мы понимаем сущность, которая, будучи применена к некоторому набору значений, вычисляется в некоторое выражение.

Правило \({\color{red}f}({\color{red}x_1}, \dots, {\color{red}x_n}) := {\color{red}e}\) определяет вычислимую функцию, которая вычисляется точно так же, как и привычные нам функции — подстановкой значений на места переменных \({\color{red}x_1}, \dots, {\color{red}x_n}\) в \({\color{red}e}\). Знак \(:=\) подчёркивает, что это правило является определением, а не произвольным равенством.

Вычислимую функцию можно также задать правилом следующего вида:

\[\begin{split}f(x) := \begin{cases} {\color{red}e_1}, &\text{если}\ {\color{red}c_1} \\ {\color{red}e_2}, &\text{если}\ {\color{red}c_2} \\ \dots \\ \end{cases}\end{split}\]

В таком случае, функция вычисляется в выражение \(\color{red}e_i\) в том случае, если высказывание \(\color{red}c_i\) истинно для вычисленных значений аргументов функции.

Вычисление сложного выражения сводится к вычислению его частей. Мы не будем фиксировать порядок вычисления: мы считаем, что терм \(\color{red}u\) вычисляется в терм \(\color{red}v\) в том случае, когда \(\color{red}v\) может быть получено из \(\color{red}u\) вычислением любой его части. Арифметические операции вычисляются как обычно.

Приведём теперь пример нетривиальной вычислимой функции, решив следующую задачу. Пусть \(a\) и \(b\) это два положительных целых числа. Найдём наибольший общий делитель этих двух чисел, то есть наибольшее такое число \(d\), что и \(a\), и \(b\) делятся на \(d\) без остатка.

Если если числа \(a\) и \(b\) равны, то тогда, очевидно, они и являются наибольшим общим делителем. В противном случае одно из чисел больше, пусть это будет \(a\). Любое число \(d\), что делит числа \(a\) и \(b\), также делит и их разность \(a - b\) (действительно, если для некоторых \(n\) и \(k\) верно \(a = n d\) и \(b = k d\), то тогда \(a - b = n d = k d = (n - k) d\) делится на \(d\)). Поэтому наибольший общий делитель \(a\) и \(b\) является также и наибольшим общим делителем чисел \(a\) и \(a - b\).

Пользуясь этим рассуждением, определим следующую функцию:

\[\begin{split}НОД(a, b) := \begin{cases} a, &\text{если}\ a = b \\ НОД(b, a - b), &\text{если}\ a > b \\ НОД(a, b - a), &\text{если}\ a < b \\ \end{cases}\end{split}\]

Это функция представляет собой алгоритм Евклида, один из древнейших алгоритмов известных человечеству.

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

Посмотрим теперь как вычисляется функция \(НОД\), вычислив \(НОД(18, 30)\):

\[\begin{split}\begin{aligned} НОД(18, 30) &\xrightarrow{} НОД(18, 30 - 18) \\ &\xrightarrow{\;*\;} НОД(18, 12) \\ &\xrightarrow{\;*\;} НОД(12, 6) \\ &\xrightarrow{\;*\;} НОД(6, 6) \\ &\xrightarrow{\;*\;} 6 \end{aligned}\end{split}\]

Функция \(НОД\) применяется к паре положительных целых чисел. Но мы можем также определять функции, которые применяются к другим функциям.

Рассмотрим суммы следующего вида:

\[\sum_{n\leqslant i < k} f(i) = f(n) + \dots + f(k - 1)\]

Мы можем определить функцию \(sum\), которая вычисляет такие суммы:

\[\begin{split}sum(n, k, f) := \begin{cases} 0, &n ≥ k \\ sum(n, k - 1, f) + f(k-1), &n<k \end{cases}\end{split}\]

Рассмотрим вычисление этой функции на примере. Определим функцию \(sq(x) = x \cdot x\). Тогда выражение \(sum(1,4,sq)\) вычисляется следующим образом:

\[\begin{split}\begin{aligned} sum(1,4, sq) &\xrightarrow{} sum(1, 4-1, sq) + sq(4-1) \\ &\xrightarrow{\;*\;} sum(1,2,sq) + sq(2) + sq(3) \\ &\xrightarrow{\;*\;} sum(1,1,sq) + sq(1) + sq(2) + sq(3) \\ &\xrightarrow{\;*\;} 0 + sq(1) + sq(2) + sq(3) \\ &\xrightarrow{\;*\;} 1\cdot 1 + 2\cdot 2 + 3\cdot 3 \\ &\xrightarrow{\;*\;} 14 \end{aligned}\end{split}\]

Хотя функция может быть применена к другой функции, введённые нами правила не предоставляют возможности построить новую функцию в качестве результата. Причиной этому является то, что определение функции не является выражением, и оно вводит новое имя, которое должно отличаться от имён других функций. Но что если бы функция могла бы быть безымянным выражением?

Будем называть безымянной функцией выражение \(\lambda {\color{red}x}.\; {\color{red}e}\), которое, будучи применено к значению, вычисляется точно так же, как вычислялось бы применение функции \(f({\color{red}x}) := {\color{red}e}\).

Например, выражение \(λx.\; x\cdot x\) соответствует функции \(sq\), что мы рассматривали выше, и вычисляется точно так же:

\[(λn.\; n\cdot n)(3) \xrightarrow{} 3\cdot 3 \xrightarrow{\;*\;} 9\]

Безымянные функции позволяет свести функции нескольких переменных к функциям одного переменного. Например, пусть \(f\) — функция двух переменных. Тогда выражение \(λx.\; λy.\; f(x, y)\) представляет собой функцию одного переменного, результатом которой является другая функция одного переменного. Чтобы вычислить значение \(f(a, b)\) для некоторых \(a\) и \(b\), достаточно применить выражение \(λx.\; λy.\; f(x, y)\) к \(a\), а затем применить полученный результат к \(b\):

\[(λx.\; λy.\; f(x,y))(a)(b) \xrightarrow{\;*\;} (λy.\; f(a,y))(b) \xrightarrow{\;*\;} f(a, b)\]

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

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

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

Но сначала нам необходимо ввести формальное исчисление безымянных функций: лямбда-исчисление.

Синтаксис выражений лямбда-исчисления описывается следующей грамматикой:

\[\begin{split}\begin{array}{rcll} {\color{red}expr} & ::= & {\color{red}var} & \text{(имя переменной)} \\ & | & {\lambda\, \color{red}{var}}\,.\; {\color{red}expr} & \text{(абстракция)} \\ & | & {\color{red}expr\ expr} & \text{(применение)} \end{array}\end{split}\]

Имя переменной может быть словом. Кроме того, мы различаем строчные и заглавные буквы, считая, к примеру, \(ab\) и \(aB\) двумя различными именами1.

Применение левоассоциативно: \({\color{red}f}\ {\color{red}x}\ {\color{red}y}\) означает \(({\color{red}f}\ {\color{red}x})\ {\color{red}y}\). Абстракция же захватывает всё, что справа неё, то есть, к примеру, \(λx.\; x\ y\) означает \(λx.\; (x\ y)\), а не \((λx.\; x)\ y\).

Терм \(λ{\color{red}x}.\; λ{\color{red}y}.\; {\color{red}e}\) мы также сокращённо записываем как \(λ{\color{red}x}\,{\color{red}y}.\; {\color{red}e}\) и аналогично для большего количества вложенных абстракций.

Символ \(λ\) читается как «лямбда». Выражение \(f\ x\ y\) же произносится как «эф от икс от игрек» или же просто как «эф икс игрек».

Перейдём от синтаксиса к правилам вычисления. Здесь возникает трудность, связанная с именами переменных. Предназначение переменных — указывать места, куда подставляется значение при применении функции. Однако, совпадающие имена переменных делают это соответствие неоднозначным.

Например, рассмотрим терм \(λx.\; λx.\; x\). Применение какой именно функции приводит к подстановке терма на место переменной \(x\)?

Есть две возможности. Мы можем связать \(x\) с внешней абстракцией, тем самым подставляя значение внутрь терма \(λx.\; x\):

Или же мы можем связать \(x\) с внутренней абстракцией, тем самым всегда вычисляя \(λx.\;x\) при применении внешней абстракции:

Наиболее разумным представляется второй вариант, так как в таком случае смысл выражения \(λx.\;x\) не зависит от того, частью какого выражения оно является. Однако, одного лишь разрешения неоднозначности в пользу того или иного варианта недостаточно, так как неоднозначность возникают в процессе вычисления выражений.

Например, пусть \((λf.\; λz.\; f\ z)\ z\) является подвыражением некоторого другого выражения. Если мы свяжем переменные с ближайшими с ними абстракциями, то одна из \(z\) относится к абстракции \(λz.\; f\ z\), когда же другая \(z\) относится к некоторой внешней абстракции. Однако если мы наивно вычислим это выражение, то получим терм \(λz.\; z\ z\), в котором, согласно выбранному способу разрешения неоднозначностей, обе \(z\) относятся к абстракции \(λz.\; z\ z\).

Это заведомо неверная интерпретация, так как то же выражение но с другими именами даёт иной результат:

\[(λf.\; λt.\; f\ t)\ z \longrightarrow λt.\; z\ t\]

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

Начнём с классификации вхождений переменных в выражение. Вхождение терма в другой терм это терм в конкретном месте синтаксического дерева.

Вхождение переменной при абстракции, то есть \(\color{red}x\) в \(λ{\color{red}x}.\; {\color{red}e}\), называется связывающим. Переменные не при абстракции мы называем отдельными, они могут входить в выражение либо связанно, либо свободно.

Вхождение переменной \(\color{red}x\) в терм \(\color{red}t\) называется связанным, если оно связано с одной из абстракций в \(\color{red}t\). То есть, в \(\color{red}t\) входит терм \(λ{\color{red}x}.\; {\color{red}u}\), такой, что \(\color{red}x\) входит в \(\color{red}u\) и это вхождение не является частью иного терма \(λ{\color{red}x}.\; {\color{red}v}\), входящего в \(\color{red}u\).

Вхождение переменной, не являющееся ни связывающим, ни связанным, называется свободным.

В качестве примера, рассмотрим вхождения переменных в терм \(λx.\; λy.\; f\ y\ x\):

В это выражение переменные \(x\) и \(y\) входят связанно. Красные стрелки показывают связи между связывающими переменными и соответствующими им связанными переменными. Синяя стрелка же указывает на переменную \(f\), которая входит в выражение свободно.

Вхождения переменных зависят от рассматриваемого выражения: так, \(x\) входит в \(λx.\; λy.\; f\ y\ x\) связанно, но при этом входит свободно в выражение \(λy.\; f\ y\ x\).

Имена связанных переменных не влияют на смысл выражения, так как вычисление не зависит от конкретных имён. Например, функции \(λx.\;λy. y\) и \(λa.\; λb.\; b\) при применении вычисляются совершенно одинаково. Раскроем эту мысль подробнее.

Переименование переменной при абстракции \(λ{\color{red}x}.\; {\color{red}e}\) это замена связывающей переменной и всех связываемых ею переменных на переменные с новым именем. При этом новая переменная не должна входить свободно в \(λ{\color{red}x}.\; {\color{red}e}\) (но при этом может совпадать с \(\color{red}x\), то есть оставить выражение как есть считается за тривиальное переименование).

Например, результатом переименования переменной при внешней абстракции в выражении \(λx.\; λx.\; x\) может быть выражение \(λy.\; λx.\; x\), когда же результатом переименования при внутренней абстракции будет \(λx.\; λy.\; y\).

Два терма называются альфа-эквивалентными, если один из них можно преобразовать в другой переименованием переменных. К примеру, выражение \(λx.\;λx.\; y\) альфа-эквивалентно выражению \(λa.\; λb.\; b\).

Поскольку смысл выражений не зависит от имён связанных переменных, мы будем считать альфа-эквивалентные выражения фактически одним выражением.

Переименование переменных позволяет предотвратить неоднозначности, возникающие в процессе вычисления выражений. Достаточно, чтобы подстановка переименовывала те связывающие переменные, которые могли бы захватить свободные переменные в подставляемом выражении.

Метавыражение \({\color{red}e}[{\color{red}x} := {\color{red}v}]\) означает терм \(\color{red}e\), в котором без захвата переменных во все свободные вхождения переменной \(\color{red}x\) подставляется терм \(\color{red}v\).

Подстановка осуществяется следующим образом:

• Если \(\color{red}e\) представляет собой применение \({\color{red}e_1}\ {\color{red}e_2}\), то тогда результатом подстановки является терм \({\color{red}e_1}[{\color{red}x} := {\color{red}v}]\ {\color{red}e_2}[{\color{red}x} := {\color{red}v}]\)

• Если \(\color{red}e\) представляет собой абстракцию \(λ{\color{red}y}.\; {\color{red}e_y}\), то тогда переменная при абстракции переименовывается таким образом, что новая переменная не входит свободно в \({\color{red}v}\). Пусть результатом такого переименования является выражение \(λ{\color{red}z}.\; {\color{red}e_z}\), тогда результатом подстановки является выражение \(λ{\color{red}z}.\; {\color{red}e_z}[{\color{red}x} := {\color{red}v}]\)

• Если же \(\color{red}e\) представляет собой переменную \(\color{red}y\), то тогда результатом является выражение \(\color{red}v\), если имя \(\color{red}y\) совпадает с \(\color{red}x\), или же выражение \(\color{red}y\), если не совпадает

В качестве примера подстановки, найдём \((λz.\; f\ z)[f := z]\):

• \((λz.\; f\ z)[f := z]\)

• \(λt.\; (f\ t)[f := z]\)

• \(λt.\; f[f := z]\ t[f := z]\)

• \(λt.\; z\ t\)

Определив подстановку, мы можем, наконец, определить и правило вычисления выражений.

Правило вычисления лямбда-выражений (бета-редукция):

\[(λ\textcolor{red}x.\;\textcolor{red}e)\ \textcolor{red}v \longrightarrow {\textcolor{red}e}[{\textcolor{red}x := {\textcolor{red}v}}]\]

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

Поскольку мы не оговариваем какой именно редекс заменяется при шаге вычисления, мы можем рассматривать множество путей вычисления одного и того же выражения. Например, выражение \((λx\,y.\; x)\ ((λx.\;x)\ z)\) можно вычислять следующими путями (подчёркиванием выделены редуцируемые редексы):

\[\begin{split}\begin{aligned} \underline{(λx\,y.\; x)\ ((λx.\;x)\ z)} &⟶ λy.\; (\underline{(λx.\;x)\ z}) &⟶ λy.\;z \\ (λx\,y.\; x)\ (\underline{(λx.\;x)\ z}) &⟶ \underline{(λx\,y.\; x)\ z} &⟶ λy.\;z \end{aligned}\end{split}\]

Несмотря на то, что выражения можно вычислять по разному, два различных результата вычисления одного и того же выражения можно дальнейшим вычислением свести к одному и тому же выражению.

Теорема (Чёрч — Россер): пусть \(\color{red}e\), \(\color{red}a\) и \(\color{red}b\) это такие выражения, что \({\color{red}e} \xrightarrow{\;*\;} {\color{red}a}\) и \({\color{red}e} \xrightarrow{\;*\;} {\color{red}b}\). Тогда существует такое выражение \(\color{red}w\), что \({\color{red}a} \xrightarrow{\;*\;} {\color{red}w}\) и \({\color{red}b} \xrightarrow{\;*\;} {\color{red}w}\).

Наглядно утверждение этой теоремы можно изобразить следующим образом:

Теорема Чёрча — Россера это важнейшая теорема лямбда-исчисления. Но доказывать мы ещё не будем3.

Важное замечание: теорема Чёрча — Россера говорит о возможности, но не о необходимости. У некоторых выражений два пути вычисления могут так никогда и не сойтись. Например:

\[\begin{split}\begin{aligned} (λx\,y.\; y)\ (\underline{(λx.\;x\ x)\ (λx.\;x\ x)}) &⟶ (λx\,y.\; y)\ (\underline{(λx.\;x\ x)\ (λx.\;x\ x)}) &⟶ \dots \\ \underline{ (λx\,y.\; y)\ ((λx.\;x\ x)\ (λx.\;x\ x))} &⟶ λy.\;y \end{aligned}\end{split}\]

Так как выражение \((λx.\;x\ x)\ (λx.\;x\ x)\) вычисляется само в себя, всё выражение целиком можно вычислять неограниченно, так и не достигая терма \(λy.\;y\).

Перейдём от вычисления к равенству. Естественное равенством двух выражений это равенство результатов их вычисления.

Определение: выражение \(\color{red}a\) называется вычислительно равным выражению \(\color{red}a\) (пишется \({\color{red}a} \equiv {\color{red}b}\)), если существует такое выражение \(\color{red}w\), что \({\color{red}a} \xrightarrow{\;*\;} {\color{red}w}\) и \({\color{red}b} \xrightarrow{\;*\;} {\color{red}w}\).

Вычислительное равенство удовлетворяет всем необходимым свойствам равенства:

• Рефлексивность: \({\color{red}a} \equiv {\color{red}a}\) для любого \(\color{red}a\)

• Симметричность: если \({\color{red}a} \equiv {\color{red}b}\), то \({\color{red}b} \equiv {\color{red}a}\)

• Транзитивность: если \({\color{red}a} \equiv {\color{red}b}\) и \({\color{red}b} \equiv {\color{red}c}\), то и \({\color{red}a} \equiv {\color{red}c}\)

Транзитивность вычислительного равенства следует из теоремы Чёрча — Россера:

1. Пусть \(\color{red}ab\) это такое выражение, что \({\color{red}a} \xrightarrow{\;*\;} {\color{red}ab}\) и \({\color{red}b} \xrightarrow{\;*\;} {\color{red}ab}\)

2. Пусть \(\color{red}bc\) это такое выражение, что \({\color{red}b} \xrightarrow{\;*\;} {\color{red}bc}\) и \({\color{red}c} \xrightarrow{\;*\;} {\color{red}bc}\)

3. Согласно теореме Чёрча — Россер, существует такое выражение \(\color{red}abc\), что \({\color{red}ab} \xrightarrow{\;*\;} {\color{red}abc}\) и \({\color{red}bc} \xrightarrow{\;*\;} {\color{red}abc}\)

4. Но для такого выражения также верно \({\color{red}a} \xrightarrow{\;*\;} {\color{red}abc}\) и \({\color{red}c} \xrightarrow{\;*\;} {\color{red}abc}\)

5. Что означает, что \({\color{red}a} \equiv {\color{red}c}\)

Наглядно это рассуждение можно изобразить следующей диаграммой:

Мы полностью описали лямбда-исчисление. Теперь же посмотрим, как можно построить мир из одних только безымянных функций.

Мир безымянных функций

Рассматриваемый нами мир состоит из данных и действий над ними.

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

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

Рассмотрим следующее выражение:

\[f\ (h\ x)\]

Пусть результатом применения функции \(h\) являются всегда лишь ответы «да» и «нет», которые мы обозначим, соответственно, как \(yes\) и \(no\). Каким образом подобное значение может быть использованно?

Поскольку возможных значений всего два, результатов применений функции \(f\) к этим значениям тоже может быть не более, чем два. Пусть функция \(f\) вычисляется в значение \(a\), когда применена к значению \(no\), и в значение \(b\), когда применена к значению \(yes\):

\[f\ no \equiv a \qquad f\ yes \equiv b\]

Попробуем теперь найти какую-нибудь функцию \(f\), удовлетворяющую подобным вычислительным равенствам.

В лямбда-исчислении, значения \(no\), \(yes\), \(a\) и \(b\) являются функциями. Если функция \(f\) применяется к некоторому значению \(x\), то единственное что она может сделать это либо применить некоторую функцию к \(x\), либо применить \(x\) к некоторым значениям. Но поскольку \(a\) и \(b\) произвольны, применение любого из них в общем случае не ведёт к требуемому результату. Поэтому, имеет смысл применить \(x\) к значениям \(a\) и \(b\).

Предположим теперь, что \(f\ x \equiv x\ a\ b\). Тогда уже значения \(no\) и \(yes\) должны удовлетворять следующим равенствам:

\[no\ a\ b \equiv a\qquad yes\ a\ b \equiv b\]

Гипотетические рассуждения о неизвестных функциях выявили следующую возможность. Данные вида ответов «да» и «нет» можно представить в лямбда-исчислении следующим образом:

\[no := λx\, y.\; x\qquad yes := λx\, y. \; y\]

Эти значения используются иначе, чем использовались числа в определении \(НОД\), которое мы давали в самом начале: вместо того, чтобы действовать тем или иным способом в зависимости от того, чему равны значения, мы позволяем самому значению выбрать тот или иной результат в зависимости от того, чем оно является.

Схожим образом можно закодировать и натуральные числа. Каждое натуральное число можно рассматривать как овеществление процесса счёта:

• Натуральные числа начинаются с нуля4

• \(1\) это число, следующее за нулём

• \(2\) это число, следующее за \(1\)

• И так далее

Таким образом, любое натуральное число является либо нулём, либо числом, следующим за некоторым натуральным числом \(n\). Обозначим эти возможности, соответственно, как \(z\) и \(s\ n\).

Пусть некоторая функция \(f\) применяется к натуральному числу. Она может либо вычислиться в некоторое значение \(v\), если число является нулём, либо вычислиться в некоторое другое значение, если число следует за некоторым другим числом \(n\). Это другое значение, вообще говоря, зависит от \(n\). Предположим, что значение может быть вычисленно применением функции \(g\) к \(n\).

Таким образом имеем:

\[z\ v\ f \equiv v \qquad (s\ n)\ v\ f \equiv (f\ n)\]

Рассуждая как и в прошлый раз, мы можем вывести следующие определения \(z\) и \(s\):

\[\begin{split}\begin{aligned} z &:= λz\, s.\; z \\ s &:= λn.\; λz\, s.\; s\ n \end{aligned}\end{split}\]

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

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

Обозначим искомую функцию, складывающую два числа, как \(add\). Если \(n\) это некоторое натуральное число, то тогда \(add\ n\) это функция, которая, будучи применена к любому натуральному числу \(k\), вычисляется в сумму \(n\) и \(k\). Рассмотрим результат применения функции \(add\ n\) в зависимости от того, к какому натуральному числу она применяется.

Если \(add\ n\) применяется к нулю, то результатом будет число \(n\):

\[add\ n\ z \equiv n\]

Если же \(add\ n\) применяется к числу, следующему за некоторым числом \(k\), то тогда результатом вычисления будет число, следующее за суммой \(n\) и \(k\) (поскольку \(n + (k+1) = (n+k) + 1\)):

\[add\ n\ (s\ k) \equiv s\ (add\ n\ k)\]

Вспомним теперь, что если \(p\) это натуральное число в кодировании Скотт, то тогда для любых \(n\) и \(g\) выражение \(p\ n\ g\) вычисляется в \(n\), если \(p\) это нуль, или в \(g\ k\), если \(p\) это число, следующее за числом \(k\). Это позволяет соединить предыдущие два равенства в одно:

\[add\ n\ p \equiv p\ n\ (λk.\; s\ (add\ n\ k))\]

Отсюда мы можем положить:

\[add\ n \equiv λp.\; p\ n\ (λk.\; s\ (add\ n\ k))\]

Функция \(add\ n\) упоминается по обе стороны от равенства. Вынесем её наружу, введя абстракцию:

\[add\ n \equiv \big(λr.\; λp.\; p\ n\ (λk.\; s\ (r\ k))\big)\ (add\ n\ k)\]

Таким образом, функция \(add\ n\) вычислительно равна применению некоторой другой функции к себе.

На первый взгляд этот результат кажется бесполезным: он выражает функцию \(add\) через саму себя, при том, что в лямбда-исчислении нет прямого способа выразить рекурсию. Тем не менее, это равенство можно решить, решив другую, более общую задачу.

Пусть \(f\) это произвольная функция. Найдём функцию \(Y\), удовлетвояющую следующему равенству:

\[Y\ f \equiv f\ (Y\ f)\]

Эта задача кажется не менее трудной чем предыдущая, но на самом деле мы знаем всё, что требуется для её решения. Вспомним выражение, что вычислялось само в себя:

\[(λx.\;x\ x)\ (λx.\;x\ x) ⟶ (λx.\;x\ x)\ (λx.\;x\ x)\]

Достаточно лишь изменить это выражение так, чтобы оно применяло функцию \(f\) к результату:

\[(λx.\;f\ (x\ x))\ (λx.\;f\ (x\ x)) ⟶ f\ \big((λx.\;f\ (x\ x))\ (λx.\;f\ (x\ x))\big)\]

Отсюда мы немедлемо получаем требуемую функцю \(Y\):

\[Y\ f \equiv (λx.\;f\ (x\ x))\ (λx.\;f\ (x\ x))\]

Функция \(Y\) называется комбинатором неподвижной точки.

Вернёмся к определению сложения. Комбинатор неподвижной точки позволяет решить равенство с функцией \(add\ n\) следующим образом:

\[add\ n \equiv Y\ \big(λr.\; λp.\; p\ n\ (λk.\; s\ (r\ k))\big)\]

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

\[add := λn.\;Y\ \big(λr.\; λp.\; p\ n\ (λk.\; s\ (r\ k))\big)\]

Рассмотрим вычисление этой функции на примере. Вычислим \(add\ 3\ 2\):

\[\begin{split}\begin{aligned} add\ 3\ 2 &\equiv Y\ (add\ 3)\ 2 \\ &\equiv (add\ 3)\ (Y\ (add\ 3))\ 2 \\ &\equiv \big(λa\,k.\; k\ 3\ (λk.\; s\ (a\ k))\big)\ \big(Y\ (add\ 3)\big)\ 2 \\ &\equiv \big(λk.\; k\ 3\ (λk.\; s\ (Y\ (add\ 3)\ k))\big)\ 2 \\ &\equiv 2\ 3\ (λk.\; s\ (Y\ (add\ 3)\ k)) \\ &\equiv s\ (Y\ (add\ 3)\ 1) \\ &\equiv s\ (s\ (Y\ (add\ 3)\ 0)) \\ &\equiv 5 \end{aligned}\end{split}\]

С помощью комбинатора неподвижной точки можно определить не только сложение, но и любую другую рекурсивную функцию.

Упражнения

Несколько необязательных упражнений на программирование в лямбда-исчислении.

1. Для натуральных чисел, определить следующие функции:

   1. Предшествующее число: \(pred\ z \equiv z\) и \(pred\ (s\ n) \equiv n\)

   2. Усечённое вычитание: наибольшее из \(n - k\) и нуля

   3. Умножение чисел

   4. Неполное деление. Если делитель равен нулю, результатом может быть любое значение

   5. Сравнение: \(le\ n\ k \equiv yes\), если \(n ⩽ k\), иначе \(le\ n\ k \equiv no\)

2. Используя кодирование Скотт, выразить списки

   • Подсказка: список \([a,b,c]\) можно представить как \(cons\ a\ (cons\ b\ (cons\ c\ nil))\)

3. Для списков, определить следующие функции:

   1. Длину списка

   2. \(map\ f\), которая применяет \(f\) к каждому элементу списка

   3. Сумма всех натуральных чисел в списке

---

1

Подобное соглашение, как правило, не встречается в математических текстах, но обычно в программировании.

2

Aнгл. redex (reducible expression).

3

Заинтересованный читатель может найти доказательства этой теоремы в интернете по словам Church-Rosser theorem.

4

Как и всё остальное прогрессивное человечество, мы считаем нуль натуральным числом.

5

Оно отличается от кодирования Чёрча: в последнем \((s\ (s\ z))\ v\ f \equiv f\ (f\ v)\), когда же кодирование Скотт даёт \((s\ (s\ z))\ v\ f \equiv f\ (s\ z)\).