# Church Numerals

## Introduction

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 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 its argument.

Basically speaking, church numerals is just another way to present natural numbers, in higher-order function style.

For example, church number `zero` means a function `f` is to be applied 0 times, church number `one` means function `f` is to be applied 1 times, church number `n` means function `f` is to be applied n times.

```zero = id ( id is the identity function )
one = f
...
n = f.f.f.f...f (here '.' means function composition, so there is n times composition of function f)
```

## Implementation in Haskell

Haskell is born to be functional, so it is easy to show the concept of church numbers.

First, we need to define a type synonym for church numbers:

```type CNum a = (a -> a) -> (a -> a)
```

What's saying here is that type `CNum a` is a function that take a function `a->a` and return a function `a->a`.

#### the first church number `zero`

In order to deduce church number, we need to define a church number first, say zero.

```zero :: CNum a
zero f = id
```

The `id` here is identity function that return function argument, like `id 3 = 3`

#### successor of church number

Successor of church number means apply function one more times. So we can use function composition in haskell: the `.` syntax.

```succ :: CNum a -> CNum a
succ cn = \f -> f.(cn f)
```

#### int to church number

It is useful to convert an int to a church number and vice versa. We first define the equation between int 0 and church number zero, then we use recursive and `succ` function defined before to deduce church number.

```int2ch :: Int -> CNum a
int2ch 0 = zero
int2ch n = succ (int2ch (n-1))
```

#### church number to int

Church number to int is easy to implement, we just apply the `(+1)` function and argument 0 to church number `cn`, the definition of cn is applying a function n times. So with function `(+1)`, it just plus 1 n time from 0 and then return integer n.

```ch2int :: CNum Int -> Int
ch2int cn = cn (+1) 0
```

#### predecessor of church number

To calculate the predecessor, we first change the church number to int and then minus 1, after that we change int back to church number, simple.

```predec :: CNum Int -> CNum Int
predec cn = int2ch (ch2int cn - 1)
```

The sum of two church number `cn1` and `cn2` means applying function `cn1 + cn2` times.

```chadd cn1 cn2 = \f x -> cn1 f (cn2 f x)
```

We can use function composition to simplify as below:

```chadd :: CNum a -> CNum a -> CNum a
chadd cn1 cn2 = \f -> (cn1 f).(cn2 f)
```

#### multiply operation

The sum of two church number `cn1` and `cn2` means applying function `cn1 * cn2` times. First we apply function f cn2 times as `cn2 f`, then we take `cn2 f` as a new function, and apply it cn1 times as `cn1 (cn2 f)`.

```chmulti cn1 cn2 = \f -> cn1 (cn2 f)
```

Again with function composition, we can simplify as below:

```chmulti :: CNum a -> CNum a -> CNum a
chmulti cn1 cn2 = cn1.cn2
```

#### exponentialtion operation

for example, consider exponent is church number two and base three, then

```two three = (\f -> f.f) (\f -> f.f.f)
= (\f -> f.f.f).(\f -> f.f.f)

so,
two three f = (\f -> f.f.f).(\f -> f.f.f) f
= (\f -> f.f.f) f.f.f
= (f.f.f).(f.f.f).(f.f.f)
```

we can see that `two three` is a function that takes function f and return a function that apply f 9 times, which is exactly the definition of exponentiation.

So we can define exponentiation operation as below, where `cn1` is exponent and `cn2` is the base.

```chexp cn1 cn2 = cn1 cn2
```
Currently unrated