Skip navigation

When you hear “Craig’s Theorem”, you probably think of the Craig Interpolation Theorem, and rightly so.  This is the most famous theorem (I suppose) of philosopher and logician William Craig.  So I was surprised to find out there is another “Craig’s Theorem” that is even cooler for those of us interested in lambda calculus.  It is well known that every lambda term can be simulated using a combinator term written using combinators S and K.  Have you ever wondered if there is a way to simulate all lambda terms using just a single proper combinator Q (proper here means that the combinator is defined by a reduction rule showing how to reduce Q\ x_1\ \ldots\ x_k to some term built from applications of the variables x_1, \ldots, x_k)?  Craig’s (other) Theorem says no.  There is a very short (2 pages) proof given here (sorry, this is behind a paywall, I think).  I can give a simple variation of this proof here.

Suppose there were such a combinator Q.  Since it is, by assumption, combinatorily complete, there must be some way to write the identity combinator I using just Q.  Consider the reduction sequence I\ x\ \to^* M\ \to\ x, where M\ \to \ x is the last step in this reduction sequence (which must be of length at least one since I\ x is not the same as x).  Since M reduces, it must be of the form Q\ c_1\ \ldots\ c_n for some combinators c_1,\ldots,c_n.  But this tells us that Q must be projecting one of the inputs c_1,\ldots,c_n to the final result (and one of those c_i must be x).  So Q is a projection combinator.   This part is from the linked paper by Bellot.  Here is now an alternative conclusion.  If a sequence of reductions consists solely of projections of inputs, then that sequence must be terminating, because at each step, the size of the term is decreased by doing a projection.  But the lambda calculus includes nonterminating terms, so a projection function cannot be a sufficient basis for the lambda calculus.  Hence there is no one-combinator basis for the lambda calculus (and we need at least two, such as S and K).

Fun stuff!


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: