**…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
```

In Haskell:

*To work easily, we have created a type alias:*

```
type Church a = (a -> a) -> a -> a
zero :: Church a
= x zero f 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:
= church(n-1)
pred_church return lambda f,x: f(pred_church(f,x))
def unchurch(c):
return c(lambda x: x+1, 0)
```

In Haskell:

```
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 0 unchurch
```

## Operations

**…WIP…**