λ-calculus

IV. Продвинутая арифметика

Вычитание

Теперь вернемся к реализации декремента. Здесь будет использоваться трюк, чем-то похожий на оптимизацию динамики матрицами. А именно: для каждого числа n мы будем поддерживать пару (n, n-1). От пары для числа n: (n, n-1) мы можем переходить к паре для числа n+1: (n+1, n), преобразовывая пару (a, b) по правилу (succ a, a). Именно так, а не (succ a, succ b) — это важно.

Например: (2, 1) → (3, 2) → (4, 3) → ...

Теперь реализуем функцию для инкремента пары:

succ2 := \p. pair (succ (first p)) (first p)

Где-то здесь должен возникнуть вопрос: как это поможет реализовать декремент? Что ж, по-хорошему, мы бы сейчас написали что-то вроде

pred := \n. second (n succ2 (pair 0 -1))

То есть мы начинаем с пары (0, -1), затем n раз ее инкрементируем, и тогда второй член пары содержал бы нужное значение. Единственная проблема — число -1 нельзя выразить в той форме, в которой мы представляем числа. Но здесь пригодится хитрое определение succ2: оно игнорирует второй аргумент подаваемой ему пары. Значит, если вместо -1 написать что угодно, то декремент будет так же хорошо работать. Единственное, на что влияет этот параметр — на значение pred 0. Для удобства условимся, что pred 0 -> 0, так что окончательная реализация выглядит так:

pred := \n. second (n succ2 (pair 0 0))

Можно провести аналогию с таким циклом:

next, curr = 0, 0
repeat n times:
    curr = next
    next = next + 1
return curr

Ну и наконец вычитание. За O(a*b), ага.

sub := \a. \b. b pred a

Вообще, в λ-исчислении можно реализовать арифметику намного более оптимально. Но пока что нам важно выразить все понятия наиболее простым образом.

Сравнения

Пусть есть два числа a и b. Как понять, равны ли они, или одно больше другого? Здесь нам пригодится свойство pred 0 -> 0. Отсюда следует, что iszero (sub a b) тогда и только тогда, когда a - b <= 0, иначе говоря, a <= b. Соответственно:

le := \a. \b. iszero (sub a b)

Сравнение на "больше или равно" (greater than or equal to) симметрично:

ge := \a. \b. le b a

Сравнение на "меньше" выведем из того, что a < b и a >= b — противоположные утверждения.

lt := \a. \b. not (ge a b)

Наконец, сравнение на "больше":

gt := \a. \b. lt b a

Числа равны, если одно меньше или равно другого и наоборот:

eq := \a. \b. and (le a b) (le b a)
ne := \a. \b. not (eq a b)

Деление

Реализацию деления с округлением вниз предлагаем в качестве упражнения читателю.

div := \x. \d. (lt x d) 0 (succ (div (sub x d) d))