Church encoding

Church encoding is a means of embedding data and operators into the lambda calculus, the most familiar form being the church numerals, a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.

Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding; from the Church-Turing thesis we know that any computable operator (and its operands) can be represented under Church encoding.

Many students of mathematics are familiar with Gödel numbering members of a set; Church encoding is an equivalent operation defined on lambda abstractions instead of natural numbers.

Church numerals

A Church numeral is the representation of a natural number as a function under Church encoding. The higher-order function that represents natural number n is a function that maps any other function F to its n-fold composition Fⁿ = F ο F o ... o F.

Definition

Church numerals 0, 1, 2, ..., are defined as follows in the lambda calculus:

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

...

That is, the natural number n is represented by the Church numeral n, which has property that for any lambda-terms F and X,

n F X =_β Fⁿ X

Computation with Church numerals

In the lambda calculus, numeric functions are representable by corresponding functions of Church numerals, as in the following examples:

The successor function succ(x)=x+1:

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

Note that n f x =_β fⁿ x, so f (n f x) =_β f (fⁿ x) =_β fⁿ⁺¹ x.

The addition function add(m,n)=m+n iterates f n times (starting with x) and uses that result as the base case for m iterations of x.

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

The multiplication function mult(m,n)=m*n

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

The exponentiation function exp(m,n)=mⁿ

exp ≡ λm.λn.λf.λx. n m f x

The predecessor function pred(x)=0 if x=0, x-1 otherwise.

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

Church numerals in functional programming languages

The functions described above can be implemented in most functional programming languages (subject to type constraints) by direct translation of lambda terms. Since most real-world languages have support for machine-native integers, the church and unchurch functions (given here in Haskell) can make explicit the correspondence between nonnegative integers and lambda terms:

church :: Integer -> (a -> a) -> a -> a


church 0 = \s -> \z -> z
church n = \s -> \z -> s (church (n-1) s z)

unchurch :: ((a -> a) -> a -> a) -> Integer

unchurch n = n (\x -> x + 1) 0



Implementations of these conversions in other languages are similar.

Church booleans

Church booleans are the Church encoding of the boolean values true and false. Some programming languages use these as implementation model for boolean arithmetic, examples are Smalltalk and Pico programming language. The boolean values
are represented as functions of two values that evaluate to one or the other of their arguments.
Formal definition in lambda calculus:

true := λab.a
false := λab.b

Functions of boolean arithmetic can be derived for Church booleans:

And := λmnab.m(nab)b
Or := λmnab.ma(nab)
Not := λmab.mba

This section needs expansion. You can help by adding to it.See alsoLambda calculus

External linksSome interactive examples of Church numerals