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:

• variables: v0, v1, v2, ...,
• abstractor: λ,
• parentheses and dot: (, ), ..

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

• x∈Λ, where x is a variable,
• if M∈Λ then λx.M∈Λ, where x is a variable,
• if M,N∈Λ then (MN)∈Λ.

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:

• λx.x
• λx.λy.x
• (λx.x λy.y)

References

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