Skip navigation

Category Archives: Lambda Calculus

This past Tuesday (June 19) I gave the second lecture in the series I am working on, about optimal beta-reduction.  The screencast can be found here.  This lecture covers the basic nondeterministic graph reduction rules for lazy duplication.  The notes you will see my writing are here in ora and jpeg formats.  The lambdascope implementation I try using (and many thanks to Jan Rochel for this!) can be found here on hackage.  The lambdascope paper can be found here.

Advertisements

It is a warm start to summer here in Iowa, and among other interesting things to think about, I have been studying the subject of optimal beta-reduction, which has been developed from Jean-Jacques Levy’s dissertation in the 1970s to John Lamping’s 1990 POPL paper, and beyond.  I am using an amazing book by Andrea Asperti and Stefano Guerrini: The Optimal Implementation of Functional Programming Languages.

To help myself learn this, I am giving (and have decided to record) some lectures on the topic.  I am definitely not an expert, only an aspirant!  If you happen to watch these and find errors or confusions, please correct me.  The screencast for the first lecture, covering some main points of Chapter 2 of Asperti and Guerrini, is here.  The notes you will see me writing in the screencast are here, in jpg and ora formats.

I am interested in this because my friend Victor Maia of Ethereum Foundation is considering using a variant of Lamping’s abstract algorithm to run smart contracts in Ethereum, to be written in pure lambda calculus and verified with Cedille (the tool we are working on here now the past few years).

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!