Is there any known reason why Alonzo Church chose Greek $\lambda$ as the "binding operator" for the Lambda Calculus?
$\begingroup$
$\endgroup$
2
-
7$\begingroup$ Seems to be answered on math.SE: math.stackexchange.com/a/64469/413. $\endgroup$– Joel David HamkinsCommented Dec 19, 2013 at 14:29
-
3$\begingroup$ We don't generally close questions here as a duplicate on another site, but rather we just link to them with an answer. I suggest that you should post an answer containing the link in my comment and perhaps a summary of the answer, and then the question will be completed here. The upvotes indicate to me that the question was appreciated here, and so it doesn't make sense to me to close or delete the question. $\endgroup$– Joel David HamkinsCommented Dec 19, 2013 at 18:42
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
This question has been answered on math.SE (as pointed out by Joel David Hamkins). With a reference to Lambda-Calculus and Combinators in the 20th Century by Felice Cardone and J. Roger Hindley, Handbook of the History of Logic Volume 5, 2009, Pages 723–817, it is stated that “$\lambda x$” comes from “$\hat x$” in Principia Mathematica. Here is a quote from a preprint of Lambda-Calculus and Combinators in the 20th Century:
By the way, why did Church choose the notation “$\lambda$”? In [A. Church, 7 July 1964. Unpublished letter to Harald Dickson, §2] he stated clearly that it came from the notation “$\hat x$” used for class-abstraction by Whitehead and Russell, by first modifying “$\hat x$” to “$\wedge x$” to distinguish function-abstraction from class-abstraction, and then changing “$\wedge$” to “$\lambda$” for ease of printing. This origin was also reported in [J. B. Rosser. Highlights of the history of the lambda calculus. Annals of the History of Computing, 6:337—349, 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 “$\lambda$” just happened to be chosen.
Assuming that “$\lambda x$” comes from “$\hat x$” in Principia Mathematica, let us look how it is used there.
In Principia Mathematica there are two ways the notation “$\hat x$” is used. The first use is to write “propositional functions,” it is introduced in Volume I, in Chapter I of the Introduction, on page 15. Here is a quote:
[...] When we wish to speak of the propositional function corresponding to “$x$ is hurt,” we shall write “$\hat x$ is hurt.” Thus “$\hat x$ is hurt” is the propositional function, and “$x$ is hurt” is an ambiguous value of that function. Accordingly though “$x$ is hurt” and “$y$ is hurt” occurring in the same context can be distinguished, “$\hat x$ is hurt” and “$\hat y$ is hurt” convey no distinction of meaning at all. [...]
The second use is to write classes in a way similar to the modern “$\{\,z\mid\psi(z)\,\}$”, it is introduced in Volume I, in Section C of Part I, in definition *20.01, on page 197. Here is some quote:
[...] But it is convenient to regard $f\{\hat z(\psi z)\}$ as though it had an argument $\hat z(\psi z)$, which we will call “the class determined by the function $\psi\hat z$.” [...]
-
3$\begingroup$ In his book "A Theory of Sets",A. P. Morse proposed that the abstraction operator $\lambda$ be read as "Lonzo". (But of course Alonzo Church had nothing to do with that idea.) $\endgroup$ Commented May 11, 2016 at 14:46