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”?
- Anybody can ask a question
- Anybody can answer
- The best answers are voted up and rise to the top
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).
I heard that Church originally used the hat symbol above the bounded variable, like $\hat x.x$, in handwritten papers. Then, the notation became
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”:
$\lambda$ symbol has (at least) 2 (related) meanings in mathematics (and logic), stemming directly from the ancient greek texts.
Its meaning stems form the fact that is the initial letter of the word ratio (greek: λόγος), meaning both analogy (i.e ratio) and logic (i.e rationality/reasoning)
Presumably this could be the reason Church used that symbol.
Furthermore, there is indeed a $\rho$-calculus which combines (or generalises) $\lambda$-calculus with pattern matching rewritting systems