formal systemIn the 1930s, a new type of expressions, called lambda expressions, were introduced by Alonzo Church and Stephen Kleene for formalizing functions and their evaluation. They form the basis for lambda calculus, a formal system used in mathematical logic and the theory of programming languages.
The equivalence of two lambda expressions is undecidable. This is also the case for the expressions representing real numbers, which are built from the integers by using the arithmetical operations, the logarithm and the exponential (Richardson's theorem).
Many mathematical expressions include variables. Any variable can be classified as being either a free variable or a bound variable.
For a given combination of values for the free variables, an expression may be evaluated, although for some combinations of values of the free variables, the value of the expression may be undefined. Thus an expression represents a function
For a given combination of values for the free variables, an expression may be evaluated, although for some combinations of values of the free variables, the value of the expression may be undefined. Thus an expression represents a function whose inputs are the values assigned to the free variables and whose output is the resulting value of the expression.[citation needed]
For example, the expression
evaluated for x = 10, y = 5, will give 2; but it is undefined for y = 0.
The evaluation of an expression is dependent on the definition of the mathematical operators and on the system of values that is its context.
Two expressions are said to be equivalent if, for each combination of values for the free variables, they have the same output, i.e., they represent the same function. Example:
The expression