На прошлой неделе я выкладывал сюда свое решение по реализации чисел Черча и жаловался, что не смог написать функцию вычитания единицы. Самостоятельно до решения так и не додумался, поэтому пошел искать в гугле.
Сложность тут в том, что нужно написать функцию, которая от выражения как бы убирает одно применение функции. То есть, например, из конструкции f(f(x)) получить f(x). В лямбда исчислении нет способа вместо выражения подставить пустоту, поэтому на первый взгляд задача кажется невыполнимой. Сам Черч считал, что составить такую функцию невозможно. Первым решение нашел его ученик Клини (изобретатель регулярных выражений, между прочим).
Решение заключается в том, чтобы посчитать от нуля до n, сохраняя при этом n - 1. Считать вперед мы уже умеем функцией Succ. Хранить предыдущее и текущее значение можно при помощи пар.
Берем пару (Zero, Zero), назовем ее p для краткости. Заменяем ее на (second(p), Succ(second(p)). Повторяем процедуру n раз. На выходе получается пара (n - 1, n). А n - 1 — это как раз то значение, которое нам и нужно, вытаскиваем его селектором first.
Имея функцию для вычитания единицы несложно написать функцию вычитания одного числа из другого. Посмотреть на эти функции вживую: https://repl.it/@buyfn/Church-arithmetic.
Пока изучал вопрос, нашел статью, где автор утверждает, что нашел несколько других, более простых, способов выразить эту же функцию. Я, признаться, не смог их понять. Возможно, сможете вы: http://okmij.org/ftp/Computation/lambda-calc.html.