What is λ-Calculus?

λ-Calculus is a formal system in mathematics invented by Alonzo Church as a means of doing research in the Foundations of Mathematics. It turned out to be very useful in that it led to the resolution of the Entscheidungsproblem.

Both Alonzo Church and Alan Turing published papers in 1936 in which they answered the Entscheidungsproblem in the negative; Church used his λ-calculus to do it, while Turing used what became known as the Turing Machine. However, it is Alonzo Church who gets the credit for resolving the Entscheidungsproblem because his paper was published first.

One reason that the Turing Machine is more well known than λ-calculus may be that the Turing Machine is easier to understand. In fact, many explanations of λ-calculus are presented while making comparisons to the Turing Machine.

An early computer programming language called LISP was based on Church's λ-calculus. LISP and FORTRAN were the first two higher level computer programming languages.