Abstract
Knuth and Bendix showed that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. We show that this is still true of a rewrite system \({R_{\textit{T}}} \cup{R_{\textit{NT}}} \) such that \(R_{\textit{T}}\) is terminating and \(R_{\textit{NT}}\) is a left-linear, rank non-increasing, possibly non-terminating rewrite system. Confluence can then be reduced to the joinability of the critical pairs of \(R_{\textit{T}}\) and to the existence of decreasing diagrams for the critical pairs of \(R_{\textit{T}}\) inside \(R_{\textit{NT}}\) as well as for the rigid parallel critical pairs of \(R_{\textit{NT}}\).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Felgenhauer, B.: Rule labeling for confluence of left-linear term rewrite systems. In: IWC, pp. 23–27 (2013)
Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reasoning 47, 481–501 (2011)
Huet, G.P.: Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. J. ACM 27, 797–821 (1980)
Jouannaud, J.P., Toyama, Y.: Modular Church-Rosser modulo: The complete picture. Int. J. Software and Informatics 2, 61–75 (2008)
Jouannaud, J.P., van Oostrom, V.: Diagrammatic confluence and completion. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 212–222. Springer, Heidelberg (2009)
Klein, D., Hirokawa, N.: Confluence of non-left-linear TRSs via relative termination. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 258–273. Springer, Heidelberg (2012)
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, Elsevier (1970)
Newman, M.H.A.: On theories with a combinatorial definition of ‘equivalence’. Ann. Math. 43, 223–243 (1942)
Rosen, B.K.: Tree-manipulating systems and Church-Rosser theorems. J. ACM 20, 160–187 (1973)
Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. J. ACM 34, 128–143 (1987)
Tristan, J.B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: Proceedings of ACM SIGPLAN Conference PLDI. ACM, New York (2011)
van Oostrom, V.: Confluence by decreasing diagrams. Theor. Comput. Sci. 126, 259–280 (1994)
van Oostrom, V.: Modularity of confluence. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 348–363. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Liu, J., Dershowitz, N., Jouannaud, JP. (2014). Confluence by Critical Pair Analysis. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-08918-8_20
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08917-1
Online ISBN: 978-3-319-08918-8
eBook Packages: Computer ScienceComputer Science (R0)