## 2011年6月23日木曜日

### 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 combinatori = \x -> x                             -- λx.xk = \x -> \y -> x                       -- λxy.xs = \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:

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.
Here's the definition. I was able to define one, two, three, and four.
`-- Church numeralzero = k ione = itwo = (s (s (k s) k)) ithree = (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 onlytype Church = (Int -> Int) -> Int -> IntunChurch :: Church -> IntunChurch n = unsafeApply n (+1) (0)unsafeApply n a b = unsafeApply' (unsafeCoerce n) a bunsafeApply' :: Church -> (Int -> Int) -> Int -> IntunsafeApply' n a b = n a bmain = 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.