Church encoding

In mathematics, 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; the Church-Turing thesis asserts 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

Church numerals are the representations of natural numbers under Church encoding. The higher-order function that represents natural number $n$ is a function that maps any function $f$ to its n-fold composition. In simpler terms, the "value" of the numeral is equivalent to the number of times the function encapsulates its argument.

$f^{n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ times}}}.\,$

All Church numerals are functions that take two parameters. Church numerals 0, 1, 2, ..., are defined as follows in the lambda calculus:

Then starting with zero, being not applying the function, then one being applying the function, ...

Number	Function definition	Lambda expression
0	$0\ f\ x=x$	$0=\lambda f.\lambda x.x$
1	$1\ f\ x=f\ x$	$1=\lambda f.\lambda x.f\ x$
2	$2\ f\ x=f\ (f\ x)$	$2=\lambda f.\lambda x.f\ (f\ x)$
3	$3\ f\ x=f\ (f\ (f\ x))$	$3=\lambda f.\lambda x.f\ (f\ (f\ x))$
...
n	$n\ f\ x=f^{n}\ x$	$n=\lambda f.\lambda x.f^{n}\ x$

Intuitively, Church numeral 3 is a function that performs any supplied function three times. The supplied function is first applied to a supplied parameter and then successively to its own result. It is important to remember that the end result is not the numeral 3 (unless the supplied parameter happens to be 0 and the function is a successor function). The function itself, and not its end result, is the Church numeral 3. As a further intuitive simplification, Church numeral 3 means simply to do anything three times. Furthermore, it contains within its definition an ostensive demonstration of what is meant by "three times".

Computation with Church numerals

In the lambda calculus, numeric functions are representable by corresponding functions on Church numerals. These functions can be implemented in most functional programming languages (subject to type constraints) by direct translation of lambda terms.

The addition function plus(m,n)=m+n uses the identity $f^{(m+n)}(x)=f^{m}(f^{n}(x))$.

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

The successor function succ(n)=n+1 is β-equivalent to (plus 1).

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

The multiplication function mult(m,n)=m*n uses the identity $f^{(m*n)}(x)=(f^{n})^{m}(x)$.

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

The exponentiation function exp(m,n)=m^n is straightforward by the definition of Church numerals.

exp ≡ λm.λn. n m

The predecessor function $\operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}$ works by generating an $n$-fold composition of functions that each apply their argument g to f; the base case discards its copy of f and returns x.

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

The $\operatorname {pred} (n)$ function is probably the most difficult of the basic operations to understand. To gain insight into the operation of $\operatorname {pred} (n)$ it is instructive to look at the expansion of its body when it is applied to the first few Church numerals.

Use abbreviations constx for (λu. x), Evalx for (λu. (u x)) and G for

(λg.λh. h (g f)).

Then

G const_x ≡ Eval_x,

G Eval_x ≡ Eval_{f x}.

The last rule may be chained, so

G (G Eval_x) ≡ Eval_{f (f x)}

etc. So for N > 0,

G^N const_x ≡ Eval_{f^N-1 x}.

Applying the above right-hand sides to the identity function (which is the last part of the body of pred) and including the formal parameters at the beginning gives the predecessor Church numeral for each of the numbers.

The subtraction function can be written based on the predecessor function.

sub ≡ λm.λn. (n pred) m

Successor

The successor adds one more call to the function f.

Number	Function definition	Lambda expression
$\operatorname {succ} n$	$\operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)$	$\operatorname {succ} =\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)$

Addition

To add two numbers n and m first apply the function n times and then apply it m.

Number	Identity	Function definition	Lambda expression	n * Successor
n + m	$f^{n+m}\ x=f^{n}(f^{m}x)$	$\operatorname {plus} \ n\ m\ f\ x=n\ f(m\ f\ x)$	$\lambda n.\lambda m.\lambda f.\lambda x.n\ f(m\ f\ x)$	$\lambda m.\lambda n.n\operatorname {succ} m$

Multiplication

Multiplication is also trivial in this encoding. Apply the function f m times to create a function. Then apply this function n times.

Number	Identity	Function definition	Lambda expression	Simplified
$n*m$	$f^{n*m}\ x=(f^{n})^{m}\ x$	$\operatorname {multiply} \ n\ m\ f\ x=n\ (m\ f)\ x$	$\lambda n.\lambda m.\lambda f.\lambda x.n\ (m\ f)\ x$	$\lambda n.\lambda m.\lambda f.n\ (m\ f)$

