Expressions may have "free variables" that are not defined in the expression, but taken from the context.

Two expressions are said to be equivalent if they can be evaluated to the same value.

Expressions and their evaluation were formalised by Alonzo Church and Stephen Kleene in the 1930s in their lambda calculus. The lambda calculus has has been a major influence in the development of modern mathematics and computer programming languages.

One of the more interesting results of the lambda calculus is that the equivalence of two expressions in the lambda calculus is in some cases undecideable. This is also true of any expression in any system that has power equivalent to the lambda calculus.

See also: