Crypt-equivalent algebraic specifications |
| |
Authors: | F L Bauer and M Wirsing |
| |
Affiliation: | (1) Institut für Informatik, Technische Universit?t München, Postfach 202420, D-8000 München 2, Federal Republic of Germany;(2) Fakult?t für Mathematik und Informatik, Universit?t Passau, Postfach 2540, D-8390 Passau, Federal Republic of Germany |
| |
Abstract: | Summary Equivalence is a fundamental notion for the semantic analysis of algebraic specifications. In this paper the notion of “crypt-equivalence”
is introduced and studied w.r.t. two “loose” approaches to the semantics of an algebraic specificationT: the class of all first-order models ofT and the class of all term-generated models ofT. Two specifications are called crypt-equivalent if for one specification there exists a predicate logic formula which implicitly
defines an expansion (by new functions) of every model of that specification in such a way that the expansion (after forgetting
unnecessary functions) is homologous to a model of the other specification, and if vice versa there exists another predicate
logic formula with the same properties for the other specification. We speak of “first-order crypt-equivalence” if this holds
for all first-order models, and of “inductive crypt-equivalence” if this holds for all term-generated models. Characterizations
and structural properties of these notions are studied. In particular, it is shown that firstorder crypt-equivalence is equivalent
to the existence of explicit definitions and that in case of “positive definability” two first-order crypt-equivalent specifications
admit the same categories of models and homomorphisms. Similarly, two specifications which are inductively crypt-equivalent
via sufficiently complete implicit definitions determine the same associated categories. Moreover, crypt-equivalence is compared
with other notions of equivalence for algebraic specifications: in particular, it is shown that first-order cryptequivalence
is strictly coarser than “abstract semantic equivalence” and that inductive crypt-equivalence is strictly finer than “inductive
simulation equivalence” and “implementation equivalence”. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|