The lambda calculus provides a fairly small set of primitives for defining a language for computation: only function definition and application! However, there exists an even more minimal calculus called the SKI combinator calculus. It only has three functions S, K and I (and function application), hence the name.
To show this, we'll define a set of transformation rules than can convert any arbitrary expression in lambda calculus to some combination of S, K and I.
Definitions
First, what S, K and I are:
(K x y) = x(S x y z) = ((x z) (y z))(I x) = x
Clearly, I is the identity function we previously explored. Less obvious is that K is T, which can be rewritten as (λx,y -> x). S is an interesting beast (I have no further comment, other than that I seem to recall it has a special name).
It seems incredible that the complexity of lambda calculus, as limited as it is, can still be expressed as a combination of these 3 functions. We just need to follow a simple set of rules, applying the appropriate one on the outermost expression repeatedly.
(λx -> x) = I(λx -> c) = (K c)ifcdoesn't depend onx(λx -> (f x)) = f(λx -> (y z)) = (S (λx -> y) (λx -> z))
The first 3 should be fairly straightforward. To understand #4, note that S is a function that takes in 3 parameters, and applies the first two to the last one (independently, then applying the first result to the second). Since the RHS of #4 only supplies 2 parameters to S, that means it can still accept 1 more which will have (λx -> y) and (λx -> z) applied to it. Clearly, these are just dummy functions always returning y and z respectively, so the expression accepts 1 parameter and evaluates (y z), which is the LHS.
To demonstrate using these rules, we'll go over a few examples. First is proving that T is equivalent to K:
T = (λx,y -> x) = (λx -> (λy -> x))
= (λx -> (K x)) [by 2]
= K [by 3]
We can also find the definition for F:
F = (λx,y -> y) = (λx -> (λy -> y))
= (λx -> I) [by 1]
= (K I) [by 2]
Numbers
How about numbers?
We've already seen that 0 = F = (K I).
1 = (λx,y -> (x y))
= (λx -> (S (λy -> x) (λy -> y))) [by 4]
= (λx -> (S (K x) I)) [by 2, 1]
= (S (λx -> (S (K x))) (λx -> I)) [by 4]
= (S (S (λx -> S) (λx -> (K x))) (K I)) [by 4, 2]
= (S (S (K S) K) (K I)) [by 2, 3]
Similar to how 1 in Church numerals is just the application of x once to y, you may notice that the above expression is equivalent to (S (S (K S) K) 0). If we work out the equivalent representation of 2 in SKI combinator calculus, we'll also find that 2 = (S (S (K S) K) 1). Pretty neat stuff.
Do we really need I?
Commonly, (S K) is used as a representation for F instead of the (K I) we derived above: this illustrates that there can be more than one SKI representation for any lambda calculus expression. However, I find deriving (S K) to be much less intuitive. Here it is:
F = (λx,y -> y)
= (λx,y -> ((λz -> y) (x y)) [introduce dummy function]
= (λx,y -> ((K y) (x y))) [by 2]
= (λx -> (S (λy -> (K y)) (λy -> (x y)))) [by 4]
= (λx -> (S K x)) [by 3]
= (S K) [by 3]
We explored previously that F can be used to generate the identity function simply by applying it to a variable:
(F x) = id
Thus, we can actually express I using S and K, meaning that our calculus only needs 2 combinators instead of 3! (We can rewrite I as ((S K) K), for example.) This is more of a neat trick than anything else, but it's why this calculus is sometimes referred to as just the SK combinator calculus.
Can we go deeper?
In fact, there exists a single combinator ι (iota) that can be used to generate S, K and I.
ι = (λf -> ((f S) K))
This is written using S and K for simplicity, though we could expand them to get it in pure lambda calculus.
I is simply (ι ι) (ι applied to itself):
I = (ι ι) = ((ι S) K)
= (((S S) K) K) [def'n of ι]
= (S S K K) [removing extra parens]
= ((S K) (K K)) [def'n of S]
= (F (K K)) [def'n of F]
= I [(F x) = id]
K is simply (ι (ι (ι ι))) (ι applied to itself 3 times):
K = (ι (ι (ι ι))) = (ι (ι I))
= (ι ((I S) K)) [def'n of ι]
= (ι (S K)) [def'n of I]
= (((S K) S) K) [def'n of ι]
= (S K S K) [removing extra parens]
= ((K K) (S K)) [def'n of S]
= (K K (S K)) [removing extra parens]
= K [def'n of K]
S is simply (ι (ι (ι (ι ι)))) (ι applied to itself 4 times):
S = (ι (ι (ι (ι ι)))) = (ι K)
= ((K S) K) [def'n of ι]
= (K S K) [removing extra parens]
= S [def'n of K]
Given the four conversion rules we explored previously and the 3 substitutions above, we can now represent any lambda calculus expression using only applications of ι! Incredible.
This will likely be the last post in the lambda calculus series. It's been fascinating to explore how functions can be used for everything in truly minimal languages.