Цифры церкви: как мне интерпретировать числа из выражений?

Церковная цифра n — это функция, которая принимает другую функцию f и возвращает функцию, которая применяет f к своему аргументу n раза. Итак, 0 a (где 0, как вы сказали, λf.λx.x ) возвращает λx.x, потому что это применяет a к x 0 раз.

1 a дает вам λx. a x, 2 a дает вам λx. a (a x) и так далее.

Ниже приведено объяснение, основанное на статье автора Эрхан Багдемир в комментарии к ответу от sepp2k.

Основные моменты, которые нужно усвоить:

• все числительные Черча являются функциями двух параметров;
• for Church numerals, it is implied that:
  • f — is the 'successor' function (i.e. function which accepts a Church numeral and return church numeral next one, it's basically and increment);
  • x — это (число церкви) значение, представляющее «ноль» (начальная точка отсчета).

Имея это в виду:

λf . λx . x

будет равно нулю, если мы передадим соответствующие f (в данном конкретном случае неважно, какая функция будет передана как f, так как она никогда не применялась) и x:

λf . λx . ZERO

следующий:

λf . λx .  fx

будет оцениваться как 1:

λf . λx . INCREMENT ZERO

и это:

λf . λx . f f x

будет равен 2:

λf . λx . INCREMENT(INCREMENT ZERO)

и так далее для всех последующих чисел.

См. мой (более широкий) ответ на другой (но тесно связанный) вопрос.

Церковное число n (скажем, 2) представляет собой «действие» по применению любой заданной функции n раз (здесь — два раза) к любому заданному параметру.

Церковное числительное по определению – это функция, которая принимает два параметра, а именно
1) функцию
2) параметр, выражение или значение, к которому применяется указанная функция.

Когда предоставленная функция является функцией-преемником, а предоставленный второй параметр равен Zero , вы получаете числовое значение. (2, в приведенном выше примере)

Церковная цифра 2 по определению,

λf . λx . f( f( x)) 

, Которая, очевидно, является функцией, которая принимает два параметра.

При передаче функции-преемника, то есть f(x)=x+1 в качестве первого параметра и нуля в качестве второго параметра функции, мы получаем...

f(f(0))  
=f(1) 
=2

Это объяснение несколько упрощено, поскольку определение функции-преемника и ноль не такие, как показано в лямбда-исчислении.

См.: http://www.cse.unt.edu/~tarau/teaching/GPL/docs/Church%20encoding.pdf Отличное объяснение церковных кодировок