An expression that asserts the equality of two terms. To be precise, an equation has the following form. Let Σ be a signature and let t1(X1,…, Xn) and t2(X1,…, Xn) be two terms over Σ involving the variables X1,…, Xn. Then
is an equation.
Equations are a natural means of expressing possible relationships between the functions in a signature. In fact, the equations can be used to specify or define the functions uniquely using initial algebra semantics (see equational specification).
Most systems in science and engineering are described mathematically using equations. Two stages are involved: a mathematical model of the system is made using sets and functions; some functions are known and others are to be found. Equations are postulated to define the unknown functions in terms of one another and the known functions. Research has shown that the same process is possible for computing systems. Indeed, theoretically it is known that any computing system, or any physical system that can be faithfully modelled using digital computation, can be characterized by small sets of equations. See also computable algebra.