Decidability of confluence and termination of monadic term rewriting systems

Abstract

Term rewriting systems where the right-hand sides of rewrite rules have height at most one are said to be monadic. These systems are a generalization of the well known monadic Thue systems. We show that termination is decidable for right-linear monadic systems but undecidable if the rules are only assumed to be left-linear. Using the Peterson-Stickel algorithm we show that confluence is decidable for right-linear monadic term rewriting systems. It is known that ground confluence is undecidable for both left-linear and rightlinear monadic systems. We consider partial results for deciding ground confluence of linear monadic systems.