Натуральные числа

Натуральное число п можно представить в виде:

n = λ f x. fⁿ х

т.е. 0 = λ f х. х, 1 = λ f x. f х, 2 = λ f x. f (f x) и т.д. Данное представление называется «цифрами по Черчу». Цифры по Черчу обладают рядом удобных формальных свойств.

Можно определить операцию следования (увеличения на 1):

SUC = λ n f x. n f (f x)

В самом деле:

Определим функцию проверки числа на равенство нулю:

ISZERO λ п. n (λ x. false) true

поскольку

ISZERO 0 = (λ f х.х) (λ x. false) true = true

ISZERO n + 1 = (λ f x.fⁿ⁺¹ x)(λ x. false) true =

= (λ x. false) ⁿ⁺¹ true =

= (λ x. false)((λ x. false) ⁿ true) =

= false

Определим сложение и умножение:

Действительно:

и

Более сложной является операция вычиания единицы от натурального числа. Требуется найти лямбда-выражение (обозначим его PRE), такое, что PRE 0 = 0 и PRE п + 1 = п. Эту задачу решил Клини в 1935 году. Следуя Клини, определим вначале функцию PREFN, удовлетворяющую условиям:

Тогда (PREFN f) ^{n +1} (true, x) = (false, f ⁿ x) и функцию предшествования можно задать следующим образом:

Функцию PREFN можно определить как: