Abstract
We consider the problem of verifying confluence and termination of conditional term rewriting systems. Recently we have obtained some interesting results for unconditional term rewriting systems (TRSs) which are non-overlapping or, more generally, locally confluent overlay systems. These results provide sufficient criteria for termination plus confluence in terms of restricted termination and confluence properties (Gramlich 1994a). Here we generalize our approach to the conditional case and show how to solve the additional complications due to the presence of conditions in the rules. Our main result can be stated as follows: Any conditional TRS (CTRS) which is an innermost terminating overlay system such that all (conditional) critical pairs are joinable is complete, i.e., terminating and confluent.
This research was supported by the ‘Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)’.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. A. Bergstra and J. W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.
R.S. Boyer and J S. Moore. A Computational Logic. Academic Press, 1979.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69–116, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Formal models and semantics, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243–320. Elsevier-The MIT Press, 1990.
N. Dershowitz, M. Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In S. Kaplan and J.-P. Jouannaud, editors, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 31–44. Springer-Verlag, 1988.
B. Gramlich. New abstract criteria for termination and confluence of conditional rewrite systems. SEKI-Report SR-93-17, Fachbereich Informatik, Universität Kaiserslautern, 1993.
B. Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, 1994, special issue on term rewriting systems, to appear. A preliminary version appeared as “Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems” in Proc. LPAR'92, LNAI 624, pp. 285–296, 1992, see also SEKI-Report SR-93-09, Fachbereich Informatik, Universität Kaiserslautern, 1993.
B. Gramlich. On modularity of termination and confluence properties of conditional rewrite systems. In G. Levi and M. Rodríguez-Artalejo, editors, Proc. 4th Int. Conf. on Algebraic and Logic Programming, Madrid, Spain, volume 850 of Lecture Notes in Computer Science, pages 186–203, Springer-Verlag, 1994.
G. Huet and D. Lankford. On the uniform halting problem for term rewriting systems. Technical Report 283, INRIA, 1978.
G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, oct 1980.
D.E. Knuth and P.B. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, U. K., 1970. Reprinted 1983 in “Automation of Reasoning 2”, Springer, Berlin, pp. 342–376.
J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 2–117. Clarendon Press, Oxford, 1992.
A. Middeldorp. Modular properties of conditional term rewriting systems. Information and Computation, 104(1):110–158, May 1993.
A. Middeldorp. Completeness of combinations of conditional constructor systems. Journal of Symbolic Computation, 17:3–21, 1994.
A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. Journal of Symbolic Computation, 15:331–348, September 1993.
M.H.A. Newman. On theories with a combinatorial definition of equivalence. Annals of Mathematics, 43(2):223–242, 1942.
M.J. O'Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer-Verlag, 1977.
B.K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, 20:160–187, 1973.
C. Walther. Argument bounded algorithms as a basis for automated termination proofs. In E. Lusk and R. Overbeek, editors, Proc. of the 9th Int. Conf. on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 601–622. Springer-Verlag, 1988.
C.-P. Wirth and B. Gramlich. A constructor-based approach for positive/negative conditional equational specifications. Journal of Symbolic Computation, 17:51–90, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gramlich, B. (1995). On termination and confluence of conditional rewrite systems. In: Dershowitz, N., Lindenstrauss, N. (eds) Conditional and Typed Rewriting Systems. CTRS 1994. Lecture Notes in Computer Science, vol 968. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60381-6_10
Download citation
DOI: https://doi.org/10.1007/3-540-60381-6_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60381-8
Online ISBN: 978-3-540-45513-4
eBook Packages: Springer Book Archive