Modularity of Confluence

9 years 10 months ago
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.
Vincent van Oostrom
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Vincent van Oostrom
Comments (0)