О кодировании натуральных чисел (часть 1)

Широко известно классическое индуктивное объявление натуральных чисел: ноль — натуральное число, и число следующее за натуральным — натуральное. На языке с поддержкой индуктивных типов это можно записать как-то так:

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)

В частности, первые несколько таких пар будут (мы считаем, что предыдущее для ноля — ноль):

\begin{aligned} pair \; 0 \; 0\\ pair \; 0 \; 1\\ pair \; 1 \; 2\\ \ldots \end{aligned}

А можем ли мы вместо выписывания всех пар просто придумать терм, позволяющий нам получить следующую пару из предыдущей? Да, запросто!

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-комбинатор, мы получили тот же набор функций. Вопрос же, на который мы постараемся ответить в следующий раз, а существует ли алгоритм, позволяющий переводить понятные индуктивные конструкции в лямбда-термы?