Abstract
The decreasing diagrams technique is a complete method to reduce confluence of a rewrite relation to local confluence. Whereas previous presentations have focussed on the proof the technique is correct, here we focus on applicability. We present a simple but powerful generalisation of the technique, requiring peaks to be closed only by conversions instead of valleys, which is demonstrated to further ease applicability.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. PhD thesis. Vrije Universiteit, Amsterdam (March 1994)
van Oostrom, V.: Confluence by decreasing diagrams. Theoretical Computer Science 126(2), 259–280 (1994)
Winkler, F., Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth–Bendix algorithm. In: Algebra, Combinatorics and Logic in Computer Science, Györ (Hungary) (1983) Colloquia Mathematica Societatis János Bolyai, 42, vol. II, North-Holland, Amsterdam (1986)
Newman, M.: On theories with a combinatorial definition of “equivalence”. Annals of Mathematics 43(2), 223–243 (1942)
Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)
Terese,: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)
van Oostrom, V.: Random descent. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 314–328. Springer, Heidelberg (2007)
Bezem, M., Klop, J., van Oostrom, V.: Diagram techniques for confluence. Information and Computation 141(2), 172–204 (1998)
Klop, J., van Oostrom, V., de Vrijer, R.: A geometric proof of confluence by decreasing diagrams. Journal of Logic and Computation 10(3), 437–460 (2000)
Geser, A.: Relative Termination. PhD thesis, Universität Passau (1990)
Klop, J.: Term rewriting systems. In: Handbook of Logic in Computer Science. Background: Computational Structures, vol. 2, pp. 1–116. Oxford Science Publications (1992)
Pous, D.: New up-to techniques for weak bisimulation. Theoretical Computer Science 380(1-2), 164–180 (2007)
Gramlich, B., Lucas, S.: Generalizing Newman’s lemma for left-linear rewrite systems. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 66–80. Springer, Heidelberg (2006)
Dehornoy, P.: Braids and Self-Distributivity. Progress in Mathematics, vol. 192. Birkhäuser, Basel (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Oostrom, V. (2008). Confluence by Decreasing Diagrams. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)