Document Open Access Logo

Higher-Order Constrained Dependency Pairs for (Universal) Computability

Authors Liye Guo , Kasper Hagens , Cynthia Kop , Deivid Vale

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2024.57.pdf
  • Filesize: 0.75 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Higher-order term rewriting
  • constrained rewriting
  • dependency pairs

Metrics

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

Abstract

Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order formalism with logical constraints built in. We also propose the concept of universal computability, which enables a form of open-world termination analysis through the use of static dependency pairs.

Cite As Get BibTex

Liye Guo, Kasper Hagens, Cynthia Kop, and Deivid Vale. Higher-Order Constrained Dependency Pairs for (Universal) Computability. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 57:1-57:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.MFCS.2024.57

Author Details

Liye Guo
  • Radboud University, Nijmegen, The Netherlands
Kasper Hagens
  • Radboud University, Nijmegen, The Netherlands
Cynthia Kop
  • Radboud University, Nijmegen, The Netherlands
Deivid Vale
  • Radboud University, Nijmegen, The Netherlands

Funding

The authors are supported by NWO VI.Vidi.193.075, project "CHORPE".

Supplementary Materials

References

  1. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. TCS, 236(1-2):133-178, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  2. F. Blanqui. Higher-order dependency pairs. In A. Geser and H. Søndergaard, editors, Proc. WST, pages 22-26, 2006. URL: https://doi.org/10.48550/arXiv.1804.08855.
  3. F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-data-type systems. TCS, 272(1-2):41-68, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00347-9.
  4. F. Blanqui, J.-P. Jouannaud, and A. Rubio. The computability path ordering: the end of a quest. In M. Kaminski and S. Martini, editors, Proc. CSL, pages 1-14, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_1.
  5. Community. The termination problem database (TPDB). URL: https://github.com/TermCOMP/TPDB.
  6. N. Dershowitz. Hierarchical termination. In N. Dershowitz and N. Lindenstrauss, editors, Proc. CTRS, pages 89-105, 1995. URL: https://doi.org/10.1007/3-540-60381-6_6.
  7. C. Fuhs and C. Kop. A static higher-order dependency pair framework. In L. Caires, editor, Proc. ESOP, pages 752-782, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_27.
  8. J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Analyzing program termination and complexity automatically with AProVE. JAR, 58:3-31, 2017. URL: https://doi.org/10.1007/s10817-016-9388-y.
  9. J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: combining techniques for automated termination proofs. In F. Baader and A. Voronkov, editors, Proc. LPAR, pages 301-331, 2005. URL: https://doi.org/10.1007/978-3-540-32275-7_21.
  10. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and improving dependency pairs. JAR, 37:155-203, 2006. URL: https://doi.org/10.1007/s10817-006-9057-7.
  11. L. Guo, K. Hagens, C. Kop, and D. Vale. Higher-order constrained dependency pairs for (universal) computability. Technical report, Radboud University, 2024. URL: https://doi.org/10.48550/arXiv.2406.19379.
  12. L. Guo and C. Kop. Higher-order LCTRSs and their termination. In S. Weirich, editor, Proc. ESOP, pages 331-357, 2024. URL: https://doi.org/10.1007/978-3-031-57267-8_13.
  13. N. Hirokawa and A. Middeldorp. Dependency pairs revisited. In V. van Oostrom, editor, Proc. RTA, pages 249-268, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_18.
  14. J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In G. Longo, editor, Proc. LICS, pages 402-411, 1999. URL: https://doi.org/10.1109/LICS.1999.782635.
  15. C. Kop. Termination of LCTRSs. In J. Waldmann, editor, Proc. WST, pages 59-63, 2013. URL: https://doi.org/10.48550/arXiv.1601.03206.
  16. C. Kop. WANDA - A higher order termination tool. In Z. M. Ariola, editor, Proc. FSCD, pages 36:1-36:19, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.36.
  17. C. Kop. Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting. In A. P. Felty, editor, Proc. FSCD, pages 1:1-1:17, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.1.
  18. C. Kop. A weakly monotonic, logically constrained, HORPO-variant. Technical report, Radboud University, 2024. URL: https://doi.org/10.48550/arXiv.2406.18493.
  19. C. Kop and N. Nishida. Term rewriting with logical constraints. In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Proc. FroCoS, pages 343-358, 2013. URL: https://doi.org/10.1007/978-3-642-40885-4_24.
  20. C. Kop and D. Vale. The Cora analyzer. URL: https://github.com/hezzel/cora.
  21. C. Kop and D. Vale. hezzel/cora: artifact for MFCS 2024. URL: https://doi.org/10.5281/zenodo.12551027.
  22. C. Kop and D. Vale. Tuple interpretations for higher-order complexity. In N. Kobayashi, editor, Proc. FSCD, pages 31:1-31:22, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.31.
  23. C. Kop and F. van Raamsdonk. Dynamic dependency pairs for algebraic functional systems. LMCS, 8(2):10:1-10:51, 2012. URL: https://doi.org/10.2168/lmcs-8(2:10)2012.
  24. K. Kusakari and M. Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting. AAECC, 18(5):407-431, 2007. URL: https://doi.org/10.1007/s00200-007-0046-9.
  25. A. Matsumi, N. Nishida, M. Kojima, and D. Shin. On singleton self-loop removal for termination of LCTRSs with bit-vector arithmetic. In A. Yamada, editor, Proc. WST, 2023. URL: https://doi.org/10.48550/arXiv.2307.14094.
  26. P. W. O'Hearn. Continuous reasoning: scaling the impact of formal methods. In A. Dawar and E. Grädel, editors, Proc. LICS, pages 13-25, 2018. URL: https://doi.org/10.1145/3209108.3209109.
  27. M. R. K. K. Rao. Completeness of hierarchical combinations of term rewriting systems. In R. K. Shyamasundar, editor, Proc. FSTTCS, pages 125-138, 1993. URL: https://doi.org/10.1007/3-540-57529-4_48.
  28. M. R. K. K. Rao. Simple termination of hierarchical combinations of term rewriting systems. In M. Hagiya and J. C. Mitchell, editors, Proc. TACS, pages 203-223, 1994. URL: https://doi.org/10.1007/3-540-57887-0_97.
  29. M. R. K. K. Rao. Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, Proc. CAAP, pages 379-393, 1995. URL: https://doi.org/10.1007/3-540-59293-8_208.
  30. M. Sakai and K. Kusakari. On dependency pair method for proving termination of higher-order rewrite systems. IEICE Trans. Inf. Syst., E88-D(3):583-593, 2005. URL: https://doi.org/10.1093/ietisy/e88-d.3.583.
  31. M. Sakai, Y. Watanabe, and T. Sakabe. An extension of the dependency pair method for proving termination of higher-order rewrite systems. IEICE Trans. Inf. Syst., E84-D(8):1025-1032, 2001. URL: https://search.ieice.org/bin/summary.php?id=e84-d_8_1025.
  32. R. Tarjan. Depth-first search and linear graph algorithms. SICOMP, 1(2):146-160, 1972. URL: https://doi.org/10.1137/0201010.
  33. R. Thiemann. The DP Framework for Proving Termination of Term Rewriting. PhD thesis, RWTH Aachen University, 2007. URL: http://cl-informatik.uibk.ac.at/users/thiemann/paper/diss.pdf.
  34. J. C. van de Pol. Termination of Higher-Order Rewrite Systems. PhD thesis, Utrecht University, 1996. URL: https://www.cs.au.dk/~jaco/papers/thesis.pdf.
  35. A. Yamada. Tuple interpretations for termination of term rewriting. JAR, 66:667-688, 2022. URL: https://doi.org/10.1007/s10817-022-09640-4.
  36. H. Zantema. Termination of term rewriting: interpretation and type elimination. JSC, 17(1):23-50, 1994. URL: https://doi.org/10.1006/jsco.1994.1003.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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