Skip to main content
Post Made Community Wiki
Source Link

The lambda calculus was first published in 1933 by Alonzo Church, intended to be an alternative to first-order logic. Two of his students, Kleene and Rosser, proved it inconsistent in 1935. In 1936, another student, Alan Turing, proved that a stripped-down version was equivalent in computational power to the Turing machine. It was pretty much "just another example of a Turing-equivalent language" for about 30 years.

In the late 1960s and 1970s, John McCarthy, Dana Scott, and Peter Landin (among others) revived the lambda calculus: John McCarthy by loosely basing LISP on it, Dana Scott by giving it a set-theoretic interpretation, and Peter Landin by developing a theoretical machine that - unlike Turing's - was similar to actual computers and a transformation into its machine instructions. These things together showed that the lambda calculus was not only good at encoding mathematical procedures as programs, but could be compiled into reasonable programs that run on actual machines. Guy Steele showed shortly after in his series of "Lambda the Ultimate" papers that the programs could be run efficiently, and that the lambda calculus easily models many familiar programming language constructs.

Today, the lambda calculus is THE theory of programming languages. Among the ways to describe algorithms, its mathematical purity is unrivaled.

Compared to other mathematical areas, 30 years isn't a long time for something to lay dormant. But consider that Computer Science has only been around for about 70!