Modularity of Confluence

Constructed


We present a novel proof of Toyama's famous modularity of confluence result for term rewriting systems. Apart from being short and intuitive, the proof is modular itself in that it factors through the decreasing diagrams technique for abstract rewriting systems, is constructive in that it gives a construction for the converging rewrite sequences given a pair of diverging rewrite sequences, and general in that it extends to opaque constructor-sharing term rewriting systems. We show that for term rewrite systems with extra variables, confluence is not preserved under de composition, and discuss whether for these systems confluence is preserved under composition.