Church encoding
Under Church encoding refers to the embedding of data and operators in the lambda calculus. The most common form are the Church numerals representing the natural numbers. They are named after Alonzo Church, the modeled data first in this way.
Church Numerals
Definition
The basic idea of encoding based on the Peano axioms, then the natural numbers by a start value - the 0 - and a successor function are defined. Accordingly, the Church - numerals are defined as follows:
Calculating with Church Numeralen
In lambda calculus arithmetic functions by corresponding functions via Church numerals are displayed. These functions can be implemented directly by transfer of lambda expressions in functional programming languages .
The successor function is defined as follows:
The addition of two numbers n and m is the m- fold application of the successor function on n:
The multiplication of two numbers n and m is the m- fold application of the addition ( n) to n:
The predecessor function:
Boolean expressions
Similar to the natural numbers can also be ( bivalent ) truth values in the lambda calculus model.
This also allows a simple control structure (IF THEN ELSE ) can be derived:
The variable is to be understood as a condition b, x as "then" and y as "ELSE ".
- Mathematical Logic
- Computability theory
- Mathematical notation