## Algebraic Languages

Some systems can be described in terms of their algebraic properties. Algebraic specification languages describe the behavior of a system in terms of axioms that completely characterize its desired properties. An example (and ancestor) of an algebraic specification language is OBJ.

In short, an algebra consists of a set of symbols denoting values of some type, a set of operations on this set, and axioms (sorts of rules) modeling the authorized behaviors of the system.

One important argument in favor of the algebraic approach to specification is that equations can be used to provide a mechanism for evaluating syntactically valid, but otherwise arbitrary, combinations of operations. For instance, on a stack model, an axiom might model that the result of pushing some element onto a stack and then removing it is precisely that very same element. This axiom is written:

Axioms can be oriented as rewrite rules (this is known as term rewriting), which makes algebraic specifications partially executable. The above axiom can be turned into the following rewrite rule:

pop(push(e,s)) ^ e meaning that every expression (term) matching the left-hand side can be replaced by the corresponding right-hand side term (after variables substitution). An axiomatic system can become a term rewriting system, which can be embedded in a deductive theorem prover. 