Document Open Access Logo

Compositional Confluence Criteria

Authors Kiraku Shintani , Nao Hirokawa

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2022.28.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • term rewriting
  • confluence
  • decreasing diagrams

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. In addition to them, we prove that Toyama’s parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.

Cite As Get BibTex

Kiraku Shintani and Nao Hirokawa. Compositional Confluence Criteria. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.28

Author Details

Kiraku Shintani
  • Japan Advanced Institute of Science and Technology, Ishikawa, Japan
Nao Hirokawa
  • Japan Advanced Institute of Science and Technology, Ishikawa, Japan

Funding

  • Hirokawa, Nao: JSPS KAKENHI Grant Numbers 22K11900.

Acknowledgements

We are grateful to Jean-Pierre Jouannaud, Vincent van Oostrom, and Yoshihito Toyama for their valuable comments on preliminary results of this work. We thank the reviewers for their thorough reading and suggestions, which helped us to improve the presentation.

References

  1. T. Aoto and Y. Toyama. Persistency of confluence. Journal of Universal Computer Science, 3(11):1134-1147, 1997. Google Scholar
  2. T. Aoto and Y. Toyama. A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. Logical Methods in Computer Science, 8, 2012. Google Scholar
  3. T. Aoto, J. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In Proc. 20th International Conference on Rewriting Techniques and Applications, volume 5595 of LNCS, pages 93-102, 2009. Google Scholar
  4. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  5. L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 337-340, 2008. The website of Z3 is: URL: https://github.com/Z3Prover/z3.
  6. N. Dershowitz. Open. Closed. Open. In Proc. 16th International Conference on Rewriting Techniques and Applications, volume 3467 of LNCS, pages 276-393, 2005. Google Scholar
  7. G. Dowek, G. Férey, J.-P. Jouannaud, and J. Liu. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Mathematical Structures in Computer Science, 2022. Google Scholar
  8. B. Felgenhauer, A. Middeldorp, H. Zankl, and V. van Oostrom. Layer systems for proving confluence. ACM Trans. Comput. Logic, 16(2):1-32, 2015. Google Scholar
  9. B. Felgenhauer and V. van Oostrom. Proof orders for decreasing diagrams. In Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of LIPIcs, pages 174-189, 2013. Google Scholar
  10. B. Gramlich. Confluence without termination via parallel critical pairs. In Proc. 21st International Colloquium on Trees in Algebra and Programming, volume 1059 of LNCS, pages 211-225, 1996. Google Scholar
  11. N. Hirokawa and A. Middeldorp. Decreasing diagrams and relative termination. Journal of Automated Reasoning, 47:481-501, 2011. Google Scholar
  12. N. Hirokawa and A. Middeldorp. Commutation via relative termination. In Proc. 2nd International Workshop on Confluence, pages 29-34, 2013. Google Scholar
  13. N. Hirokawa, J. Nagele, and A. Middeldorp. Cops and CoCoWeb: Infrastructure for confluence tools. In Proc. 9th International Joint Conference on Automated Reasoning, volume 10900 of LNCS (LNAI), pages 346-353, 2018. The website of COPS is: URL: https://cops.uibk.ac.at/.
  14. N. Hirokawa, J. Nagele, V. van Oostrom, and M. Oyamaguchi. Confluence by critical pair analysis revisited. In Proc. 27th International Conference on Automated Deduction, volume 11716 of LNCS, pages 319-336, 2019. Google Scholar
  15. G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797-821, 1980. Google Scholar
  16. J.-P. Jouannaud and J. Liu. From diagrammatic confluence to modularity. Theoretical Computer Science, 464:20-34, 2012. Google Scholar
  17. S. Kahrs. Confluence of curried term-rewriting systems. Journal of Symbolic Computation, 19:601-623, 1995. Google Scholar
  18. D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970. Google Scholar
  19. J. Liu and J.-P. Jouannaud. Confluence: The unifying, expressive power of locality. In Specification, Algebra, and Software, volume 8375 of LNCS, pages 337-358, 2014. Google Scholar
  20. J. Nagele, B. Felgenhauer, and A. Middeldorp. Improving automatic confluence analysis of rewrite systems by redundant rules. In Proc. 26th International Conference on Rewriting Techniques and Applications, volume 36 of LIPIcs, pages 257-268, 2015. Google Scholar
  21. M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43(2):223-243, 1942. Google Scholar
  22. E. Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. Google Scholar
  23. S. Okui. Simultaneous critical pairs and Church-Rosser property. In Proc. 9th International Conference on Rewriting Techniques and Applications, volume 1379 of LNCS, pages 2-16, 1998. URL: https://doi.org/10.1007/BFb0052357.
  24. M. Oyamaguchi and Y. Ohta. A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In Proc. 10th International Conference on Rewriting Techniques and Applications, volume 1232 of LNCS, pages 187-201, 1997. Google Scholar
  25. M. Oyamaguchi and Y. Ohta. On the Church-Rosser property of left-linear term rewriting systems. IEICE Transactions on Information and Systems, E86-D(1):131-135, 2003. Google Scholar
  26. B. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, pages 160-187, 1973. Google Scholar
  27. K. Shintani and N. Hirokawa. CoLL: A confluence tool for left-linear term rewrite systems. In Proc. 25th International Conference on Automated Deduction, volume 9195 of LNCS (LNAI), pages 127-136, 2015. Google Scholar
  28. M. Takahashi. λ-calculi with conditional rules. In Proc. International Conference on Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 406-417, 1993. Google Scholar
  29. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  30. Y. Toyama. On the Church-Rosser property of term rewriting systems. In NTT ECL Technical Report, volume No. 17672. NTT, 1981. Japanese. Google Scholar
  31. Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128-143, 1987. Google Scholar
  32. Y. Toyama. Commutativity of term rewriting systems. In Programming of Future Generation Computers II, pages 393-407. North-Holland, 1988. Google Scholar
  33. Y. Toyama. Confluence criteria based on parallel critical pair closing, March 2017. Presented at the 46th TRS Meeting: URL: https://www.trs.cm.is.nagoya-u.ac.jp/event/46thTRSmeeting/.
  34. J. van de Pol. Modularity in many-sorted term rewriting systems. Master’s thesis, Utrecht University, 1992. Google Scholar
  35. V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994. Google Scholar
  36. V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. Google Scholar
  37. V. van Oostrom. Confluence by decreasing diagrams, converted. In Proc. 19th International Conference on Rewriting Techniques and Applications, volume 5117 of LNCS, pages 306-320, 2008. Google Scholar
  38. A. Yamada, K. Kusakari, and T.Sakabe. Nagoya termination tool. In Proc. 25th International Conference on Rewriting Techniques and Applications, volume 8560 of LNCS, pages 446-475, 2014. The website of NaTT is: URL: https://www.trs.cm.is.nagoya-u.ac.jp/NaTT/.
  39. H. Zankl, B. Felgenhauer, and A. Middeldorp. CSI - a confluence tool. In Proc. 23th International Conference on Automated Deduction, volume 6803 of LNCS (LNAI), pages 499-505, 2011. Google Scholar
  40. H. Zankl, B. Felgenhauer, and A. Middeldorp. Labelings for decreasing diagrams. Journal of Automated Reasoning, 54(2):101-133, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact