Document Open Access Logo

Simulating Dependency Pairs by Semantic Labeling

Authors Teppei Saito , Nao Hirokawa

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2024.13.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Term rewriting
  • Relative termination
  • Semantic labeling
  • Dependency pairs

Metrics

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

Abstract

We show that termination proofs by a version of the dependency pair method can be simulated by semantic labeling plus multiset path orders. By incorporating a flattening technique into multiset path orders the simulation result can be extended to the dependency pair method for relative termination, introduced by Iborra et al. This result allows us to improve applicability of their dependency pair method.

Cite As Get BibTex

Teppei Saito and Nao Hirokawa. Simulating Dependency Pairs by Semantic Labeling. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSCD.2024.13

Author Details

Teppei Saito
  • JAIST, Nomi, Japan
Nao Hirokawa
  • JAIST, Nomi, Japan

Funding

  • Saito, Teppei: JST SPRING Grant Number JPMJSP2102
  • Hirokawa, Nao: JSPS KAKENHI Grant Number JP22K11900

Acknowledgements

The second author is grateful to Vincent van Oostrom for his valuable questions and comments on his talk at FSCD 2021. We thank René Thiemann and Jürgen Giesl for telling us about the first correctness proof of the dependency pair method via semantic labeling. Last but certainly not least, Alfons Geser and Aart Middeldorp’s help on literature was indispensable for this work.

Supplementary Materials

References

  1. B. Alarcón, S. Lucas, and J. Meseguer. A dependency pair framework for A∨C-termination. In Proceedings of the 8th International Workshop on Rewriting Logic and its Applications, LNCS, pages 36-52, 2010. URL: https://doi.org/10.1007/978-3-642-16310-4_4.
  2. A. Almeida and M. Ayala-Rincón. Formalizing the dependency pair criterion for innermost termination. Science of Computer Programming, 195:102474, 2020. URL: https://doi.org/10.1016/j.scico.2020.102474.
  3. T. Arts. Termination by absence of infinite chains of dependency pairs. In Proc. 21st International Colloquium on Trees in Algebra and Programming, volume 1059 of LNCS, pages 196-210, 1996. URL: https://doi.org/10.1007/3-540-61064-2_38.
  4. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133-178, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  5. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  6. L. Bachmair and D. Plaisted. Associative path orderings. In Proc. 1st International Conference on Rewriting Techniques and Applications, volume 202 of LNCS, pages 241-254, 1985. URL: https://doi.org/10.1007/3-540-15976-2_11.
  7. 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. URL: https://doi.org/10.1017/S0960129511000120.
  8. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279-301, 1982. URL: https://doi.org/10.1016/0304-3975(82)90026-3.
  9. N. Dershowitz. Termination by abstraction. In Proc. 20th International Conference on Logic Programming, volume 3132 of LNCS, pages 1-18, 2004. URL: https://doi.org/10.1007/978-3-540-27775-0_1.
  10. C. Fuhs and C. Kop. A static higher-order dependency pair framework. In Proceedings of ESOP 2019, volume 11423 of LNCS, pages 752-782, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_27.
  11. A. Geser. Relative Termination. PhD thesis, Universität Passau, 1990. URL: http://vts.uni-ulm.de/docs/2012/8146/vts_8146_11884.pdf.
  12. A. Geser. Semantic labelling followed by recursive path order with status is strictly more powerful than the corresponding semantic path order. Technical report, Universität Passau, 1994. Google Scholar
  13. J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Proc. 11th International Conference on Logic Programming and Automated Reasoning, volume 3452 of LNCS (LNAI), pages 301-331, 2005. URL: https://doi.org/10.1007/978-3-540-32275-7_21.
  14. Nao Hirokawa and Aart Middeldorp. Automating the dependency pair method. Information and Computation, 199:172-199, 2005. URL: https://doi.org/10.1016/j.ic.2004.10.004.
  15. J. Iborra, N. Nishida, G. Vidal, and A. Yamada. Relative termination via dependency pairs. Journal of Automated Reasoning, 58:391-411, 2017. URL: https://doi.org/10.1007/s10817-016-9373-5.
  16. J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proc. 14th Symposium on Logic in Computer Science, pages 402-411, 1999. URL: https://doi.org/10.1109/LICS.1999.782635.
  17. S. Kamin and J.J. Lévy. Two generalizations of the recursive path ordering. Technical report, University of Illinois, 1980. Unpublished manuscript. Google Scholar
  18. K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE Transactions on Information and Systems, E92.D(10):2007-2015, 2009. URL: https://doi.org/10.1587/transinf.E92.D.2007.
  19. A. Middeldorp, H. Ohsaki, and H. Zantema. Transforming termination by self-labelling. In Proc. 13th International Conference on Automated Deduction, volume 1104 of LNCS, pages 373-387, 1996. URL: https://doi.org/10.1007/3-540-61511-3_101.
  20. H. Ohsaki, A. Middeldorp, and J. Giesl. Equational termination by semantic labelling. In Proc. 14th Annual Conference of the European Association for Computer Science Logic, volume 1862 of LNCS, pages 457-471, 2000. URL: https://doi.org/10.1007/3-540-44622-2_31.
  21. Albert Rubio. A fully syntactic AC-RPO. Information and Computation, 178(2):515-533, 2002. URL: https://doi.org/10.1006/inco.2002.3158.
  22. C. Sternagel and R. Thiemann. Signature extensions preserve termination - an alternative proof via dependency pairs. In Proc. 19th Annual Conference of the European Association for Computer Science Logic, volume 6247 of LNCS, pages 514-528, 2010. Google Scholar
  23. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  24. Termination Community. The Termination Problem Database (TPDB). https://github.com/TermCOMP/TPDB. Accessed: 05.12.2023.
  25. R. Thiemann, G. Allais, and J. Nagele. On the formalization of termination techniques based on multiset orderings. In Proc. 23rd International Conference on Rewriting Techniques and Applications, volume 15 of LIPIcs, pages 339-354, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.339.
  26. R. Thiemann, J. Schöpf, C. Sternagel, and A. Yamada. Certifying the weighted path order. In Proc. 5th International Conference on Formal Structures on Computation and Deduction, volume 167 of LIPIcs, pages 4:1-4:20, 2020. URL: https://doi.org/10.4230/LIPICS.FSCD.2020.4.
  27. A. Yamada, C. Sternagel, R. Thiemann, and K. Kusakari. AC dependency pairs revisited. In Proc. 25th Annual Conference of the European Association for Computer Science Logic, volume 62 of LIPIcs, pages 8:1-8:16, 2016. URL: https://doi.org/10.4230/LIPICS.CSL.2016.8.
  28. H. Zankl, B. Felgenhauer, and A. Middeldorp. Labelings for decreasing diagrams. Journal of Automated Reasoning, 54(2):101-133, 2015. URL: https://doi.org/10.1007/S10817-014-9316-Y.
  29. H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89-105, 1995. URL: https://doi.org/10.3233/FI-1995-24124.
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