cdiggins.com

What follows is intended a simple explanation of the SK calculus and its relationship to the Lambda calculus.

The SK calculus is a simple and complete programming language made up entirely of functions. The name comes from the fact that you can build any function you may want from two base functions: S and K.

S and K are defined in pseudo-code as follows:

  K(a, b) = a 
  S(a, b, c) = a(c)(b(c))

In the lambda calculus, this would be written as:

  K = a b . a b
  S = a b c . a c (b c)

In Haskell we would write:

  let K a b = a b
  let S a b c = a c (b c)

A key point to understanding this for those unfamiliar with the lambda calculus and Haskell, is that function application automatically occurs between any two consecutive terms. So “a b” means call the function “a” with the function “b” as an argument. The lambda calculus is also left-associative so “a b c” means call the function resulting from “a b” with the function “c” as an argument.

This may be a bit confusing at first because we are defining S to take three argument and K to take to arguments. This is due to the inherent property of functional languages that calling a function with one argument, where more are desired, will simply yield a new function which requires one fewer arguments. This is also known as currying.

So what I am saying is that the following statements are equivalent:

  K(f, g)
  K(f)(g)
  K f g

Hopefully you are with me so far. This is crucial to going further.

So having said these things the S K calculus can be used to define any function in the lambda calculus, without using any argument names. The I combinator, or identity function can be defined as follows:

  let I = S K K

This is in fact valid Haskell code. And if we query the type (e.g. using the :t command) we would see it to be exactly what we expect: (t -> t). Other functions (also known as combinators) can also be constructed similarly using the examples from Chris Rathman’s list of combinator birds. 

Unfortunately Haskell will fail if you try to type the M or Y combinators since it is unable to infer recursive types. In a later post I’ll explain how to implement the SK calculus in Cat, and how I plan to overcome the recursive type problem.

This entry was posted on Thursday, March 22nd, 2007 at 8:09 am and is filed under Everything. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.