Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Where does the choice of the Greek letter $\lambda$ in the name of “lambda calculus” come from? Why isn't it, for example, “rho calculus”?

share|improve this question
4  
So that in Haskell, the symbol could easily be replaced with `\`! –  leftaroundabout Sep 14 '11 at 18:21
1  
Not really relevant to the question, but: Anthony Morse's book "A Theory of Sets" is written in an extremely formalistic style, so I doubt that many people read enough of it to encounter the joke (embedded as part of the formalism) suggesting that the $\lambda$-abstraction operator be read as "lonzo". –  Andreas Blass Dec 19 '13 at 15:13

2 Answers 2

up vote 27 down vote accepted

The symbol “λ” is used for one of two basic constructions in the system introduced by Alonzo Church, specifically abstraction. The notation did not just happen to be chosen but was to distinguish it from another construction by Whitehead and Russell represented as “xˆ.” For his new system, Church initially used “∧x,” then replaced it to “λx” to ease printing, obviously, interpreting the former logical symbol as the capital Greek letter “Λ.”

See “History of λ-calculus and Combinatory Logic” by J. R. Hindley, F. Cardone (Handbook of the History of Logic, 5: 723–817, Elsevier, 2009).

share|improve this answer
    
I've found an online preprint –  Alexey Dec 19 '13 at 15:36

I heard that Church originally used the hat symbol above the bounded variable, like $\hat x.x$, in handwritten papers. Then, the notation became ^x.x because of old-fashioned typewriters. I think it first became $\Lambda x.x$ when more recent text processors appeared, and $\lambda x.x$ after that (for aesthetics reasons probably).

Thanks to the silent downvoter, I did some googling and found Barendregt version in “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(x) = 2x + 1$ is $2 \hat x + 1$. Church originally intended to use the notation $\hat x.2x + 1$. The typesetter could not position the hat on top of the $x$ and placed it in front of it, resulting in $\wedge x.2x + 1$. Then another typesetter changed it into $\lambda x.2x + 1$.

share|improve this answer
1  
The reference [100] belongs to Whitehead and Russell, not Church. The “History of λ-calculus and Combinatory Logic” paper distinguishes these two constructions, saying explicitly that Church had to introduce another notation. –  user13300 Sep 16 '11 at 5:14
    
Indeed, meta-lambda abstraction is denoted another way, and is not the same as that of the system by Church. –  user13300 Sep 16 '11 at 5:16

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.