Church numeral encyclopedia topics

Browse Nearby Entries

Church lads and chur...

Church management so...

Church memorial

Church encoding

1 reference results for: Church numeral

Wikipedia

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; 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

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 other 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 x.

f^n = f circ f circ cdots circ 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 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 $scriptstyleoperatorname{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 $scriptstyleoperatorname{succ}(n)=n+1$ is β-equivalent to (plus 1).

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

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

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

The exponentiation function $scriptstyleexp(m,n)=m^n$ is straightforward given our 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 subtraction function can be written based on the predecessor function.

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

Translation with other representations

Most real-world languages have support for machine-native integers; the church and unchurch functions (given here in Haskell) convert between nonnegative integers and their corresponding church numerals. Implementations of these conversions in other languages are similar.

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

church :: Integer -> Church a


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

The same code as above, here given in F#

let rec church n = fun f x -> match n with


| 0 -> x

| n -> f (church (n-1) f x)

let unchurch f = f (fun x -> x + 1) 0

In the case of church, the keyword rec is required to allow recursion in F#.

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. 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 ≡ λa.λb. a

false ≡ λa.λ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.

Functions of boolean arithmetic can be derived for Church booleans:

and ≡ λm.λn. m n m

or ≡ λm.λn. m m n

not ≡ λm.λa.λb. m b a

xor ≡ λm.λn.λa.λb. m (n b a) (n a b)

Some examples:

and true false ≡ (λm.λn. m n m) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) (λa.λb. b) (λa.λb. a) ≡ (λa.λb. b) ≡ false

or true false ≡ (λm.λn. m m n) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) ≡ true

not true ≡ (λm.λa.λb. m b a) (λa.λb. a) ≡ (λa.λb. (λa.λb. a) b a) ≡ (λa.λb. b) ≡ false


Church pairs
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:
pair ≡ λx.λy.λz.z x y
fst ≡ λp.p (λx.λy.x)
snd ≡ λp.p (λx.λy.y)
An example:
fst (pair a b) ≡ λp.p (λx.λy.x) ((λx.λy.λz.z x y) a b) ≡ λp.p (λx.λy.x) (λz.z a b) ≡ (λz.z a b) (λx.λy.x) ≡ (λx.λy.x) a b ≡ a
See also
Lambda calculus
System F for Church numerals in a typed calculus
Mogensen-Scott encoding
References
 Directly Reﬂective Meta-Programming
 Some interactive examples of Church numerals



        
        Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)
This article is licensed under the GNU Free Documentation License.
Last updated on Thursday June 05,  2008 at 10:10:42 PDT (GMT -0700)
View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation
        

        







    
    
        
        
    



    CITE THIS SOURCE|PRINT


    


            
            
        
    
    
    















    
    
        
            
            
                
            
        
        
    



























    

    
    
         
            
            
                


















    


            
        
    
    
    











    
    
    
    
       
    






    
    
        
        
        
    









 


    Share This:


    





    

    

    
        
    

    



    















    

    








































   




    
    
    
        
        
        
        
    
    

  

            
        









    
        
             
            
                
                
                    
                
            
            
            
                
                
            
            
                
           
        
    





About
·
Privacy Policy
·
Terms of Use
·
Link to Us
·
Report Ad
·
Contact Us


    
    Copyright © 2008, Dictionary.com, LLC. All rights reserved.