SKI combinators

In the last few days, I’ve tried to learn a bit of combinatory logic, using mostly the SKI combinator calculus system.

I’m currently reading An Introduction to Lambda Calculi for Computer Scientists, which has a chapter on combinatory logic. Reading this book is very humbling for me, as I lack a lot of math skills to understand it all.

Still, learning the mathematical theory behind functional programming is fascinating: these combinators can be used to define complex structures and eventually “programs”, using only very simple basic operations.

It is not practical though, using such a primitive means of computation can result in ridiculously large formulas to express the most basic operations.

When translating large λ-expressions to SKI expressions by hand, it can be hard to check that the two formulas are identical (i.e. that they can both be reduced to the same beta normal form). To make sure that my expression stays equivalent from one step to the next, I used a Haskell interpreter and more specifically its type inference feature.

module SKI where

data Nat = Zero | Succ Nat

instance Show Nat where
        show n = "Natural " ++ (show $ count n) where
                count Zero = 0
                count (Succ n) = 1 + count n

s = \x y z -> x z (y z)
k = \x y -> x
i = \x -> x

mkChurch n = \f x -> (iterate f x) !! n

Nat is the type for Peano Numbers. This type helps display display Church Numerals, using Succ for f and Zero for x.

Zero in Church Numerals is \f -> \x -> x:

SKI> (\f x -> x) Succ Zero
Natural 0

One in Church Numerals is \f -> \x -> f x:

SKI> (\f x -> f x) Succ Zero
Natural 1

Using the Church Number generator:

SKI> (mkChurch 42) Succ Zero
Natural 42

So much for the introduction, let’s convert λ-expressions to SKI expressions.

Three simple mappings can be used to convert λ-expressions to SKI expressions. According to EssAndKayCombinators, they were discovered by Moses Schönfinkel:

• \x -> x translates to I
• \x -> c translates to (K c)
• \x -> (p q) translates to S (\x -> p) (\x -> q)

Using the :type (abbreviated :t) command in a Haskell shell tries to infer the type of an expression. Sometimes types can be discovered, but when only λ-expressions and function calls on these expressions are used, the types are displayed as a, b, c… think of them as template parameters, or generics.

For example:

SKI> :t \x -> 1+x    -- this function takes x and returns 1+x
\x -> 1 + x :: Num a => a -> a

The type signature is a -> a, a being an instance of Num.

SKI> :t \f x -> f x  -- takes a function f and x, and applies f to x
\f x -> f x :: (a -> b) -> a -> b

The first parameter f of this λ-function is a function of type a -> b, it will produce a result of type b when given a value of type a. The second parameter is precisely this value.
There is indeed an infinity of functions with the same type signature, but by using only lambdas we are forcing the Haskell type system to use a different type for each parameter. This means that two expressions of the same normal form will have the same type. Still, two different λ-expressions could have the same type in Haskell (e.g. all church numerals!), but checking the type from one step to the next helps to detect obvious mistakes.

I got some help from the community in #haskell for the validity of this method; I had read blog posts praising its efficiency and friendliness and was not disappointed.

Although it is not completely safe to rely on the type inference to check if two SKI or λ-expressions are equivalent, it certainly helps; here is an example of the application of the previous three mappings to convert 1 from Church notation to a SKI expression.

SKI> :t \f -> \x -> f x    -- definition of 1 in Church Numerals
\f -> \x -> f x :: (a -> b) -> a -> b

Let’s remove the top \x using the third mapping.

SKI> :t \f -> (s (\x -> f) (\x -> x))
\f -> s (\x -> f) (\x -> x) :: (a -> b) -> a -> b

Apply the first and second mappings to get (K f) and I.

SKI> :t \f -> (s (k f) i)
\f -> s (k f) i :: (a -> b) -> a -> b

Use the first mapping to change the top \f:

SKI> :t s (\f -> s (k f)) (\f -> i)
s (\f -> s (k f)) (\f -> i) :: (a -> b) -> a -> b

Carry on…

SKI> :t s (s (\f -> s) (\f -> k f)) (k i) 
s (s (\f -> s) (\f -> k f)) (k i) :: (a -> b) -> a -> b

SKI> :t s (s (\f -> s) (\f -> k f)) (k i)
s (s (\f -> s) (\f -> k f)) (k i) :: (a -> b) -> a -> b

SKI> :t s (s (k s) (\f -> k f)) (k i)
s (s (k s) (\f -> k f)) (k i) :: (a -> b) -> a -> b

SKI> :t s (s (k s) (s (\f -> k) (\f -> f))) (k i)
s (s (k s) (s (\f -> k) (\f -> f))) (k i) :: (a -> b) -> a -> b

SKI> :t s (s (k s) (s (k k) i)) (k i)
s (s (k s) (s (k k) i)) (k i) :: (a -> b) -> a -> b

And finally change (S (K K) I) into K.

SKI> :t s (s (k s) k) (k i)
s (s (k s) k) (k i) :: (a -> b) -> a -> b

\f -> \x -> f x is now converted to S(S(K S)K)(K I). We can verify that it is still the same function:

SKI> Succ Zero
Natural 1

SKI> (\f -> \x -> f x) Succ Zero
Natural 1

SKI> (s (s (k s) k) (k i)) Succ Zero
Natural 1

Things get complicated pretty quickly. Here’s how “2” is encoded:

SKI> (s (s (k s) (s (k k) i)) (s (s (k s) (s (k k) i)) (k i))) Succ Zero
Natural 2

Using this notation, we can represent (1+) as \n -> \f -> \x -> f (n f x); you can think of it as having n and applying f to it once more.

Converting this λ-function to SKI got very large and I ended up with (s (k (s (s (k s) (s (k k) i)))) (s (s (k s) (s (k (s (k k))) (s (s (k s) (s (k k) i)) (k i)))) (k (k (k i))))).

Recursive reductions lead to the much simpler s (s (k s) k). Unsurprisingly, this structure is actually visible in our previously converted “1”, which is coded as “(1+) zero” with zero being (K I).

Applying this simplified encoding of (+1) on “1”:

SKI> (s (s (k s) k)) (mkChurch 1) Succ Zero
Natural 2

With such an incredibly inefficient way to represent numbers, 500,000 + 1 is computed in about 3 seconds on my machine, using the mkChurch function defined above. The SKI representation of this number is certainly very large :)

I find this breakdown in simple terms fascinating.