Church Number with SKI combinators

I wrote on my blog that lambda calculus is turing-complete the other day.

But more surprisingly you can simulate all the procedures executable on a turing machine with only three operators: S combinator, K combinator, and I combinator.

They are defined as follows respectively:

-- SKI combinator
i = \x -> x                             -- λx.x
k = \x -> \y -> x                       -- λxy.x
s = \x -> \y -> \z -> x z (y z)         -- λxyz.x z (y z)

There are other combinators, including the most famous one --Y combinator--.

I found an interesting table in which you can find a lot of combinators:

http://www.angelfire.com/tx4/cus/combinator/birds.html

Among them, I picked up a I* combinator, which seemed useful, and played around with it.

i' = s (s k)                            -- λxy.x y

Today's topic is how to represent church numbers in terms of SKI combinators.

I'll go with Haskell.

Here's the definition. I was able to define one, two, three, and four.

-- Church numeral
zero = k i
one = i
two = (s (s (k s) k)) i
three = (s (s (k s) k)) (s (s (k s) k) i)
four = (s (s (k s) k)) ((s (s (k s) k)) (s (s (k s) k) i))

I could continue it forever. But the definition above is somewhat awkward. I'll improve it later on. But for now, I'll go with it!

To assert that it really works correctly, I also implemented interfaces between lambda calculus world and standard computation world.

Here's it:

import Unsafe.Coerce

-- For assertion only
type Church = (Int -> Int) -> Int -> Int

unChurch :: Church -> Int
unChurch n = unsafeApply n (+1) (0)

unsafeApply n a b = unsafeApply' (unsafeCoerce n) a b
unsafeApply' :: Church -> (Int -> Int) -> Int -> Int
unsafeApply' n a b = n a b

main = do print $ unChurch zero
         print $ unChurch one
         print $ unChurch two
         print $ unChurch three
         print $ unChurch four
         print $ unsafeApply i' (^2) 10
         print $ unsafeApply i' (subtract 99) 10
         print $ unsafeApply ki (+40) 2

I had to use a forbiddened technique "Unsafe.Corece," since Haskell's clever type inference got in my way. For more details, let's consider the following I* combinator.

i* = s (s k)

This combinator works like λxy.x y, simply applying the function to the second argument.

And what will happen when reducing the next expression?

i* succ 0

= s (s k) succ 0

= (s k) 0 (succ 0)

= k (succ 0) (0 succ 0)

= succ 0

= 1

In the middle of the process, we've got k (succ 0) (0 succ 0). This seems OK, even though (0 succ 0) is clearly NG, because the part is not evaluated thanks to lazy evaluation.

But in Haskell, its wise type inferrence throws an error since it fails consistent type definitions.

So you have to keep GHC from inferring the type definition as for it, which can be achieved by a banned instruction "unsafeCoerce." This function seems useful when you define Y-combinator also, though Haskell has concise syntax for fixed point combinator.

Anyway you have to remmember that when using unsafeCoerce, you are responsible for its results -- your program might stop when running --. So a thorough check is required before using unsafeCoerce.

Thanks for reading.

Since I'm a newbie to Haskell, this post might include some mistakes.

In that case, please make a comment. All advices and corrections are welcomed.