# The Church numerals (WIP)

Posted on March 18, 2021 by Suguivy

…WIP…

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:

``λx.x``

We can apply an argument to the function using a rule called β-reduction:

``(λx.x) 1``

`x` is binded to `1`:

``1``

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))
...``````

This is:

• 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:

In Python:

``````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
zero f x = x``````

To work easily with the numerals, we can create two functions, one for convert integers to church numerals and vice versa:

In Python:

``````def zero(f, x):
return x

def church(n):
if n == 0:
return lambda f,x: x
else:
pred_church = church(n-1)
return lambda f,x: f(pred_church(f,x))

def unchurch(c):
return c(lambda x: x+1, 0)``````

``````church :: Integer -> Church a