Church Numerals

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)

add operation

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

Comments

ADDRESS

  • Email: jimmykobe1171@126.com
  • Website: www.catharinegeek.com