|
==Church numerals==
A Church numeral is the representation of a [[natural number]] as a [[function (mathematics)|function]] under Church encoding. The [[higher-order function]] that represents natural number <tt>''n''</tt> is a function that maps aany other function <tt>''F''</tt> to its <tt>''n''</tt>-fold [[function composition|composition]] <tt>''F'' <smallsup>o''n''</smallsup> = ''F'' <small> ο ''F'' o</small> ... <small> o</small> ''F''</tt>.
===Definition===
Church numerals <tt><'''0''>', <'''1''>', <'''2''>', ...</tt>, are defined as follows in the [[lambda calculus]]:
: <code style="text-decoration:overline">0</code> ≡ <code>λf.λx. x</code>
: <tt><''0''> := λ''fx''.''x''</tt>
: <tt><'''1''' >equiv; := <code>λ''fx''f.''fx''λx. f x</ttcode>
: <tt><'''2''' >equiv; := <code>λ''fx''f.''λx. f'' (''fx''f x)</ttcode>
: <tt><'''3''' >equiv; := <code>λ''fx''f.''λx. f'' (''f'' (''fx''f x))</ttcode>
: ...
: <tt><'''n''' >equiv; := <code>λ''fx''f.''λx. f''<sup>''n''</sup>'' x''</ttcode>
: ...
That is, the natural number <tt>''n''</tt> is represented by the Church numeral <tt><'''n''></tt>', which is a lambda-term with thehas property that for any lambda-terms ''F'' and ''X'',
: '''n''' <code>''F'' ''X''</code> [[Lambda calculus#β-reduction|=<sub>β</sub>]] <code>''F''<sup>''n''</sup> ''X'' </code>
: <tt> <''n''> ''F X'' </tt>
: <tt> = (λ''fx''.''f''<sup>''n''</sup>x) ''F X'' </tt>
: <tt> = (λ''x''.''F''<sup>''n''</sup>x) ''X'' </tt>
: <tt> = ''F''<sup>''n''</sup> ''X'' </tt>
The notation here assumes the usual convention that unless otherwise indicated by parentheses, association is to the ''left'' on the right side of the "<tt>.</tt>", and to the ''right'' on the left side (where implied λ's are also omitted). Thus, <tt>λ''xyz''.''abc''</tt> abbreviates <tt>λ''x''.(λ''y''.(λ''z''.((''ab'')''c'')))</tt>.
===Computation with Church numerals===
In the lambda calculus, numeric functions are representable by corresponding functions of Church numerals, as in the following examples:
:The <tt>successor Successorfunction := λ''nfx'succ'.''f(''(x''nfx)='') </tt> x''+1:
has the property that for any Church numeral <''n''>,
: <tt> Successor <''n''> </tt>
: <tt> = (λ''nfx''.''f''(''nfx'')) <''n''> </tt>
: <tt> = λ''fx''.''f''(<''n''>''fx'') </tt>
: <tt> = λ''fx''.''f''(''f''<sup>''n''</sup>''x'')</tt>
: <tt> = λ''fx''.''f''<sup>''n+1''</sup>''x'' </tt>
: <tt> = <''n+1''> </tt>
Similarly,
: <tt> Add := λ''mnfx''.''mf''(''nfx'') </tt>
has the property that for any Church numerals <tt><''m''></tt>,<tt><''n''></tt>,
: <tt> Add <''m''> <''n''> </tt>
: <tt> = (λ''mnfx''.''mf''(''nfx'')) <''m''> <''n''> </tt>
: <tt> = λ''fx''.<''m''>''f''(<''n''>''fx'') </tt>
: <tt> = λ''fx''.''f''<sup>''m''</sup>(''f''<sup>''n''</sup>''x'') </tt>
: <tt> = λ''fx''.''f''<sup>''m+n''</sup>''x'' </tt>
: <tt> = <''m+n''></tt>
Likewise,
: <tt> Predecessor := λ''nfx''.''n''(λ''gh''.''h''(''gf''))(λ''u''.''x'')(λ''u''.''u'')</tt>
: <tt> Multiply := λ''mnfx''.''m''(''nf'')''x'' </tt>
: <tt> Exponentiate := λ''mnfx''.''nmfx'' </tt>
have the expected properties
: <tt> Predecessor <''n''> = <''n-1''> (''n'' > 0) </tt>
: <tt> Multiply <''m''> <''n''> = <''m''*''n''>
: <tt> Exponentiate <''m''> <''n''> = <''m''<sup>''n''</sup>>
: '''succ''' ≡ <code>λn.λf.λx. f (n f x)</code>
In similar fashion, ''all [[recursive function]]s'' are representable in the lambda calculus (are "λ-definable") using Church numerals.
Note that <code>n f x</code> =<sub>β</sub> <code>f<sup>''n''</sup> x</code>, so <code>f (n f x)</code> =<sub>β</sub> <code>f (f<sup>''n''</sup> x)</code> =<sub>β</sub> <code>f<sup>''n+1''</sup> x</code>.
===Church numerals in other functional programming languages=== ▼In [[Haskell programming language|Haskell]], a [[function (programming)|function]] that returns a particular Church numeral might be
The addition function add(''m'',''n'')=m+n iterates <code>f</code> ''n'' times (starting with <code>x</code>) and uses that result as the base case for ''m'' iterations of <code>x</code>.
church n = c
where
c f x = c' f (f x)
where
c' = church (n - 1)
: '''add''' ≡ <code>λm.λn.λf.λx. m f (n f x)</code>
The transformation from a Church numeral to an ordinary numeral might be
The multiplication function mult(''m'',''n'')=m*n
: '''mult''' ≡ <code>λm.λn.λf.λx. m (n f) x</code>
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.)
The exponentiation function exp(''m'',''n'')=m<sup>n</sup>
In [[Scheme programming language|Scheme]], one simple expression of the Church numerals is as follows:
: '''exp''' ≡ <code>λm.λn.λf.λx. n m f x</code>
(define (church n)
(if (= n 0)
(lambda (f x) x)
(lambda (f x) ((church (- n 1)) f (f x))))))
The predecessor function pred(''x'')=0 if ''x''=0, ''x''-1 otherwise.
This set of Church numerals can be transformed to ordinary numerals as follows:
: '''pred''' ≡ <code>λn.λf.λx. n (λg.λh. h (g f))(λu. x)(λu. u)</code>
(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.
▲===Church numerals in other functional programming languages===
There are other mappings -- the Church numerals will map onto any countable set. Here is a mapping onto the powers of 2.
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 programming language|Haskell]]) can make explicit the correspondence between nonnegative integers and lambda terms:
:<code>church :: Integer -> (a -> a) -> a -> a
(define times2 (lambda (x) (* 2 x)))
▲ :<code>church 0 = \ s f-> x\z -> xz</code>
(define unchurchpoweroftwo (lambda (c) (c times2 1)))
:<code>church n = \s -> \z -> s (church (n-1) s z)</code>
:<code>unchurch :: ((a -> a) -> a -> a) -> Integer
Then unchurchpoweroftwo three returns 8, the third power of 2.
▲ :<code>unchurch n = n ( \x -> x + 1) 0 </code>
Addition: (define (add (lambda m n) (lambda (f x) (m f (n f x)))))
Implementations of these conversions in other languages are similar.
(define seven (church 7))
(define eight (church 8))
(unchurch (add seven eight))
==> 15
==Church booleans==
| 