понедельник, 28 февраля 2011 г.

Мимолётом о числах Чёрча

Классическое определение числа Чёрча - эта функция, которая принимает два значения: функцию и аргумент. И применяет функцию к аргументу какое-то число раз.

0 ≡ λfx. x
1 ≡ λfx. f x
n ≡ λfx. fn x


для таких чисел легко определить добавление единицы:

succ ≡ λnfx. n f (f x)

сложение двух чисел:

plus ≡ λmnfx m succ (n f x)

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

pred ≡ λnfx. ngh. h (g f)) (λu. x) (λu. u)

Может быть я глуп, но осознать это я не смог. Но можно попробовать написать немного проще:
Для начала рассмотрим такую конструкцию

pair ≡ λfsc. c f s
fst ≡ λp. (λfs. f)
snd ≡ λp. (λfs. s)


Благодаря её можно создавать кортежи и обращаться к ним:

fst (pair x y) → x
snd (pair x y) → y


Теперь всё просто:

init ≡ pair 0 0
next ≡ λp. pair (snd p) (succ (snd p))
pred ≡ λn. fst (n next init)


мы строим ряд:

0 → (0, 0)
1 → (0, 1)
2 → (1, 2)
n → (n-1, n)


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