“equational specification”的概念、定义、翻译、参考文献-科学参考

equational specification

Computer

A set of equations that specifies a computing system or abstract data type. More precisely, the system or data type is modelled 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, \dots}; 0, n + 1, n + m, n . m, n^{2})$
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, \dots}; 0, n + 1, n^{2})$
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 (Σ_{0}, E_{0}) |_{Σ}$
of the initial algebra T(Σ‎₀, E₀) with respect to Σ‎ is isomorphic with A.
Equational specification.
See also computable algebra.

单词	equational specification
释义	equational specification Computer A set of equations that specifies a computing system or abstract data type. More precisely, the system or data type is modelled 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, \dots}; 0, n + 1, n + m, n . m, n^{2})$ 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, \dots}; 0, n + 1, n^{2})$ 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 (Σ_{0}, E_{0}) \|_{Σ}$ of the initial algebra T(Σ‎₀, E₀) with respect to Σ‎ is isomorphic with A. Equational specification. See also computable algebra.
随便看	noise noise factor(symbol: F) noise figure(symbol: FdB) noise immunity noiseless coding noise margin noise sequence noise source noise temperature noisy mode Nok culture Nollet, Abbé Jean Antoine no-load nomad((in cytology)) nomadism Nomarski microscope nomenklatura Nomex cloth nomic composite hypothesis composite idea Composite Infrared Spectrometer composite intrusion composite material composite polymer