Abstract
In this paper, the problem of termination of rewriting in order-sorted algebras is addressed for the first time. Our goal is to perform termination proofs of programs for executable specification languages like OBJ3. An extension of Lexicographic Path Ordering is proposed, that gives a termination proof for order-sorted rewrite systems, that would not terminate in the unsorted case. We mention also, that this extension provides a termination tool for unsorted terminating systems, that usual orderings cannot handle.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G. Bernot, M. Bidoit, and C. Choppy. Abstract data types with exception handling: an initial approach based on a distinction between exceptions and errors. Theoretical Computer Science, 46:13–45, 1986.
N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 & 2):69–116,1987.
I. Gnaedig. Termination of rewriting in order-sorted algebras. Technical Report 91-R-108, Centre de Recherche en Informatique de Nancy, 1991.
I. Gnaedig. ELIOS-OBJ: Theorem proving in a specification language. In B. Krieg-Brückner, editor, Proceedings of the 4th European Symposium on Programming, pages 182–199. Lecture Notes in Computer Science, February 1992. Volume 582.
I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. Theoretical Computer Science, 72:169–202, 1990.
J. A. Goguen and J. Meseguer. Order-sorted algebra I: Partial and overloaded operations, errors and inheritance. Technical report, SRI International, Computer Science Lab, 1988. Given as lecture at a Seminar on Types, Carnegie-Mellon University, June 1983.
J. A. Goguen, J. Meseguer, and D. Plaisted. Programming with parameterized abstract objects in OBJ. Theory And Practice of Software Technology, pages 163–193, 1982.
John V. Guttag, James J. Horning, and J. M. Wing. Larch in five easy pieces. Technical report, Digital Systems Research Center, 1985.
J. Roger Hindley and Johnathan P. Seldin. Introduction to Combinators and Lambdacalculus. Cambridge University, 1986.
G. Huet and D. Oppen. Equations and rewrite rules: A survey. In R. V. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349–405. Academic Press, New York, 1980.
S. Kamin and J.-J. Lévy. Attempts for generalizing the recursive path ordering. Inria, Rocquencourt, 1982.
C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ-3. In Proceedings of 15th International Colloquium on Automata, Languages and Programming, volume 317 of Lecture Notes in Computer Science, pages 287–301. Springer-Verlag, 1988.
G. Smolka. Tel (version 0.9), report and user manual. SEKI report SR-87-11, Universität Kaiserslautern (Germany), 1988.
Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the Association for Computing Machinery, 34(1):128–143, January 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gnaedig, I. (1992). Termination of order-sorted rewriting. In: Kirchner, H., Levi, G. (eds) Algebraic and Logic Programming. ALP 1992. Lecture Notes in Computer Science, vol 632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013818
Download citation
DOI: https://doi.org/10.1007/BFb0013818
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55873-6
Online ISBN: 978-3-540-47302-2
eBook Packages: Springer Book Archive