Church Numeral

lambda-calculus

Definition

Church Numeral

Church numerals are a type of Church encoding for natural numbers.

The general form for a Church numeral is:

where is a shorthand for applying repeatedly times.

Successor

Successor

The successor function is a combinator that is used to get the next number of a Church numeral and is defined as:

Addition

To add and , we need to apply a total of times. We can achieve this by first applying times (using the numeral ), and then applying times (using the numeral ) to the result.