Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract)

ABSTRACT. This paper briefly sketches that "non-E"-overlapping and weakly-shallow TRSs are confluent" by extending reduction graph in our previous work (M.Sakai and M.Ogawa. Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent. Information Processing Letters vol.110, 2010) by introducing constructor expansion. A term is weakly shallow if each defined function symbol appears either at the root or in the ground subterms, and a TRS is weakly shallow if the both sides of rules are weakly shallow. The non-E-overlapping property is undecidable for weakly shallow TRSs and a decidable sufficient condition is the strongly non-overlapping condition. A Turing machine can be simulated by a weakly shallow TRS (p.27 in J.W.Klop, Term Rewriting Systems, 1993); thus the word problem is undecidable,in contrast to shallow TRSs.