Power

Raising to a power is multiplying a number n by itself m times. Composing n with m achieves this.

Number	Function definition	Lambda expression	Simplified
$n^{m}$	$\operatorname {power} \ n\ m\ f\ x=(m\ n)\ f\ x$	$\lambda n.\lambda m.\lambda f.\lambda x.(m\ n)\ f\ x$	$\lambda n.\lambda m.m\ n$

Predecessor

The predecessor function used in the Church Encoding is,

$\operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}$.

To build the predecessor we need a way of applying the function 1 less time. A numeral n applies the function f n times to x. The predecessor function must use the numeral n to apply the function n-1 times.

Before implementing the predecessor function, here is a scheme that wraps the value in a container function. We will define new functions to use in place of f and x, called inc and init. The container function is called value. The left hand side of the table shows a numeral n applied to inc and init.

Number	Using init	Using const
0	$\operatorname {init} =\operatorname {value} \ x$
1	$\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)$	$\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x$
2	$\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))$	$\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)$
3	$\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))$	$\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))$
...	...	...
n	$n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)$	$n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)$

The general recurrence rule is,

$\operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)$

If there is also a function to retrieve the value from the container (called extract),

$\operatorname {extract} \ (\operatorname {value} \ v)=v$

Then extract may be used to define the samenum function as,

$\operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n$

The samenum function is not intrinsically useful. What we want is the initial value to skip an application of f. Call this new initial container const. The right hand side of the above table shows the expansions of n inc const. Then by replacing init with const in the expression for the same function we get the predecessor function,

$\operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)$

As explained below the functions inc, init, const, value and extract may be defined as,

$\operatorname {value}$	$\operatorname {extract} \ k$	$\operatorname {inc}$	$\operatorname {init}$	$\operatorname {const}$
$\lambda v.(\lambda h.h\ v)$	$k\ \lambda u.u$	$\lambda g.\lambda h.h\ (g\ f)$	$\lambda h.h\ x$	$\lambda u.x$

Which gives the lambda expression for pred as,

$\operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)$

Value container

The value container applies a function to its value. It is defined by,

$\operatorname {value} \ v\ h=h\ v$

so,

$\operatorname {value} =\lambda v.(\lambda h.h\ v)$

Extract

The value may be extracted by applying the identity function,

$I=\lambda u.u$

Using I,

$\operatorname {value} \ v\ I=v$

so,

$\operatorname {extract} \ k=k\ I$

Inc

The inc function should take a value containing v, and return a new value containing f v.

$\operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)$

Letting g be the value container,

$g=\operatorname {value} \ v$

then,

$g\ f=\operatorname {value} \ v\ f=f\ v$

so,

$\operatorname {inc} \ g=\operatorname {value} \ (g\ f)$

$\operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)$

Const

To implement pred the init function is replaced with the const that does not apply f. We need const to satisfy,

$\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x$

$\lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x$

Which is satisfied if,

$\operatorname {const} \ f=x$

Or as a lambda expression,

$\operatorname {const} =\lambda u.x$

Subtraction

Then subtraction is defined using pred.

Operation	Lambda expression
$n-m$	$\operatorname {minus} =\lambda n.\lambda m.m\operatorname {pred} n$

Note that minus returns zero if m > n.

Translation with other representations

Most real-world languages have support for machine-native integers; the church and unchurch functions convert between nonnegative integers and their corresponding church numerals. The functions are given here in Haskell, where the \ corresponds to the λ of Lambda calculus. Implementations in other languages are similar.

type Church a = (a -> a) -> (a -> a)

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

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

Church booleans

Church booleans are the Church encoding of the boolean values true and false. Some programming languages use these as an implementation model for boolean arithmetic; examples are Smalltalk and Pico. Boolean logic may be considered as a choice. Given two parameters and two values, a true function could choose the first parameter, and the false. The two definitions are known as Church Booleans.

$\operatorname {true} =\lambda a.\lambda b.a$

$\operatorname {false} =\lambda a.\lambda b.b$

Note that this definition allows predicates (i.e. functions returning logical values) to directly act as if-clauses, e.g. if predicate is a unary predicate,

predicate x then-clause else-clause

evaluates to then-clause if predicate x evaluates to true, and to else-clause if predicate x evaluates to false.

Because true and false choose the first or second parameter they may be combined to provide logic operators,

$\operatorname {and} =\lambda p.\lambda q.p\ q\ p$

$\operatorname {or} =\lambda p.\lambda q.p\ p\ q$

$\operatorname {not1} =\lambda p.\lambda a.\lambda b.p\ b\ a$ - This is only a correct implementation if the evaluation strategy is applicative order.

$\operatorname {not2} =\lambda p.\lambda a.\lambda b.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)$ - This is only a correct implementation if the evaluation strategy is normal order.

$\operatorname {xor} =\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b$

$\operatorname {IfThenElse} =\lambda p.\lambda a.\lambda b.p\ a\ b$

Some examples:

$\operatorname {and} \operatorname {true} \operatorname {false} =(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false}$

$\operatorname {or} \operatorname {true} \operatorname {false} =(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true}$

$\operatorname {not1} \ \operatorname {true} =(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda x.b)\ a=\lambda a.\lambda b.b=\operatorname {false}$

$\operatorname {not2} \ \operatorname {true} =(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false}$

Predicates

A predicate is a function that returns a Boolean value. The most fundamental predicate is $\operatorname {IsZero}$, which returns $\operatorname {true}$ if its argument is the Church numeral $0$, and $\operatorname {false}$ if its argument is any other Church numeral:

$\operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true}$

The following predicate tests whether the first argument is less-than-or-equal-to the second:

$\operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)$,

Because of the identity,

$x=y\equiv (x<=y\land y<=x)$

The test for equality may be implemented as,

$\operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)$

Church pairs

See also: Cons

Church pairs are the Church encoding of the pair (two-tuple) type. The pair is represented as a function that takes a function argument. When given its argument it will apply the argument to the two components of the pair.

Formal definition in lambda calculus:

$\operatorname {pair} \equiv \lambda x.\lambda y.\lambda z.z\ x\ y$

$\operatorname {first} \equiv \lambda p.p\ (\lambda x.\lambda y.x)$

$\operatorname {second} \equiv \lambda p.p\ (\lambda x.\lambda y.y)$

For example,

$\operatorname {first} \ (\operatorname {pair} \ a\ b)$

$=(\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b)$

$=(\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b)$

$=(\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x)$

$=(\lambda x.\lambda y.x)\ a\ b=a$

List encodings

An encoding of (immutable) lists of varying length must define a constructor for creating an empty list (nil), an operation testing whether or not a list is empty (isnil), an operation to prepend a given value to a (possibly empty) list (cons), and two operations to determine the first element and the list of the remaining elements of a nonempty list (head and tail).

Church pairs

A nonempty list can basically be encoded by a Church pair with the head of the list stored in the first component of the pair and the tail of the list in the second component. However, special care is needed to unambiguously encode the empty list. This can be achieved by encapsulating any individual list node within the second component of another pair whose first component contains a Church boolean which is true for the empty list and false otherwise, similar to a tagged union. Using this idea the basic list operations can be defined like this:

nil ≡ pair true true

isnil ≡ fst

cons ≡ λh.λt.pair false (pair h t)

head ≡ λz.fst (snd z)

tail ≡ λz.snd (snd z)

The second component of the pair encoding nil is never used provided that head and tail are only applied to nonempty lists.

Alternatively, one can define

cons ≡ pair

head ≡ fst

tail ≡ snd

nil ≡ false

isnil ≡ λl.l (λh.λt.λd.false) true

where the last definition is a special case of the general

process-list ≡ λl.l (λh.λt.λd. head-and-tail-clause) nil-clause

Higher-order function

As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its right fold function. For example, a list of three elements x, y and z can be encoded by a higher-order function which when applied to a combinator c and a value n returns c x (c y (c z n)).

nil ≡ λc.λn.n

isnil ≡ λl.l (λh.λt.false) true

cons ≡ λh.λt.λc.λn.c h (t c n)

head ≡ λl.l (λh.λt.h) false

tail ≡ λl.fst (l (λx.λp.pair (snd p) (cons x (snd p))) (pair nil nil))

See also

• Lambda calculus
• System F for Church numerals in a typed calculus
• Mogensen–Scott encoding

References

• Directly Reflective Meta-Programming
• Church numerals and booleans explained by Robert Cartwright at Rice University
• Theoretical Foundations For Practical 'Totally Functional Programming' (Chapters 2 and 5) All about Church and other similar encodings, including how to derive them and operations on them, from first principles
• Some interactive examples of Church numerals