Lambda Calculus

The lambda calculus is the model of computation that is most similar to the programming languages that we use today.

The alphabet of λ-terms is defined as follows:

The set of λ-terms, Λ, is defined inductively as follows:

The parentheses are usually dropped if they are not needed to give a unique reading. We call λ-terms of the form (MN) applications. We call λ-terms of the form λx.M abstractions. Examples of λ-terms follow:


H. P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. Elsiever, 1984.