Crypt-equivalent algebraic specifications

abstract semantic equivalence crypt-equivalence first- order models implementation equivalence inductive simulation equivalence positive definability predicate logic semantic analysis of algebraic specifications term-generated models

Mathematics Subject Classification ID

Data structures (68P05)

Review text

Equivalence is a fundamental notion for the semantic analysis of algebraic specifications. The notion of ``crypt-equivalence is introduced and studied w.r.t. two ``loose approaches to the semantics of an algebraic specification T: the class of all first-order models of T and the class of all term-generated models of T. 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 first-order 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 crypt-equivalence is strictly coarser than ``abstract semantic equivalence and that inductive crypt-equivalence is strictly finer than ``inductive simulation equivalence and ``implementation equivalence.

Recommendations

Cites work

Cited in

(2)

This page was built for publication: Crypt-equivalent algebraic specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1095646)