A geometric proof of confluence by decreasing diagrams

The criterion for confluence using decreasing diagrams is a generalization of several well-known confluence criteria act 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 unsuccessful attempts to obtain a confluent diagram by tiling with elementary diagrams.

• Type: Journal
• Year: 2000
• Where: LOGCOM
• Authors: Jan Willem Klop, Vincent van Oostrom, Roel C. de Vrijer
• Keywords: Diagrams, LOGCOM 2000, Strong Confluence Lemma, Well-known Confluence Criteria