Abstract
Modular properties of term rewriting systems, i.e. properties which are preserved under disjoint unions, have attracted an increasing attention within the last few years. Whereas confluence is modular this does not hold true in general for termination. By means of a careful analysis of potential counterexamples we prove the following abstract result. Whenever the disjoint union \(\mathcal{R}_1 \oplus \mathcal{R}_2\) of two (finite) terminating term rewriting systems \(\mathcal{R}_1 ,\mathcal{R}_2\) is non-terminating, then one of the systems, say \(\mathcal{R}_1\), enjoys an interesting (undecidable) property, namely it is not termination preserving under non-deterministic collapses, i.e. \(\mathcal{R}_1\)⊕G({x,y}) → x,G({x, y}) → y is non-terminating, and the other system \(\mathcal{R}_2\) is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient syntactical criteria for modular termination of rewriting and provides the basis for a couple of derived modularity results. Furthermore, we prove that the minimal rank of potential counterexamples in disjoint unions may be arbitrarily high which shows that interaction of systems in such disjoint unions may be very subtle. Finally, extensions and generalizations of our main results in various directions are discussed and sketched.
This research was supported by the ‘Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)’.
Preview
Unable to display preview. Download preview PDF.
References
N. Dershowitz. A note on simplification orderings. Information Processing Letters, 9(5):212–215, 1979.
N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, pages 279–301, 1982.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69–116, 1987.
K. Drosten. Termersetzungssysteme. Informatik-Fachberichte 210. Springer, 1989. in German.
H. Ganzinger and R. Giegerich. A note on termination in combinations of heterogeneous term rewriting systems. Bulletin of the European Association for Theoretical Computer Science, 31:22–28, 1987.
B. Gramlich. A structural analysis of modular termination of term rewriting systems. SEKI Report SR-91-15, Dept. of Comp. Science, Univ. of Kaiserslautern, 1991.
B. Gramlich. Relating innermost, weak, uniform and modular termination of term rewriting systems. In Conference on Logic Programming and Automated Reasoning, St. Petersburg, Lecture Notes in Artificial Intelligence. Springer-Verlag, 1992. to appear.
B. Gramlich. Sufficient conditions for modular termination of conditional term rewriting systems (extended abstract). In Proc. of the 3rd International Workshop on Conditional Term Rewriting Systems, 1992. to appear.
G. Huet and D.C. Oppen. Equations and rewrite rules: A survey. In Ronald V. Book, editor, Formal Languages, Perspectives And Open Problems, pages 349–405. Academic Press, 1980.
J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume I. Oxford University Press, 1990.
M. Kurihara and I. Kaji. Modular term rewriting systems and the termination. Information Processing Letters, 34:1–4, 1990.
M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems. Journal of IPS, Japan, 34:632–642, 1990.
M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems with shared constructors. Technical Report SF-36, Hokkaido University, Sapporo, 1990.
A. Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 396–401, Pacific Grove, 1989.
A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Centre for Mathematics and Computer Science, Amsterdam, 1990.
A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In R.V. Book, editor, Proc. of the 4th Int. Conf, on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, pages 174–187. Springer, 1991.
M. Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters, 26:65–70, 1987.
Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, 1987.
Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, 1987.
Y. Toyama, J.W. Klop, and H.P. Barendregt. Termination for the direct sum of left-linear term rewriting systems. In N. Dershowitz, editor, Proc. of the 3rd Int. Conf. on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 477–491. Springer, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gramlich, B. (1992). Generalized sufficient conditions for modular termination of 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/BFb0013819
Download citation
DOI: https://doi.org/10.1007/BFb0013819
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