Journal of Logic and Computation, Volume 10, Issue 3, pp. 437-460: Abstract.
A geometric proof of confluence by decreasing diagrams
JW Klop1, V van Oostrom2 and R de Vrijer3
1CWI, PO Box 94079, 1090 GB Amsterdam, The Netherlands, Vrije Universiteit, Department of Theoretical Computer Science, de Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands, University of Nijmegen, Department of Computer Science Toernooiveld 1, 6525 ED Nijmegen, The Netherlands, E-mail: email@example.com, 2University of Utrecht, Department of Philosophy, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands, CWI, PO Box 94079, 1090 GB Amsterdam, The Netherlands, E-mail: firstname.lastname@example.org, 3Vrije Universiteit, Department of Theoretical Computer Science, de Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands, E-mail: email@example.com
The criterion for confluence using decreasing diagrams is a generalization of several well-known 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 unsuccessful attempts to obtain a confluent diagram by tiling with elementary diagrams.
Keywords: abstract rewriting, confluence, decreasing diagram, elementary diagram