Широко известно классическое индуктивное объявление натуральных чисел: ноль — натуральное число, и число следующее за натуральным — натуральное. На языке с поддержкой индуктивных типов это можно записать как-то так:
data Nat :: * where
Zero :: Nat
Succ :: Nat -> Nat
zero :: Nat
zero = Zero
one :: Nat
one = Succ Zero
two :: Nat
two = Succ (Succ Zero)
add :: Nat -> Nat -> Nat
add n Zero = n
add n (Succ k) = Succ (add n k)
mul :: Nat -> Nat -> Nat
mul n Zero = Zero
mul n (Succ k) = add m (mul n k)
pred :: Nat -> Nat
pred Zero = Zero
pred (Succ k) = k
minus :: Nat -> Nat -> Nat
minus Zero m = Zero
minus n Zero = n
minus (Succ k) (Succ l) = minus k l
Простейший способ кодирования таких чисел при помощи нетипизированного лямбда-исчисления — метод Чёрча, не имеющий, как кажется, прямого отношения к понятному индуктивному типу:
\[
\begin{align*}
0 &= \lambda s z. z\\
1 &= \lambda s z. sz\\
2 &= \lambda s z. s(sz)\\
&\ldots\\
n &= \lambda s z. s^nz\\
\end{align*}
\]
При этом используется нотация степени, являющаяся синтаксическим сахаром для следующей записи:
\[
\begin{align*}
F^0(X) &= X\\
F^N(X) &= F^{N-1}(F(X))
\end{align*}
\]
Несмотря на странный вид таких термов, некоторую аналогию найти можно: z в лямбда-термах будет означать ноль, а некоторое количество s перед ним — увеличение этого нуля на единицу несколько раз. Для получения еще более сильной аналогии введем функцию succ:
\[
succ = \lambda n s z.s (n s z)
\]
Действительно, воспользовавшись таким термом, мы можем получить ожидаемое поведение:
\[
\begin{align*}
succ \; n &= (\lambda \color{red}n \color{black} s z.s (\color{red}n \color{black} s z)) \color{blue} (\lambda s z. s^n z) \color{black} = \\
&= (\lambda s z.s (\color{green} (\lambda \color{red} s \color{green} z. \color{red} s \color{green} ^n z) \color{blue} s \color{black} z)) = \\
&= (\lambda s z.s (\color{green} (\lambda \color{red} z \color{green}. s^n \color{red} z \color{green}) \color{blue} z \color{black})) = \\
&= (\lambda s z.s (s^n z)) = (\lambda s z.s^{n+1} z)
\end{align*}
\]
Также нам доступны простейшие арифметические операции (их можно проверить абсолютно аналогично тому, как выше проверяется функция succ):
\[
\begin{align*}
add &= \lambda m n. m \; succ \; n\\
mul &= \lambda m n. m \; add \; n\\
pow &= \lambda m n. m \; mul \; n
\end{align*}
\]
Эти функции дают важное свойство натуральных чисел в кодировке Чёрча. Применение терма, являющегося n-ным натуральным числом к некоторым термам f и x обеспечит n-кратное применение f к x:
\[
n f x = (\lambda s z.s^n z) f x = f^n x
\]
Вычитание и деление делаются несколько сложнее, с применением схемы примитивной рекурсии. Для этого обратимся к нескольким вспомогательным конструкциям. В первую очередь заведем пары из двух элементов. Индуктивное определение пары выглядит следующим образом:
data Pair :: * -> * -> * where
MkPair :: a -> b -> Pair a b
fst :: Pair a b -> a
fst (Pair x y) = x
snd :: Pair a b -> b
snd (Pair x y) = y
Мы же вновь должны пользоваться лямбда-исчислением для их кодирования:
\[
pair = \lambda a b c.c a b
\]
Действительно, мы може записать любую пару элементов таким образом, ведь \( pair X Y = \lambda c. c X Y \). Более того, нам доступны две проекции, позволяющие брать первый и второй элемент пары:
\[
\begin{align*}
fst &= \lambda p. p \; K \\
snd &= \lambda p. p \; K*
\end{align*}
\]
\( K \) и \( K* \) здесь — это комбинаторы \( \lambda x y.x \) и \( \lambda x y. y \) соответственно. Действительно:
\[
\begin{align*}
fst (pair X Y) &= (\lambda p.p \; K) \; ((\lambda a b c.c a b) X Y) = \\
&= (\lambda p.p \; K) \; (\lambda c.c X Y) = (\lambda c.c X Y) K = \\
&= K X Y = (\lambda x y.x) X Y = (\lambda y.X) Y = X
\end{align*}
\]
Как же воспользоваться этой конструкцией для получения предыдущего числа? Давайте зададим пару, которая будет содержать в качестве первого аргумента некоторое число, а в качестве второго — следующее за ним. Получить её довольно просто:
\[
pair \; n \; (succ \; n)
\]
В частности, первые несколько таких пар будут (мы считаем, что предыдущее для ноля — ноль):
\[
pair \; 0 \; 0\\
pair \; 0 \; 1\\
pair \; 1 \; 2\\
\ldots
\]
А можем ли мы вместо выписывания всех пар просто придумать терм, позволяющий нам получить следующую пару из предыдущей? Да, запросто!
\[
sp = \lambda p. pair \; (snd \; p) (snd \; (succ \; p))
\]
Здесь первым элементом новой пары становится второй элемент предыдущей, а вторым — следующее число. Применив такую функцию к паре \( (pair \; 0 \; 0) \) n раз мы получим пару, где второй элемент — число n, а первое — n - 1. А ровно это нам и требуется. Собирая все вместе получим функцию получения предыдущего натурального числа:
\[
pred \; n = \lambda n.fst \; (n \; sp \; (pair \; 0 \; 0))
\]
Из тех же соображений можно получить вычитание чисел:
\[
minus = \lambda n m. m \; pred \; n
\]
Важным наблюдением тут является то, что функция pred работает за \( O(n) \), а minus и вовсе за \( O(n^2) \)! Это, очевидно, является проблемой кодировки натуральных чисел Чёрча.
Целочисленное деление также можно получить, вспомнив рекурсивное выражение через вычитание:
\[
\left[ \frac{n}{m} \right] =
\begin{cases}
1 + \left[ \frac{n - m}{m} \right] & n \ge m \\
0 & n < m
\end{cases}
\]
Для написания данного выражения нам потребуется еще один тип данных — Boolean, для того, чтоб выражать условие, в соответствии с которым мы будем возвращать 0 или идти в рекурсивную ветку. Классическое определение Boolean тривиально — это тип, который населяют два конктреных значения:
data Bool :: * where
True :: Bool
False :: Bool
ifThenElse :: Bool -> a -> a -> a
ifThenElse True x y = x
ifThenElse False x y = y
В нетипизированном лямбда-исчислении представление тоже не особо сложное:
\[
\begin{align*}
true &= \lambda t f.t \\
false &= \lambda t f.f
\end{align*}
\]
Оператор if для такой кодировки совсем тривиальный:
\[
if = \lambda c x y.c x y
\]
Действительно, это можно проверить:
\[
\begin{align*}
if \; true \; X \; Y &= (\lambda c x y.c x y) \; true \; X \; Y = \\
&= (\lambda x y.true \; x \; y) \; X \; Y = \\
&= (\lambda y.true \; X \; y) \; Y = true \; X \; Y = \\
&= (\lambda t f.t) \; X \; Y = (\lambda f.X) \; Y = \\
&= X\\
if \; false \; X \; Y &= (\lambda c x y.c x y) \; false \; X \; Y = \\
&= (\lambda x y.false \; x \; y) \; X \; Y = \\
&= (\lambda y.false \; X \; y) \; Y = false \; X \; Y = \\
&= (\lambda t f.f) \; X \; Y = (\lambda f.f) \; Y = \\
&= Y
\end{align*}
\]
Для получения нашей формулы требуется еще понять, как сравнивать два числа. Простейший способ — вычесть одно из другого и сравнить с нулем. Вычитать мы уже умеем, а вот сравнение с нулем — это новое смешение двух миров: натуральных чисел и булевых значений. Тем не менее делается это сравнение очень просто. Заметим, что ноль выглядит так же, как false, а число отличное от нуля применит n раз какую-то функцию к нулю. Это позволяет нам написать функцию iszero по аналогии с if:
\[
iszero = \lambda n.n \; (\lambda x.false) \; true
\]
Теперь мы можем записать рекурсивную форму нашего деления:
\[
div = \lambda n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (div \; (minus \; n \; m) \; m))
\]
Отлично! За одним исключением: мы не умеем работать с рекурсивными термами. Но это легко исправить. Для начала проабстрагируемся по упоминанию div в нашем терме:
\[
div = (\lambda \color{red} d \color{black} n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (\color{red} d \color{black} \; (minus \; n \; m) \; m))) \; \color{red} div \color{black}
\]
Теперь наш терм принял вид \( X = F \; X \), иными словами div является неподвижной точкой для терма:
\[
\lambda d n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (d \; (minus \; n \; m) \; m))
\]
В соответствии с теоремой о комбинаторе неподвижной точки такая точка есть у любого терма, и находится она просто с помощью применения такого комбинатора к терму:
\[
Y = \lambda f.(\lambda x.f (xx))(\lambda x.f (xx))
\]
Итого, финальное нерекурсивное выражение для деления:
\[
div = Y (\lambda d n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (d \; (minus \; n \; m) \; m)))
\]
Подведем итог. Мы увидели простые и очевидные определения для таких типов данных как натуральные числа, пары и булевы значения. Также мы определили набор функций для работы с каждым. Следующим шагом было появление из воздуха некоторых лямбда-термов, удивительным образом копирующих поведение этих конструкций. Применяя их заодно с построением примитивной рекурсии и выражением рекурсивых термов через Y-комбинатор, мы получили тот же набор функций. Вопрос же, на который мы постараемся ответить в следующий раз, а существует ли алгоритм, позволяющий переводить понятные индуктивные конструкции в лямбда-термы?