Comments on Wadler's Blog: History of Lambda-calculus and Combinatory Logic

I wish someone would do for Curry-Howard what Hofs...

2008-06-06T17:05:00.000+01:00

I wish someone would do for Curry-Howard what Hofstadter did for Gödel.

An excellent companion paper to this one is Barend...

2008-06-06T05:09:00.000+01:00

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 deﬁne 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!

Oh my Gosh, Lambda Lambda Lambda is for real? I th...

2008-06-06T02:52:00.000+01:00

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.

JT
http://www.FIreMe.To/Udi

The definition of the predecessor is due to Kleene...

2008-06-05T16:27:00.000+01:00

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.