Document Open Access Logo

Higher-Order Constrained Dependency Pairs for (Universal) Computability

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

PDF
Thumbnail PDF

File

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

Document Identifiers

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".

Cite AsGet 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

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.

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

Related Versions

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.
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