# Функции

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

$$f(x) = 3x - 2$$

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

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

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

Сначала нам необходимо отделить процесс вычисления от равенства значений. Пусть ${\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}$. Знак $:=$ подчёркивает, что это правило является определением, а не произвольным равенством.

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

$$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}$$

В таком случае, функция вычисляется в выражение $\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$.

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

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

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

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

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

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

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

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

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

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

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

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

$$\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}$$

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

Будем называть *безымянной функцией* выражение $\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{array}{rcll}
{\color{red}expr} & ::= & {\color{red}var} & \text{(имя переменной)} \\
 & | & {\lambda\, \color{red}{var}}\,.\; {\color{red}expr} & \text{(абстракция)} \\
 & | & {\color{red}expr\ expr} & \text{(применение)}
\end{array}$$

Имя переменной может быть словом. Кроме того, мы различаем строчные и заглавные буквы, считая, к примеру, $ab$ и $aB$ двумя различными именами[^case].

Применение левоассоциативно: ${\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$:

```{figure} /_img/lxx1.svg
```

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

```{figure} /_img/lxx2.svg
```

Наиболее разумным представляется второй вариант, так как в таком случае смысл выражения $λ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$:

```{figure} /_img/lxy.fyx.svg
```

В это выражение переменные $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}}]$$

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

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

$$\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}$$

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

**Теорема (Чёрч — Россер):** пусть $\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}$.

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

```{figure} /_img/church-rosser.svg
```

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

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

$$\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}$$

Так как выражение $(λ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}$

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

```{figure} /_img/cr-equiv.svg
```

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

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

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

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

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

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

$$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$$

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

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

- Натуральные числа начинаются с нуля[^zero]
- $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{aligned}
z &:= λz\, s.\; z \\
s &:= λn.\; λz\, s.\; s\ n
\end{aligned}$$

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

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

Обозначим искомую функцию, складывающую два числа, как $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{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}$$

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

## Упражнения

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

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. Сумма всех натуральных чисел в списке

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

[^redex]: Aнгл. redex (*red*ucible *ex*pression).

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

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

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