TY - JOUR
T1 - Completeness of combinations of constructor systems
AU - Middeldorp, Aart
AU - Toyama, Yoshihito
N1 - Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.
PY - 1993/3
Y1 - 1993/3
N2 - A term rewriting system is called complete if it is both confluent and strongly normalising. 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 term rewriting systems. 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 normalisation.
AB - A term rewriting system is called complete if it is both confluent and strongly normalising. 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 term rewriting systems. 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 normalisation.
UR - http://www.scopus.com/inward/record.url?scp=0001643927&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0001643927&partnerID=8YFLogxK
U2 - 10.1006/jsco.1993.1024
DO - 10.1006/jsco.1993.1024
M3 - Article
AN - SCOPUS:0001643927
VL - 15
SP - 331
EP - 348
JO - Journal of Symbolic Computation
JF - Journal of Symbolic Computation
SN - 0747-7171
IS - 3
ER -