Church coding

Under church encoding means the embedding data and operators in the lambda calculus . The best known form are the Church numerals , which represent the natural numbers . They are named after Alonzo Church , who was the first to model data in this way.

Church numerals

definition

The basic idea for coding is based on the Peano axioms , according to which the natural numbers are defined by a starting value - the 0 - and a successor function. Accordingly, the Church numerals are defined as follows:

0 ≡λf.λx. x

1 ≡λf.λx. f x

2 ≡λf.λx. f (f x)

3 ≡λf.λx. f (f (f x))

...

n ≡λf.λx. fⁿ x

Calculating with Church numbers

In the lambda calculus, arithmetic functions can be represented by corresponding functions using Church numerals. These functions can be implemented in functional programming languages directly by transferring the lambda expressions.

The successor function is defined as follows:

succ ≡λn.λf.λx. f (n f x)

The addition of two numbers and is the application of the successor function to : ${\ displaystyle n}$ ${\ displaystyle m}$ ${\ displaystyle m}$ ${\ displaystyle n}$

plus ≡λm.λn.λf.λx. m f (n f x)

The multiplication of two numbers and is the application of the addition to : ${\ displaystyle n}$ ${\ displaystyle m}$ ${\ displaystyle m}$ ${\ displaystyle (+ n)}$ ${\ displaystyle n}$

mult ≡λm.λn.λf.λx. m (n f) x

The predecessor function:

pred ≡λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

Boolean expressions

Analogous to the natural numbers, (two-valued) truth values can also be modeled in the lambda calculus.

true ≡λx.λy. x

false ≡λx.λy. y

A simple control structure ( IF THEN ELSE ) can also be derived from this:

ifthenelse ≡λb.λx.λy.b x y

The variable is to be understood as a condition, as "THEN" and as "ELSE". ${\ displaystyle b}$ ${\ displaystyle x}$ ${\ displaystyle y}$