Lambda Calculus and its historical & technical connection to Lisp

By Anton van Straaten

The above is the title of a talk which I presented at LispNYC on Sep 10, 2003. This page contains material and references associated with that talk, along with a few details about the occasion.

The Code

The "slides" in the talk were based on a small Common Lisp program, lambda.lisp. Lambda calculus expressions embedded in CL are used to build Church numerals (natural numbers), booleans, and the applicative order Y-combinator, which is all then used to implement the good ol' factorial function, the use of which is demonstrated in the last few lines of the program.

The code contains some comments but will probably not make much sense to anyone who did not attend the talk and who is not already familiar with lambda calculus. However, some of the references at the bottom of this page will help to provide context.

Quotes

Below are some quotes which were given during the talk.

As part of describing the context and history which led up to the development of the lambda calculus, I read the following quote from Leibniz (1677). It can be found on this page. The part I read was as follows:

"Whence it is manifest that if we could find characters or signs appropriate for expressing all our thoughts as definitely and as exactly as arithmetic expresses numbers or geometric analysis expresses lines, we could in all subjects in so far as they are amenable to reasoning accomplish what is done in Arithmetic and Geometry.

"For all inquiries which depend on reasoning would be performed by the transposition of characters and by a kind of calculus, which would immediately facilitate the discovery of beautiful results. For we should not have to break our heads as much as is necessary today, and yet we should be sure of accomplishing everything the given facts allow.

"Moreover, we should be able to convince the world what we should have found or concluded, since it would be easy to verify the calculation either by doing it over or by trying tests similar to that of casting out nines in arithmetic. And if someone would doubt my results, I should say to him: "Let us calculate, Sir," and thus by taking to pen and ink, We should soon settle the question.

"Now the characters which express all our thoughts will constitute a new language which can be written and spoken; this language will be very difficult to construct, but very easy to learn. It will be quickly accepted by everybody on account of its great utility and its surprising facility, and it will serve wonderfully in communication among various peoples, which will help get it accepted. Those who will write in this language will not make mistakes provided they avoid the errors of calculation, barbarisms, solecisms, and other errors of grammar and construction. In addition, this language will possess the wonderful property of silencing ignorant people. For people will be unable to speak or write about anything except what they understand, or if they try to do so, one of two things will happen: either the vanity of what they advance will be apparent to everybody, or they will learn by writing or speaking. As indeed those who calculate learn by writing and those who speak sometimes meet with a success they did not imagine, the tongue running ahead of the mind. This will happen especially with our language on account of its exactness. So much so, that there will be no equivocations or amphibolies, and everything which will be said intelligibly in that language will be said with propriety. This language will be the greatest instrument of reason."

Although these ideas ultimately led to the development of formal systems of logic, including the lambda calculus, it seems that we have yet to succeed in converting Usenet to the use of such a language...

Another quote which I read was the "Acknowledgements" section from the end of Sussman and Steele's original Scheme paper, "Scheme - An Interpreter for an Extended Lambda Calculus". I read the first two paragraphs of these acknowledgements, which explains how the decision to apply lambda calculus in the design of Scheme was the result of "an experimental and highly empirical approach to bootstrap our knowledge".

International Lisp Conference 2003

In omitting the final paragraph of the abovementioned acknowledgments, I happened to mention that Seymour Papert, Marvin Minsky, and others were acknowledged. ALU President Raymond de Lacaze, one of the more outspoken hecklers present in the audience, pointed out that some of these people would be speaking at ILC 2003. Since this was already the Nth time that something like this had been pointed out, this resulted in a discussion of whether it wouldn't be easier just to enumerate who wasn't going to be speaking at the conference. The conclusion was that Leibniz probably wouldn't be speaking, but that was about it!

My advice to anyone reading this: register now for ILC 2003 and get your ass to New York City in October!

Have Antenna, Will Surf!

As we worked our way through the last few hundred years of human thought on the subject of formal languages, some details were inevitably called into question. An audience member who shall remain anonymous, armed with nothing but a notebook computer and an external 802.11b antenna, effortlessly located half a dozen nearby wireless networks - ah, city life! Others go wardriving to look for unguarded wireless networks, but in NYC, one can sit comfortably in one's living room, and war-sofa! Naturally, since those present were all responsible software engineers and scientists, I am quite certain that no legally questionable appropriation of bandwidth in fact took place. In any case, all that matters is the end result: the group now had a fact-checker, able to find answers to arcane questions quicker than I could find them in my copious notes.

The 20th Century

Once we had worked our way through Bertrand Russell, Hilbert, and the gang which congregated at Princeton at various times during the 1920s and '30s, including Alonzo Church, Alan Turing, Kurt Godel, and Steven Kleene, it finally became possible to relate this to the work of one John McCarthy, who needs no introduction. Apparently, he too is appearing at ILC 2003; but then, you already knew that, since it follows from the all-except-Leibniz axiom given above.

The final link in the historic chain was contributed by Sussman and Steele, in their "interpreter for an extended lambda calculus", as already referenced above. Naturally, by our axiom of appearance, Gerald Jay Sussman is providing a keynote address at ILC 2003.

Lambda Calculus Technicalities

Presenting the history, along with sundry diversions and discussion, took much longer than I had originally intended. We finally turned to the meat of the lambda calculus, going over the three grammar rules and three reduction rules far too quickly, and then working through the Lisp example. We worked our way quite successfully through Church numerals and Booleans, before the nearby bars began to exert their siren call. The gathering, having at least partially absorbed the concept of building an entire universe out of nothing but functions, reconvened to a location able to provide the highly specialized liquids required to fuel continued discussion - which discussion, thus fueled, naturally continued well into the night.

References

Some of the following references were used during the preparation of the talk; others may be useful to anyone wishing to delve further into the lambda calculus. This is hardly a complete list on the topic - it's restricted mainly to introductory material.