Итак, идея церковных цифр в том, чтобы кодировать «данные» с помощью функций, верно? Это работает путем представления значения некоторой общей операцией, которую вы выполняете с ним. Поэтому мы можем пойти и в другом направлении, что иногда может прояснить ситуацию.
Церковные цифры являются унарным представлением натуральных чисел. Итак, давайте используем Z для обозначения нуля и Sn для представления преемника n. Теперь мы можем считать вот так: Z, SZ, SSZ, SSSZ ... Эквивалентная цифра Церкви принимает два аргумента - первый соответствует S, а второй - Z - затем использует их для построения вышеуказанного шаблона. Поэтому, учитывая аргументы f и x, мы можем считать вот так: x, f x, f (f x), f (f (f x)) ...
Давайте посмотрим, что делает PRED.
Во-первых, он создает лямбду, принимающую три аргумента - n - это церковное число, предшественник которого мы, конечно, хотим, что означает, что f и x являются аргументами для получающегося числа, что, таким образом, означает что тело этой лямбды будет f применено к x на один раз меньше, чем n.
Затем он применяет n к трем аргументам. Это сложная часть.
Второй аргумент, который соответствует Z от предыдущего, это λu.x - постоянная функция, которая игнорирует один аргумент и возвращает x.
Первый аргумент, который соответствует S из более раннего, это λgh.h (g f). Мы можем переписать это как λg. (λh.h (g f)), чтобы отразить тот факт, что только самая внешняя лямбда применяется n раз. Эта функция принимает накопленный результат до g и возвращает новую функцию с одним аргументом, который применяет этот аргумент к g, примененному к f. Что, безусловно, сбивает с толку.
Так ... что здесь происходит? Рассмотрим прямую замену с S и Z. В ненулевом числе Sn n соответствует аргументу, связанному с g. Итак, помня, что f и x связаны во внешней области, мы можем считать вот так: λu.x, λh. h ((λu.x) f), λh'. h' ((λh. h ((λu.x) f)) f) ... Выполняя очевидные сокращения, мы получаем это: λu.x , λh. h x, λh'. h' (f x) ... Шаблон здесь таков, что функция передается «внутрь» одного слоя, и в этот момент S будет применять ее, а Z будет игнорировать ее. Таким образом, мы получаем одно приложение f для каждого S , за исключением самого внешнего.
Третий аргумент - это просто функция тождества, которая покорно применяется самым внешним S, возвращая конечный результат - f, примененный один раз меньше, чем число S слоев, которым соответствует n.