Abstract
We consider the problem of proving termination of order-sorted rewrite systems. The dominating method for proving termination of order-sorted systems has been to simply ignore sort information, and use the techniques developed for unsorted rewriting. The problem with this approach is that many order-sorted rewrite systems terminate because of the structure of the set of sorts. In these cases the corresponding unsorted system would not terminate.
In this paper we approach the problem of order-sorted termination by mapping the order-sorted rewrite system into an unsorted one such that termination of the latter implies termination of the former. By encoding sort information into the unsorted mapping, we are able to use general purpose termination orderings to prove termination of order-sorted rewrite systems whose termination depend on the sort hierarchy. We present a sequence of gradually stronger methods, and show that a previously published method is contained in ours as a special case.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
O.-J. Dahl and O. Owe. Formal development with ABEL. In Proceedings 4th International Symposium of VDM Europe, LNCS 552, 1991.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–116, 1987.
N. Dershowitz and C. Hoot. Natural termination. Theoretical Computer Science, 142:179–207, 1995.
H. Ganzinger. Order-sorted completion: the many-sorted way. Theoretical Computer Science, 89:3–32, 1991.
I. Gnaedig. ELIOS-OBJ: theorem proving in a specification language. In Proceedings of the 4th European Symposion on Programming, LNCS 582, pages 182–199, 1992.
I. Gnaedig. Termination of order-sorted rewriting. In Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy), LNCS 632, pages 37–52, 1992.
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: Equational deduction formultiple inheritance, overloading, exceptions and partial operators. Technical report, Programming Research Group, Oxford University Computing Laboratory, 1989.
J. A. Goguen and T. Winkler. Introducing OBJ3. Technical report, SRI International, Computer Science Lab, 1988.
S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering. Unpublished Note, Department of Computer Science, University of Illinois, Urbana, IL, 1980.
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.
P. Lescanne. Termination of rewrite systems by elementary interpretations. In Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy), LNCS 632, pages 21–36, 1992.
U. Waldman. Semantics of order-sorted specifications. Theoretical Computer Science, 94:1–35, 1992.
H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ölveczky, P.C., Lysne, O. (1996). Order-sorted termination: The unsorted way. In: Hanus, M., RodrÃguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1996. Lecture Notes in Computer Science, vol 1139. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61735-3_6
Download citation
DOI: https://doi.org/10.1007/3-540-61735-3_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61735-8
Online ISBN: 978-3-540-70672-4
eBook Packages: Springer Book Archive