Título | Implementing Inequality and Nondeterministic Specifications with Bi-rewriting Systems |
Publication Type | Conference Paper |
Year of Publication | 1992 |
Authors | Levy J, Agustí-Cullell J |
Conference Name | Lecture Notes in Computer Science |
Volume | 785 |
Editorial | Springer-Verlag |
Paginación | 252-267 |
Resumen | Rewriting with non-symmetric relations can be considered as a computational model of many specification languages based on non-symmetric relations. For instance, Logics of Inequalities, Ordered Algebras, Rewriting Logic, Order-Sorted Algebras, Subset Logic, Unified Algebras, taxonomies, subtypes, Refinement Calculus, all them use some kind of non-symmetric relation on expressions. We have developed an operational semantics for these inequality specifications named bi-rewriting systems. In this paper we show the applicability of bi-rewriting systems to Unified Algebras and nondeterministic specifications. In the first case, we give a canonical bi-rewriting system implementing the basic theory of these algebras. In the second case, nondeterministic specifications are viewed as inclusion specifications, thus bi-rewriting is a sound, although not always complete deduction method. We show how a specification has to be completed in order to have both soundness and completeness. |