There are three syntactical elements in the lambda calculus:
- variables, usually named by single lowercase letters
- abstraction, written with lambda. Abstraction takes the form `λ x . body', where x is a variable and body is any expression (wff) of the lambda calculus.
- application. Application takes the form `(f g)',
where f and g are any expressions of lambda calculus.
There are three basic rules for determining equality or equivalence (as opposed to identity) of expressions in the lambda calculus:
- alpha reduction: `λ x . E' is equivalent to `λ y . E{y/x}', where E{y/x} is E with each free occurence of x replaced with y. This is subject to certain restrictions on the boundness of occurrences of y in E.
- beta reduction: `((λ x . E) E2' is equivalent to `E{E2/x}', subject to certain restrictions on bound variables in E.
- eta reduction: `λ x . (E x)' is equivalent to `E', assuming x does not appear free in E.
Alpha reduction says that, subject to some constraints, you can freely rename variables. Beta reduction is analogous to function application, with a syntactic flavour: it most closely resembles the call-by-name evaluation present in Algol-60. Finally, eta reduction expresses the notion of extensionality: two functions are (extensionally) equivalent if they produce the same output given the same input.