Overview

The lambda calculus is a mathematical modeling of computer programming, introduced by Alonzo Church. It was intended as a way to study computation, and in particular, non-computability from a mathematical perspective. As such, it was not designed to be a usable programming language, rather it was designed to be simple from a mathematical perspective, in order to simplify computing to its essence and simplify proofs in the lambda calculus.

Terms

The definition of what constitutes a term in the lambda calculus is a set of rules that specify what constitutes a valid lambda calculus program.

• Variables - a list of variables is pre-specified (such as {% \{x_1,x_2,...x_n\} %}). Each variable is a term
• if {% M %} and {% N %} are terms, then {% (MN) %} is a term
• if {% M %} is a term and {% x %} is a variable, then {% \lambda x.M %} is a term

Reduction

Reduction is the process of taking a lambda expression and converting it into an equivalent expression. It is at the heart of what it means to compute something.

• Beta Reduction
• Eta Reduction