Wikipedia

Church encoding

This is an old revision of this page, as edited by Tony Sidaway (talk | contribs) at 14:06, 27 October 2005 (As church numeral etc now map here and are likely to be the most common entry path, put something about them into the opening sentence.). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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.

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 a function F to its n-fold composition F o F o ... o F.

Definition

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

<0> := λfx.x
<1> := λfx.fx
<2> := λfx.f(fx)
<3> := λfx.f(f(fx))
...
<n> := λfx.fnx
...

That is, the natural number n is represented by the Church numeral <n>, which is a lambda-term with the property that for any lambda-terms F and X,

<n> F X
= (λfx.fnx) F X
= (λx.Fnx) X
= Fn X

The notation here assumes the usual convention that unless otherwise indicated by parentheses, association is to the left on the right side of the ".", and to the right on the left side (where implied λ's are also omitted). Thus, λxyz.abc abbreviates λx.(λy.(λz.((ab)c))).

Computation with Church numerals

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

Successor := λnfx.f(nfx)

has the property that for any Church numeral <n>,

Successor <n>
= (λnfx.f(nfx)) <n>
= λfx.f(<n>fx)
= λfx.f(fnx)
= λfx.fn+1x
= <n+1>

Similarly,

Add := λmnfx.mf(nfx)

has the property that for any Church numerals <m>,<n>,

Add <m> <n>
= (λmnfx.mf(nfx)) <m> <n>
= λfx.<m>f(<n>fx)
= λfx.fm(fnx)
= λfx.fm+nx
= <m+n>

Likewise,

Predecessor := λnfx.n(λgh.h(gf))(λu.x)(λu.u)
Multiply := λmnfx.m(nf)x
Exponentiate := λmnfx.nmfx

have the expected properties

Predecessor <n> = <n-1> (n > 0)
Multiply <m> <n> = <m*n>
Exponentiate <m> <n> = <mn>

In similar fashion, all recursive functions are representable in the lambda calculus (are "λ-definable") using Church numerals.

Church numerals in other functional programming languages

In Haskell, a function that returns a particular Church numeral might be 

church 0 = \ f x -> x
church n = c
  where
    c f x = c' f (f x)
      where
        c' = church (n - 1)

The transformation from a Church numeral to an ordinary numeral might be 

unchurch n = n (+1) 0

Thus the (+1) function would be applied to an initial value of 0 n times, yielding the ordinary numeral for n. (By "ordinary numeral" is meant a numeral in the default representation, e.g. decimal, of whatever computer language is being used.)

In Scheme, one simple expression of the Church numerals is as follows: 

(define (church n)
  (if (= n 0)
    (lambda (f x) x)
    (lambda (f x) ((church (- n 1)) f (f x))))))

This set of Church numerals can be transformed to ordinary numerals as follows: 

(define add1 (lambda (x) (+ 1 x)))
(define unchurch (lambda (c) ((c add1 0)))

Then given (define two (church 2)), (unchurch two) returns the value 2.

There are other mappings -- the Church numerals will map onto any countable set. Here is a mapping onto the powers of 2. 

(define times2 (lambda (x) (* 2 x)))
(define unchurchpoweroftwo (lambda (c) (c times2 1)))

Then unchurchpoweroftwo three returns 8, the third power of 2.

Addition: (define (add (lambda m n) (lambda (f x) (m f (n f x))))) 

(define seven (church 7))
(define eight (church 8))
(unchurch (add seven eight))
==> 15

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

See also
Retrieved from "https://en.wikipedia.org/w/index.php?title=Church_encoding&oldid=26619972"