Modularity of Confluence

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 decreasrams 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 is flexible in that it extends to constructor-sharing term rewriting systems. We show that for term rewrite systems with extra variables, confluence is not preserved under decomposition, and discuss whether for these systems confluence is preserved under composition.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Vincent van Oostrom
• Keywords: Abstract Rewriting Systems, Automated Reasoning, CADE 2008, Term Rewrite Systems, Term Rewriting Systems