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, n2)
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, n2)
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 (Σ0, E0) with hidden functions and sorts, under initial-algebra semantics, if Σ ⊆ Σ0, and E0 is a set of equations over Σ0 such that the reduct T(Σ0, E0)|Σ
of the initial algebra T(Σ0, E0) with respect to Σ is isomorphic with A.
See also computable algebra.
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, n2)
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, n2)
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 (Σ0, E0) with hidden functions and sorts, under initial-algebra semantics, if Σ ⊆ Σ0, and E0 is a set of equations over Σ0 such that the reduct T(Σ0, E0)|Σ
of the initial algebra T(Σ0, E0) with respect to Σ is isomorphic with A.
See also computable algebra.
More From encyclopedia.com
Specific Yield , specific yield Primitive Recursion , primitive recursive function A function that can be obtained from certain initial functions by a finite number of applications of composition and pri… Functional Analysis , Few concepts in modern social science history have generated as much discussion as those of structure and function and the type of analysis associate… Computation , Computation
Older methods
General-purpose digital computer
Error analysis
BIBLIOGRAPHY
In recent years there has occurred enormous technological deve… Specific Gravity , specific gravity (sp. gr.) The ratio of the weight of a substance to the weight of an equal volume of water, expressed as a number. For example, the… Computer Science , The term Computer Science encompasses three different types of research areas: computability, efficiency, and methodology.
General Introduction
Compu…
You Might Also Like
NEARBY TERMS
equational specification