 |
|
| |
|
|
|
at Global Oneness Community.
Share your dreams and let others help you with the interpretation!
Dream Sharing Forum
|
|
Church encoding - Church numerals | | Church encoding - Church numerals: Encyclopedia II - Church encoding - 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 .
Church encoding - Definition.
Church numerals 0, 1, 2, ..., are defined as follows in the lambda calculus:
0 ≡ λf.λx. x
1 ≡ λf.λx. f x ...
See also:Church encoding, Church encoding - Church numerals, Church encoding - Definition, Church encoding - Computation with Church numerals, Church encoding - Translation with other representations, Church encoding - Church booleans | | | Church encoding, Church encoding - Church booleans, Church encoding - Church numerals, Church encoding - Computation with Church numerals, Church encoding - Definition, Church encoding - Translation with other representations, Lambda calculus | | |
| | | Church encoding: Encyclopedia II - Church encoding - Church numerals
Church encoding - 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 .
Church encoding - 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. fn 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 =β Fn X
Church encoding - 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) = fm(fn(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 times(m,n) = m * n uses the identity f(m * n) = (fm)n.
mult ≡ λm.λn.λf. n (m f)
The exponentiation function exp(m,n) = mn is straightforward given our definition of church numerals.
exp ≡ λm.λn. n m
The predecessor function 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)
Church encoding - 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
Other related archives=β, Alonzo Church, Church booleans, Gödel numbering, Haskell, Lambda calculus, Pico, Smalltalk, composition, higher-order function, lambda abstractions, lambda calculus, natural numbers, β-equivalent
 Adapted from the Wikipedia article "Church numerals", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki |
|
|
|
More material related to Church Encoding can be found here:
|
|
|
« Back
|
Search the Global Oneness web site |
|
|
|
|
|
Sneak-Peek of Global Oneness Community
Hi friend! The Global Oneness Community, the place for information and sharing about Oneness is not really launched yet (you will see there is still some clean up to do) ...but it is now open for a sneak-peek! And if you wish - please register and become one of the very first members to do so! Jonas
Forum Home,
Articles,
Photo Gallery,
Videos,
News,
Sitemap
...and much more!
|
