Numbers are a way that we have to enumerate or to count things. We can represent they in various ways. For example, in our traditional positional numeric system numbers are represented as a sequence of symbols, in which the value of the number is determined by its symbols and their position. But we can represent it by other means.
Brief introduction to the λ-calculus
The lambda calculus (or λ-calculus) is a formal system and a model of computation based on function application.
This can sound very weird or abstract, but is not so difficult. You can think it as a programming function. For example, a function that returns its same argument can be represented as:
We can apply an argument to the function using a rule called β-reduction:
x is binded to
Also, functions in lambda calculus have only one parameter.
The Church numerals
Now that we hace introduced the lambda calculus, we will introduce the Church Numerals The church numerals are a representation of natural numbers using functions.
The numbers can be represented in Haskell as is:
λ-calculus Haskell Also Haskell 0 λf.λx.x \f -> \x -> x \f x -> x 1 λf.λx.f x \f -> \x -> f x \f x -> f x 2 λf.λx.f (f x) \f -> \x -> f (f x) \f x -> f (f x) 3 λf.λx.f (f (f x)) \f -> \x -> f (f (f x)) \f x -> f (f (f x)) ...
- The number zero is represented as a function that takes a function and a value, and returns the value.
- The number one is represented as a function that takes a function and a value, and returns the application of the function to the value.
- …and so on.
Representing church numerals
We are going to use Haskell and Python to represent the numerals.
We can define the number zero as is:
def zero(f, x): return x
To work easily, we have created a type alias:
type Church a = (a -> a) -> a -> a zero :: Church a = xzero f x
To work easily with the numerals, we can create two functions, one for convert integers to church numerals and vice versa:
def zero(f, x): return x def church(n): if n == 0: return lambda f,x: x else: = church(n-1) pred_church return lambda f,x: f(pred_church(f,x)) def unchurch(c): return c(lambda x: x+1, 0)
church :: Integer -> Church a 0 = \_ x -> x church = \f x -> f (predChurch f x) church n where predChurch = church (n-1) unchurch :: Church Integer -> Integer = c succ 0unchurch