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:
`v`

,_{0}`v`

,_{1}`v`

, ...,_{2} - 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)`

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

Copyright © 2014 Barry Watson. All rights reserved.