What is the lambda calculus?
From an on-line introduction to the lambda calculus at Monash University: The lambda calculus is a formal mathematical system devised by Alonzo Church to investigate functions, function application, and recursion. It has influenced many programming languages but none more so than the functional programming languages. Lisp was the first of these although only the “pure” Lisp sublanguage can be called a true functional language. Haskell, Miranda, and ML are more recent examples. Lambda calculus also provides the meta-language for formal definitions in denotational semantics. It has a good claim to be the prototype programming language. The lambda calculus is in many ways the prototype for all programming languages. Like the Turing machine, it is capable of implementing any computable function. Unlike the Turing machine, it focuses on the transformation rules that implement a function, rather than the underlying machine implementation. Hence it lies closer to the level of software than th