Crypt-equivalent algebraic specifications (Q1095646): Difference between revisions

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''.