Abstract
We present a confluence criterion for term rewrite systems by relaxing termination requirements of Knuth and Bendix’ confluence criterion, using joinability of extended critical pairs. Because computation of extended critical pairs requires equational unification, which is undecidable, we give a sufficient condition for testing joinability automatically.
This work is supported by the Grant-in-Aids for Young Scientists (B) 22700009 and Scientific Research (B) 23300005 of the Japan Society for the Promotion of Science.
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
Aoto, T., Toyama, Y.: Persistency of confluence. Journal of Universal Computer Science 3(11), 1134–1147 (1997)
Aoto, T., Toyama, Y.: A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems. In: Proc. 22nd RTA. LIPIcs, vol. 10, pp. 91–106 (2011)
Aoto, T., Yoshida, J., Toyama, Y.: Proving Confluence of Term Rewriting Systems Automatically. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 93–102. Springer, Heidelberg (2009)
Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press (1998)
Felgenhauer, B., Zankl, H., Middeldorp, A.: Layer systems for proving confluence. In: Proc. 31st FSTTCS. LIPIcs, vol. 13, pp. 288–299 (2011)
Geser, A.: Relative Termination. PhD thesis, Universität Passau, Available as technical report 91-03 (1990)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and Disproving Termination of Higher-Order Functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
Gomi, H., Oyamaguchi, M., Ohta, Y.: On the Church-Rosser property of non-E-overlapping and strongly depth-preserving term rewriting systems. Trans. IPSJ 37(12), 2147–2160 (1996)
Gomi, H., Oyamaguchi, M., Ohta, Y.: On the Church-Rosser property of root-E-overlapping and strongly depth-preserving term rewriting systems. Trans. IPSJ 39(4), 992–1005 (1998)
Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. Journal of Automated Reasoning 47, 481–501 (2011)
Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. Journal of the ACM 27, 797–821 (1980)
Jouannaud, J.P.: Confluent and Coherent Equational Term Rewriting Systems: Application to Proofs in Abstract Data Types. In: Protasi, M., Ausiello, G. (eds.) CAAP 1983. LNCS, vol. 159, pp. 269–283. Springer, Heidelberg (1983)
Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal on Computing 15(4), 1155–1194 (1986)
Klein, D., Hirokawa, N.: Maximal completion. In: Proc. 22nd RTA. LIPIcs, vol. 10, pp. 71–80 (2011)
Klop, J.: Combinatory reduction systems. PhD thesis, Utrecht University (1980)
Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263–297 (1970)
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)
Ogawa, M.: Chew’s Theorem Revisited -Uniquely Normalizing Property of Nonlinear Term Rewriting Systems. In: Ibaraki, T., Iwama, K., Yamashita, M., Inagaki, Y., Nishizeki, T. (eds.) ISAAC 1992. LNCS, vol. 650, pp. 309–318. Springer, Heidelberg (1992)
Ohlebusch, E.: Modular properties of composable term rewriting systems. Journal of Symbolic Computation 20, 1–41 (1995)
Stump, A., Kimmell, G., Omar, R.E.H.: Type preservation as a confluence problem. In: Proc. 22nd RTA. LIPIcs, vol. 10, pp. 345–360 (2011)
TeReSe: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM 34(1), 128–143 (1987)
Toyama, Y.: Commutativity of term rewriting systems. In: Programming of Future Generation Computers II, pp. 393–407. North-Holland (1988)
van Oostrom, V.: Developing developments. Theoretical Computer Science 175(1), 159–181 (1997)
van Oostrom, V.: Confluence by Decreasing Diagrams. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 306–320. Springer, Heidelberg (2008)
Yamamoto, A.: Completeness of Extending Unification Based on Basic Narrowing. In: Fujisaki, T., Nakata, I., Tanaka, H. (eds.) Logic Programming 1988. LNCS, vol. 383, pp. 1–10. Springer, Heidelberg (1989)
Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI – A Confluence Tool. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 499–505. Springer, Heidelberg (2011)
Zankl, H., Felgenhauer, B., Middeldorp, A.: Labelings for decreasing diagrams. In: Proc. 22nd RTA. LIPIcs, pp. 377–392 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klein, D., Hirokawa, N. (2012). Confluence of Non-Left-Linear TRSs via Relative Termination. In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-28717-6_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28716-9
Online ISBN: 978-3-642-28717-6
eBook Packages: Computer ScienceComputer Science (R0)