History of Lambda-calculus and Combinatory Logic

This is the most definitive history of lambda calculus of which I am aware, a most useful resource. It includes two contradictory stories, both told by Church, of why Church picked the symbol 'lambda' (see p 7), but not the story that Church conceived the predecessor function after exposure to laughing gas at his dentist. (Does anyone know a source for that story?) My thanks to the authors for their efforts.

The definition of the predecessor is due to Kleene. See pages 56 and 57 of "Origins of Recursive Function Theory" by Stephen C. Kleene, Annals of this history of computing, Vol. 3 (1981) 52--67. He mentions the dentist, but not the laughing gas.
Oh my Gosh, Lambda Lambda Lambda is for real? I thought it was just a fictional frat house on Revenge of the Nerds! Wow thats cool.

An excellent companion paper to this one is Barendregt's "Impact of the Lambda calculus".

He refers to the story of Kleene and the predecessor:

"Be this as it may, Kleene did find a way to lambda define the predecessor function in the untyped lambda calculus, by using an appropriate data type (pairs of integers) as auxiliary device. In [69], he described how he found the solution while being anesthetized
by laughing gas (N2 O) for the removal of four wisdom teeth."

[69] is Reminiscences of logicians, Algebra and logic (Fourteenth summer res. inst., Austral. Math. Soc., Monash Univ., Clayton, 1974) (J. N. Crossley, editor), Lecture Notes in Mathematics, vol. 450, Springer-Verlag, Berlin and New York, 1975, pp. 1–62.

..haha; I cited both JRH and Barendregt in my recently-completed thesis, and Crossley is an old family friend. Small world!
I wish someone would do for Curry-Howard what Hofstadter did for Gödel.
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?