Abstract
We show various results for order-sorted term rewriting. We extend the result that order-sorted rewriting is complete if the rewrite system is compatible and confluent [17] by proving that order-sorted rewriting is complete if we consider the semantical sorts of the terms, i.e., we have confidence in the rewrite steps because they replace equals by equals.
In the order-sorted case the critical pair theorem [13] holds only if the rewrite system is weakly sort decreasing [16]. We show that every rewrite system can be made weakly sort decreasing by extending the expressibility of the signature by adding term declarations.
Unification with term declarations is undecidable in general [16]. We give a condition for the decidability of unification with term declarations that is considerably more general than the conditions given in [16]. We furthermore solve two open problems stated in [16]: unification in linear signatures is decidable and thus regularity of linear signatures, too.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
H. Chen and J. Hsiang. Order-sorted equational specification and completion. Technical report, State University of New York at Stony Brook, 1991.
H. Comon. Completion of rewrite systems with membership constraints. Research report, CNRS-LNRI, 1991.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Springer, 1985.
I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. In Proceedings of the 13th Colloquium on Trees in Algebra and Programming (CAAP), number 299 in Lecture Notes in Computer Science, pages 165–184. Springer, 1988.
M. Gogolla. Über partiell geordnete Sortennlengen und deren Anwendung zur Fehlerbehandlung in abstrakten Datentypen. PhD thesis, Naturwissenschaftliche Fakultät der Technischen Universität Braunschweig, 1986.
J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Operational semantics for order-sorted algebra. In W. Brauer, editor, Proceedings of the 12th International Colloquium on Automata, Languages and Programming, number 194 in Lecture Notes in Computer Science, pages 221–231. Springer, 1985.
J. A. Goguen and J. Meseguer. Completeness of many-sorted equational logic. Technical Report CSLI-84-15, Center for the Study of Language and Information, Stanford University, 1984.
J. A. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, 1988.
G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797–821, 1980.
G. Huet and D. C. Oppen. Equations and rewrite rules: A survey. In R, Book, editor, Formal Languages: Perspectives and Open Problems, pages 349–405. Academic Press, 1980.
C. Kirchner and H. Kirchner. Order-sorted computations in G-algebra. Technical report, Centre de Recherche en Informatique de Nancy, 1991.
C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ-3. In T. Lepistö and A. Salomaa, editors, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, number 317 in Lecture Notes in Computer Science, pages 287–301. Springer, 1988.
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebras, pages 263–297. Pergamon Press, 1970.
A. Martelli and U. Montanari. An efficient unification algorithm. ACM Trans. Prog. Lang. Syst., 4(2):258–282, 1982.
J. Meseguer and J. A. Goguen. Initiality, induction and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics. Cambridge University Press, 1985.
M. Schmidt-Schauss. Computational Aspects of an Order-Sorted Logic with Term Declarations. Number 395 in Lecture Notes in Artificial Intelligence. Springer, 1989.
G. Smolka, W. Nutt, J. A. Goguen, and J. Meseguer. Order-sorted equational computation. SEKI Report SR-87-14, Fachbereich Informatik der Universität Kaiserslautern, 1987.
U. Waldmann. Semantics of order-sorted specifications. Theoretical Comput. Sci., 94(1):1–36, 1992.
A. Werner. A semantic approach to order-sorted rewriting. unpublished, 1991.
L. With. Linear order-sorted unification. Forschungsberichte des Fachbereichs Informatik 1989-15, Technische Universität Berlin, 1989.
L. With. Multi-sort variables — a new concept for order-sorted unification. Forschungsberichte des Fachbereichs Informatik 1989-19, Technische Universität Berlin, 1989.
L. With. Completeness and confluence of order-sorted term rewriting. Forschungsberichte des Fachbereichs Informatik, Technische Universität Berlin, 1992. to appear.
L. With. Order-sorted unification with term declarations. Forschungsberichte des Fachbereichs Informatik, Technische Universität Berlin, 1992. to appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
With, L. (1993). Completeness and confluence of order-sorted term rewriting. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_30
Download citation
DOI: https://doi.org/10.1007/3-540-56393-8_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56393-8
Online ISBN: 978-3-540-47549-1
eBook Packages: Springer Book Archive