Church integer
|
|
A Church integer is a representation of natural numbers as functions, invented by Alonzo Church as part of his lambda calculus. The natural number n is represented as a higher-order function, which takes a function f as argument and returns the n-fold composition f o f o ... o f as result.
For example, in Haskell, a function that returns a particular Church integer 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 integer to an integer 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 integer n.
In Scheme, one simple expression of the Church integers is as follows:
(define zero (lambda (x) (lambda (f) x))) (define one (lambda (x) (lambda (f) (f x)))) (define two (lambda (x) (lambda (f) (f (f x))))) (define three (lambda (x) (lambda (f) (f (f (f x))))))
This set of numbers can be transformed to integers as follows:
(define add1 (lambda (x) (+ 1 x))) (define unchurch (lambda (c) ((c 0) add1)))
Then (unchurch two) returns the value 2
There are other mappings--the church integers will map onto anything countable. Here is a mapping onto powers of 2.
(define times2 (lambda (x) (* 2 x))) (define unchurchpoweroftwo (lambda (c) ((c 1) times2)))
Then (unchurchpoweroftwo three) returns 8, the third power of 2.
See also
External links
- Some interactive examples of Church integers (http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/const-int/)
- An earlier version of the above article (http://planetmath.org/encyclopedia/ChurchInteger.html), which was posted on PlanetMath. This article is open-content.