TY - GEN
T1 - Completeness of combinations of constructor systems
AU - Middeldorp, Aart
AU - Toyama, Yoshihito
N1 - Funding Information:
Tiffs paper is an abbreviated version of CWI report CS-R9059. Partially supported by ESPRIT Basic Research Action 3020, INTEGRATION.
PY - 1991
Y1 - 1991
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84976703700&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84976703700&partnerID=8YFLogxK
U2 - 10.1007/3-540-53904-2_96
DO - 10.1007/3-540-53904-2_96
M3 - Conference contribution
AN - SCOPUS:84976703700
SN - 9783540539049
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 188
EP - 199
BT - Rewriting Techniques and Applications - 4th International Conference, RTA-1991, Proceedings
A2 - Book, Ronald V.
PB - Springer Verlag
T2 - 4th International Conference on Rewriting Techniques and Applications, RTA-1991
Y2 - 10 April 1991 through 12 April 1991
ER -