equational specification

equational specification A set of equations that specifies a computing system or abstract data type. More precisely, the system or data type is modeled by an algebra, and this algebra is defined by the equations using initial-algebra semantics.

Let A be an algebra of signature Σ. Then A is said to have an equational specification (Σ, E), under initial-algebra semantics, if E is a set of equations over Σ such that the initial algebra T(Σ, E) is isomorphic with A. For example, the algebra A = ({0,1,2,…}; 0, n+1, n+m, n.m, n²)

of natural numbers is specified by means of (Σ,E) shown in Fig. a.

An equational specification with hidden functions and sorts is an equational specification in which extra or hidden functions and sorts of data are allowed in order to construct equations. Inventing and adding functions, and even data types, to specify a computation or to a model a system is an obvious and natural technique. Consider the algebra B = ({0,1,2,…}; 0, n+1, n²)

of numbers with signature Σ^SQ shown in Fig. b. The algebra B is a reduct of the algebra A of numbers given above, i.e. A|_Σ^SQ = B,

and B can be specified by specifying A using the equational specification (Σ, E) given above. If A is isomorphic with the initial algebra T(Σ, E), then the reduct T(Σ, E)|_Σ^SQ

is isomorphic with the algebra B. Thus (Σ, E) is an equational specification of B with two hidden functions, namely addition and multiplication.

The square algebra B cannot be given a finite equational specification without using hidden functions; thus the technique is essential. It is known that any computable algebra can be given an equational specification using as little as six hidden functions and four equations, and initial-algebra semantics.

The general definition is as follows. An algebra A of signature Σ is said to have an equational specification (Σ₀, E₀) with hidden functions and sorts, under initial-algebra semantics, if Σ ⊆ Σ₀, and E₀ is a set of equations over Σ₀ such that the reduct T(Σ₀, E₀)|_Σ

of the initial algebra T(Σ₀, E₀) with respect to Σ is isomorphic with A.

See also computable algebra.