A geometric proof of confluence by decreasing diagrams


Jan Willem Klop
Vincent van Oostrom 
Roel de Vrijer


Abstract 

Recently a  new confluence criterion for confluence was found using
decreasing diagrams, as a generalization of several wellknown confluence
criteria in abstract rewriting such as the strong confluence lemma. We give a
new proof of the decreasing diagram theorem based on a geometric study of
infinite reduction diagrams, arising from unsuccesful attempts to obtain a
confluent diagram by tiling with elementary diagrams.


Contents
 
1. Introduction 
2. Abstract Reduction Systems 
3. Finite reduction diagrams 
4. Infinite reduction diagrams and towers 
5. Tree coverings of reduction diagrams 
6. Impossible tree coverings 
7. Confluence by decreasing diagrams 
8. References