×

zbMATH — the first resource for mathematics

Conditional rewrite rules. (English) Zbl 0577.03013
The purpose of this paper is to develop a general study of conditional equational theories. A system of conditional equations is defined simply as a finite set of equational Horn clauses. It is shown that from an algebraic point of view these systems give rise to results analogous to those for classical equational theories. Unfortunately, for the related conditional rewriting systems the rewriting problem is unsolvable and the normal form function is uncomputable. Besides its intrinsic beauty such a general model may become a valuable tool for a ”top down” search of decidability thresholds.
Reviewer: C.Masalagiu

MSC:
03C05 Equational classes, universal algebra in model theory
68Q65 Abstract data types; algebraic specification
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Gogen, J.A.; Thatcher, J.W.; Wagner, E.G., An initial approach to the specification, correctness and implementation of abstract data types, ()
[2] Brandt, D.; Darringer, J.A.; Joyner, W.H., Completeness of conditional reductions, ()
[3] Bergstra, J.; Klop, J., Conditional rewrite rules: confluency and termination, () · Zbl 0658.68031
[4] Drosten, K., Toward executable specifications using conditional axioms, () · Zbl 0558.68019
[5] Huet, G.; Hullot, J.-M., Proofs by induction in equational theories with constructors, () · Zbl 0532.68041
[6] Huet, G.; Oppen, D.C., Equations and rewrite rules: A survey, ()
[7] Gaudel, M.-C., Génération et preuve de compilateurs basées sur une sémantique formelle des langages de programmation, Thèse d’etat, (1980), Nancy
[8] Kaplan, S., Un langage de spécifications de types abstraits algébriques, ()
[9] Knuth, D.E.; Bendix, P.B., Simple word problems in universal algebra, () · Zbl 0188.04902
[10] Lankford, D.S., Some new approaches to the theory and applications of conditional term rewriting systems, (1979)
[11] O’Donnel, M., Computing in systems described by equations, ()
[12] Pletat, U.; Engels, G.; Ehrich, H.-D., Operational semantics of algebraic specifications with conditional equations, 7th CAAP, (1981), Lille · Zbl 0549.68011
[13] Remy, J.I., Etude des systèmes de réécriture conditionnels et applications aux types abstraits algébriques, Thèse d’etat, (1982), Nancy
[14] Selman, A., Completeness of calculi for axiomatically defined classes of algebras, Algebra universalis, 2, 20-32, (1972) · Zbl 0251.08005
[15] Zilles, S.N., A look at algebraic specification, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.