Abstract
A term rewriting system is called complete if it is both confluent and strongly normalizing. Barendregt and Klop showed that the disjoint union of complete term rewriting systems does not need to be complete. In other words, completeness is not a modular property of term rewriting systems. Toyama, Klop and Barendregt showed that completeness is a modular property of left-linear TRS's. In this paper we show that it is sufficient to impose the constructor discipline for obtaining the modularity of completeness. This result is a simple consequence of a quite powerful divide and conquer technique for establishing completeness of such constructor systems. Our approach is not limited to systems which are composed of disjoint parts. The importance of our method is that we may decompose a given constructor system into parts which possibly share function symbols and rewrite rules in order to infer completeness. We obtain a similar technique for semi-completeness, i.e. the combination of confluence and weak normalization.
This paper is an abbreviated version of CWI report CS-R9059.
Partially supported by ESPRIT Basic Research Action 3020, INTEGRATION.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
N. Dershowitz, Termination of Linear Rewriting Systems (preliminary version), Proceedings of the 8th International Colloquium on Automata, Languages and Programming, Acre, Lecture Notes in Computer Science 115, pp. 448–458, 1981.
N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, in: Handbook of Theoretical Computer Science, Vol. B (ed. J. van Leeuwen), North-Holland, 1990.
K. Drosten, Termersetzungssysteme, Informatik-Fachberichte 210, Springer, 1989 (in German).
A. Geser, Relative Termination, Ph.D. thesis, University of Passau, 1990.
G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM 27(4), pp. 797–821, 1980.
J.W. Klop, Term Rewriting Systems, to appear in: Handbook of Logic in Computer Science, Vol. I (eds. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press, 1991.
M. Kurihara and I. Kaji, Modular Term Rewriting Systems: Termination, Confluence and Strategies, Report, Hokkaido University, Sapporo, 1988. (Abridged version: Modular Term Rewriting Systems and the Termination, Information Processing Letters 34, pp. 1–4, 1990.)
M. Kurihara and A. Ohuchi, Modularity of Simple Termination of Term Rewriting Systems, Journal of IPS Japan 31(5), pp. 633–642, 1990.
M. Kurihara and A. Ohuchi, Modularity of Simple Termination of Term Rewriting Systems with Shared Constructors, Report SF-36, Hokkaido University, Sapporo, 1990.
A. Middeldorp, Modular Aspects of Properties of Term Rewriting Systems Related to Normal Forms, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill, Lecture Notes in Computer Science 355, pp. 263–277, 1989. (Full version: Report IR-164, Vrije Universiteit, Amsterdam, 1988.)
A. Middeldorp, A Sufficient Condition for the Termination of the Direct Sum of Term Rewriting Systems, Proceedings of the 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, pp. 396–401, 1989.
A. Middeldorp, Confluence of the Disjoint Union of Conditional Term Rewriting Systems, Report CS-R8944, Centre for Mathematics and Computer Science, Amsterdam, 1989. (To appear in: Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting Systems, Montreal, 1990.)
A. Middeldorp, Termination of Disjoint Unions of Conditional Term Rewriting Systems, Report CS-R8959, Centre for Mathematics and Computer Science, Amsterdam, 1989.
A. Middeldorp, Unique Normal Forms for Disjoint Unions of Conditional Term Rewriting Systems, Report CS-R9003, Centre for Mathematics and Computer Science, Amsterdam, 1990.
A. Middeldorp, Modular Properties of Term Rewriting Systems, Ph.D. thesis, Vrije Universiteit, Amsterdam, 1990.
M.H.A. Newman, On Theories with a Combinatorial Definition of Equivalence, Annals of Mathematics 43(2), pp. 223–243, 1942.
M.J. O'Donnell, Equational Logic as a Programming Language, The MIT Press, 1985.
M. Rusinowitch, On Termination of the Direct Sum of Term Rewriting Systems, Information Processing Letters 26, pp. 65–70, 1987.
Y. Toyama, On the Church-Rosser Property for the Direct Sum of Term Rewriting Systems, Journal of the ACM 34(1), pp. 128–143, 1987.
Y. Toyama, Counterexamples to Termination for the Direct Sum of Term Rewriting Systems, Information Processing Letters 25, pp. 141–143, 1987.
Y. Toyama, Commutativity of Term Rewriting Systems, in: Programming of Future Generation Computer II (eds. K. Fuchi and L. Kott), North-Holland, pp. 393–407, 1988.
Y. Toyama, J.W. Klop and H.P. Barendregt, Termination for the Direct Sum of Left-Linear Term Rewriting Systems, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill, Lecture Notes in Computer Science 355, pp. 477–491, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Middeldorp, A., Toyama, Y. (1991). Completeness of combinations of constructor systems. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_96
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_96
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive