TITLE: The Why of Lambda AUTHOR: Eugene Wallingford DATE: May 26, 2009 7:18 PM DESC: ----- BODY: The Lambda Chair For the programming languages geek who has everything, try the Lambda Chair. The company took the time to name it right, then sadly took the promotional photo from the wrong side. Still, an attractive complement to any office -- and only $2,000. Perfect for my university budget! I found out about this chair on the PLT mailing list today. The initial frivolity led to an interesting excursion into history when someone asked:
Does anyone know if Church had anything in mind for lambda to stand for, or was it just an arbitrary choice?
In response, Matthias Felleisen shared a story that is similar to one I'd heard in the languages community before. At the beginning of the last century, mathematicians used ^ to indicate class abstractions, such as î : i is prime. Church used ^`, the primed version of the hat, to indicate function abstraction, because a function is a special kind of set. Church's secretary read this notation as λ, and Church let it stand. Later in the thread, Dave Herman offered pointers to a couple of technical references that shed further light on the origin of lambda. On Page 7 of History of Lambda-Calculus and Combinatory Logic, Cardone and Hindley cite Church himself:
(By the way, why did Church choose the notation "λ"? In [Church, 1964, §2] he stated clearly that it came from the notation "î" used for class-abstraction by Whitehead and Russell, by first modifying "î" to "∧i" to distinguish function-abstraction from class-abstraction, and then changing "∧" to "λ" for ease of printing. This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and "λ" just happened to be chosen.)
The two internal references are to an unpublished letter from Church to Harald Dickson, dated July 7, 1964, and to J. B. Rosser's 1984 paper Highlights of the History of the Lambda Calculus from the Annals of the History of Computing. Herman also pointed to Page 182 of The Impact of the Lambda Calculus in Logic and Computer Science:
We end this introduction by telling what seems to be the story how the letter 'λ' was chosen to denote function abstraction. In [100] Principia Mathematica the notation for the function f with f(i) = 2i + 1 is 2 î + 1. Church originally intended to use the notation î.2i + 1. The typesetter could not position the hat on top of the i and placed it in front of it, resulting in ∧i.2i + 1. Then another typesetter changed it into λi.2i + 1.
(I changed the variable x to an i in the preceding paragraph, because, much like the alleged trendsetting typesetter, I don't know how to position the circumflex on top of an x in HTML!) Even in technical disciplines, history can be an imprecise endeavor. Still, it's fun when we go from anecdote to a more reliable source. I don't know that I'll ever need to tell the story of the lambda, but I like knowing it anyway. -----