Document Open Access Logo

Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules

Authors Julian Nagele, Bertram Felgenhauer, Aart Middeldorp

PDF

File

Thumbnail PDF
PDF
LIPIcs.RTA.2015.257.pdf
  • Filesize: 0.51 MB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • term rewriting
  • confluence
  • automation
  • transformation

Metrics

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

Abstract

We describe how to utilize redundant rewrite rules, i.e., rules that can be simulated by other rules, when (dis)proving confluence of term rewrite systems. We demonstrate how automatic confluence provers benefit from the addition as well as the removal of redundant rules. Due to their simplicity, our transformations were easy to formalize in a proof assistant and are thus amenable to certification. Experimental results show the surprising gain in power.

Cite As Get BibTex

Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 257-268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.257

Author Details

Julian Nagele
Bertram Felgenhauer
Aart Middeldorp

References

  1. T. Aoto. Disproving confluence of term rewriting systems by interpretation and ordering. In P. Fontaine, editor, Proc. 9th International Workshop on Frontiers of Combining Systems, volume 8152 of Lecture Notes in Artificial Intelligence, pages 311-326, 2013. doi: family \doi10.1007/978-3-642-40885-4_22. 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(1:31):1-29, 2012. doi: family \doi10.2168/LMCS-8(1:31)2012. Google Scholar
  3. T. Aoto, J. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In R. Treinen, editor, Proc. 20th International Conference on Rewriting Techniques and Applications, volume 5595 of Lecture Notes in Computer Science, pages 93-102, 2009. doi: family \doi10.1007/978-3-642-02348-4_7. Google Scholar
  4. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  5. F. Blanqui and A. Koprowski. CoLoR, a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Mathematical Structures in Computer Science, 21(4):827-859, 2011. doi: family \doi10.1017/S0960129511000120. Google Scholar
  6. E. Contejean, P. Courtieu, J. Forest, O. Pons, and Xavier Urbain. Automated certified proofs with CiME3. In M. Schmidt-Schauß, editor, Proc. 22nd International Conference on Rewriting Techniques and Applications, pages 21-30, 2011. doi: family \doi10.4230/LIPIcs.RTA.2011.21. Google Scholar
  7. B. Felgenhauer. A proof order for decreasing diagrams. In N. Hirokawa and A. Middeldorp, editors, Proc. 1st International Workshop on Confluence, pages 7-14, 2012. URL: http://cl-informatik.uibk.ac.at/events/iwc-2012/.
  8. B. Felgenhauer and R. Thiemann. Reachability analysis with state-compatible automata. In A.-H. Dediu, editor, Proc. 8th International Conference on Language and Automata Theory and Applications, volume 8370 of Lecture Notes in Computer Science, pages 347-359, 2013. doi: family \doi10.1007/978-3-319-04921-2_28. Google Scholar
  9. B. Gramlich. Simplifying termination proofs for rewrite systems by preprocessing. In F. Pfenning, editor, Proc. 2nd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 139-150, 2000. doi: family \doi10.1145/351268.351286. Google Scholar
  10. B. Gramlich and S. Lucas. Generalizing Newman’s lemma for left-linear rewrite systems. In F. Pfenning, editor, Proc. 17th International Conference on Rewriting Techniques and Applications, volume 4098 of Lecture Notes in Computer Science, pages 66-80, 2006. doi: family \doi10.1007/11805618_6. Google Scholar
  11. N. Hirokawa and D. Klein. Saigawa: A confluence tool. In N. Hirokawa and A. Middeldorp, editors, Proc. 1st International Workshop on Confluence, page 49, 2012. URL: http://cl-informatik.uibk.ac.at/events/iwc-2012/.
  12. N. Hirokawa and A. Middeldorp. Decreasing diagrams and relative termination. Journal of Automated Reasoning, 47(4):481-501, 2011. doi: family \doi10.1007/s10817-011-9238-x. Google Scholar
  13. G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797-821, 1980. doi: family \doi10.1145/322217.322230. Google Scholar
  14. D. Klein and N. Hirokawa. Confluence of non-left-linear TRSs via relative termination. In N. Bjørner and A. Voronkov, editors, Proc. 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 7180 of Lecture Notes in Computer Science (Advanced Research in Computing and Software Science), pages 258-273, 2012. Google Scholar
  15. 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
  16. J. Nagele and R. Thiemann. Certification of confluence proofs using CeTA. In T. Aoto and D. Kesner, editors, Proc. 3rd International Workshop on Confluence, pages 19-23, 2014. URL: http://www.nue.riec.tohoku.ac.jp/iwc2014/.
  17. J. Nagele and H. Zankl. Certified rule labeling. In M. Fernández, editor, Proc. 26th International Conference on Rewriting Techniques and Applications, volume 36 of Leibniz International Proceedings in Informatics, 2015. This volume. Google Scholar
  18. S. Okui. Simultaneous critical pairs and Church-Rosser property. In T. Nipkow, editor, Proc. 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 2-16, 1998. doi: family \doi10.1007/BFb0052357. Google Scholar
  19. V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. doi: family \doi10.1016/S0304-3975(96)00173-9. Google Scholar
  20. V. van Oostrom. Confluence by decreasing diagrams - converted. In A. Voronkov, editor, Proc. 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 306-320, 2008. doi: family \doi10.1007/978-3-540-70590-1_21. Google Scholar
  21. V. van Oostrom. Feebly not weakly. In Proc. 7th International Workshop on Higher-Order Rewriting, Vienna Summer of Logic flash drive, 2014. Google Scholar
  22. B.K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, 20(1):160-187, 1973. doi: family \doi10.1145/321738.321750. Google Scholar
  23. C. Sternagel and R. Thiemann. The certification problem format. In G. Klein and R. Gamboa, editors, Proc. 11th International Workshop on User Interfaces for Theorem Provers, volume 167 of Electronic Proceedings in Theoretical Computer Science, pages 61-72, 2014. doi: family \doi10.4204/EPTCS.167.8. Google Scholar
  24. T. Suzuki, T. Aoto, and Y. Toyama. Confluence proofs of term rewriting systems based on persistency. Computer Software, 30(3):148-162, 2013. In Japanese, doi: family \doi10.11309/jssst.30.3_148. Google Scholar
  25. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  26. R. Thiemann. Certification of confluence proofs using CeTA. In N. Hirokawa and A. Middeldorp, editors, Proc. 1st International Workshop on Confluence, page 45, 2012. URL: http://cl-informatik.uibk.ac.at/events/iwc-2012/.
  27. R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In S. Berghofer, editor, Proc. 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 452-468, 2009. doi: family \doi10.1007/978-3-642-03359-9_31. Google Scholar
  28. Y. Toyama. Commutativity of term rewriting systems. In K. Fuchi and L. Kott, editors, Programming of Future Generation Computers II, pages 393-407. North-Holland, 1988. Google Scholar
  29. H. Zankl, B. Felgenhauer, and A. Middeldorp. CSI - A confluence tool. In N. Bjørner and V. Sofronie-Stokkermans, editors, Proc. 23rd International Conference on Automated Deduction, volume 6803 of Lecture Notes in Artificial Intelligence, pages 499-505, 2011. doi: family \doi10.1007/978-3-642-22438-6_38. Google Scholar
  30. H. Zantema. Reducing right-hand sides for termination. In V. van Oostrom A. Middeldorp and and F. van Raamsdonk, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of his 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 173-197, 2005. doi: family \doi10.1007/11601548_12. 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