Document Open Access Logo

Termination of Generalized Term Rewriting Systems

Author Salvador Lucas

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.32.pdf
  • Filesize: 0.92 MB
  • 18 pages

Document Identifiers

Author Details

Salvador Lucas
  • DSIC & VRAIN, Universitat Politècnica de València, Spain, Spain

Funding

Supported by MCIN/AEI/10.13039/501100011033 and by "ERDF A way of making Europe" (PID2021-122830OB-C42) and by the grant CIPROM/2022/6 funded by Generalitat Valenciana.

Acknowledgements

I thank the reviewers for their useful comments leading to several improvements in the paper. I also thank Raúl Gutiérrez for his comments.

Cite AsGet BibTex

Salvador Lucas. Termination of Generalized Term Rewriting Systems. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.32

Abstract

We investigate termination of Generalized Term Rewriting Systems (GTRS), which extend Conditional Term Rewriting Systems by considering replacement restrictions on selected arguments of function symbols, as in Context-Sensitive Rewriting, and conditional rewriting rules whose conditional part may include not only a mix of the usual (reachability, joinability,...) conditions, but also atoms defined by a set of definite Horn clauses. GTRS can be used to prove confluence and termination of Generalized Rewrite Theories and Maude programs. We have characterized confluence of terminating GTRS as the joinability of a finite set of conditional pairs. Since termination of GTRS is underexplored to date, this paper introduces a Dependency Pair Framework which is well-suited to automatically (dis)prove termination of GTRS.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Program Analysis
  • Reduction-Based Systems
  • Termination

Metrics

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

References

  1. Beatriz Alarcón, Raúl Gutiérrez, and Salvador Lucas. Context-sensitive dependency pairs. Inf. Comput., 208(8):922-968, 2010. URL: https://doi.org/10.1016/j.ic.2010.03.003.
  2. Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theor. Comput. Sci., 236(1-2):133-178, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  3. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  4. Roberto Bruni and José Meseguer. Semantic foundations for generalized rewrite theories. Theor. Comput. Sci., 360(1-3):386-414, 2006. URL: https://doi.org/10.1016/j.tcs.2006.04.012.
  5. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  6. Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn L. Talcott. Programming and symbolic computation in Maude. J. Log. Algebr. Meth. Program., 110, 2020. URL: https://doi.org/10.1016/j.jlamp.2019.100497.
  7. Melvin Fitting. First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science. Springer, 1996. URL: https://doi.org/10.1007/978-1-4612-2360-3.
  8. Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Proceedings, volume 3452 of Lecture Notes in Computer Science, pages 301-331. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-32275-7_21.
  9. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. Mechanizing and improving dependency pairs. J. Autom. Reasoning, 37(3):155-203, 2006. URL: https://doi.org/10.1007/s10817-006-9057-7.
  10. Raúl Gutiérrez and Salvador Lucas. Proving termination in the context-sensitive dependency pair framework. In Peter Csaba Ölveczky, editor, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers, volume 6381 of Lecture Notes in Computer Science, pages 18-34. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16310-4_3.
  11. Raúl Gutiérrez and Salvador Lucas. Function calls at frozen positions in termination of context-sensitive rewriting. In Narciso Martí-Oliet, Peter Csaba Ölveczky, and Carolyn L. Talcott, editors, Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200 of Lecture Notes in Computer Science, pages 311-330. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23165-5_15.
  12. Raúl Gutiérrez and Salvador Lucas. Automatic Generation of Logical Models with AGES. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 287-299. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_17.
  13. Raúl Gutiérrez and Salvador Lucas. Automatically Proving and Disproving Feasibility Conditions. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 416-435. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_27.
  14. Nao Hirokawa and Aart Middeldorp. Dependency pairs revisited. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004, Proceedings, volume 3091 of Lecture Notes in Computer Science, pages 249-268. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_18.
  15. Cynthia Kop and Naoki Nishida. Term rewriting with logical constraints. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, volume 8152 of Lecture Notes in Computer Science, pages 343-358. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40885-4_24.
  16. Cynthia Kop and Naoki Nishida. Constrained term rewriting tool. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 549-557. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_38.
  17. Salvador Lucas. Context-sensitive Rewriting. ACM Comput. Surv., 53(4):78:1-78:36, 2020. URL: https://doi.org/10.1145/3397677.
  18. Salvador Lucas. Using Well-Founded Relations for Proving Operational Termination. J. Autom. Reasoning, 64(2):167-195, 2020. URL: https://doi.org/10.1007/s10817-019-09514-2.
  19. Salvador Lucas. Applications and extensions of context-sensitive rewriting. Journal of Logical and Algebraic Methods in Programming, 121:100680, 2021. URL: https://doi.org/10.1016/j.jlamp.2021.100680.
  20. Salvador Lucas. Confluence of Conditional Rewriting Modulo. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 37:1-37:21, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.37.
  21. Salvador Lucas. Local confluence of conditional and generalized term rewriting systems. Journal of Logical and Algebraic Methods in Programming, 136:paper 100926, pages 1-23, 2024. URL: https://doi.org/10.1016/j.jlamp.2023.100926.
  22. Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Inf. Process. Lett., 95(4):446-453, 2005. URL: https://doi.org/10.1016/j.ipl.2005.05.002.
  23. Salvador Lucas and José Meseguer. Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Meth. Program., 85(1):67-97, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.06.001.
  24. Salvador Lucas and José Meseguer. Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Meth. Program., 86(1):236-268, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.03.003.
  25. Salvador Lucas, José Meseguer, and Raúl Gutiérrez. The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci., 96:74-106, 2018. URL: https://doi.org/10.1016/j.jcss.2018.04.002.
  26. Salvador Lucas, José Meseguer, and Raúl Gutiérrez. The 2D Dependency Pair Framework for Conditional Rewrite Systems. Part II: Advanced Processors and Implementation Techniques. J. Autom. Reasoning, 64(8):1611-1662, 2020. URL: https://doi.org/10.1007/s10817-020-09542-3.
  27. Elliott Mendelson. Introduction to mathematical logic (4. ed.). Chapman and Hall, 1997. Google Scholar
  28. Enno Ohlebusch. Termination of logic programs: Transformational methods revisited. Appl. Algebra Eng. Commun. Comput., 12(1/2):73-116, 2001. URL: https://doi.org/10.1007/s002000100064.
  29. Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. URL: https://doi.org/10.1007/978-1-4757-3661-8.
  30. Dag Prawitz. Natural deduction. A proof theoretical study. Stockholm Studies in Philosophy. Almqvist & Wiksell, 1965. Google Scholar
  31. John Alan Robinson. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM, 12(1):23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
  32. Felix Schernhammer and Bernhard Gramlich. Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Log. Algebraic Methods Program., 79(7):659-688, 2010. URL: https://doi.org/10.1016/j.jlap.2009.08.001.
  33. Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2003. Google Scholar
  34. Yoshihito Toyama and Michio Oyamaguchi. Church-rosser property and unique normal form property of non-duplicating term rewriting systems. In Nachum Dershowitz and Naomi Lindenstrauss, editors, Conditional and Typed Rewriting Systems, 4th International Workshop, CTRS-94, Jerusalem, Israel, July 13-15, 1994, Proceedings, volume 968 of Lecture Notes in Computer Science, pages 316-331. Springer, 1994. URL: https://doi.org/10.1007/3-540-60381-6_19.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact