Document Open Access Logo

An Innermost DP Framework for Constrained Higher-Order Rewriting

Authors Carsten Fuhs , Liye Guo , Cynthia Kop

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.20.pdf
  • Filesize: 0.91 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
Keywords
  • Higher-order term rewriting
  • constrained rewriting
  • innermost termination
  • call by value
  • open-world analysis
  • dependency pairs

Metrics

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

Abstract

Logically constrained simply-typed term rewriting systems (LCSTRSs) are a higher-order formalism for program analysis with support for primitive data types. The termination problem of LCSTRSs has been studied so far in the setting of full rewriting. This paper modifies the higher-order constrained dependency pair framework to prove innermost termination, which corresponds to the termination of programs under call by value. We also show that the notion of universal computability with respect to innermost rewriting can be effectively handled in the modified, innermost framework, which lays the foundation for open-world termination analysis of programs under call by value via LCSTRSs.

Cite As Get BibTex

Carsten Fuhs, Liye Guo, and Cynthia Kop. An Innermost DP Framework for Constrained Higher-Order Rewriting. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.20

Author Details

Carsten Fuhs
  • Birkbeck, University of London, UK
Liye Guo
  • Radboud University, Nijmegen, The Netherlands
Cynthia Kop
  • Radboud University, Nijmegen, The Netherlands

Funding

  • Guo, Liye: NWO VI.Vidi.193.075, project "CHORPE".
  • Kop, Cynthia: NWO VI.Vidi.193.075, project "CHORPE".

Acknowledgements

We thank the reviewers for helpful comments that allowed us to improve the presentation.

Supplementary Materials

References

  1. B. Alarcón, R. Gutiérrez, and S. Lucas. Context-sensitive dependency pairs. IC, 208(8):922-968, 2010. URL: https://doi.org/10.1016/J.IC.2010.03.003.
  2. T. Aoto and T. Yamada. Argument filterings and usable rules for simply typed dependency pairs. In S. Ghilardi and R. Sebastiani, editors, Proc. FroCoS, pages 117-132, 2009. URL: https://doi.org/10.1007/978-3-642-04222-5_7.
  3. 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.
  4. D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. In A. Biere and C. Pixley, editors, Proc. FMCAD, pages 25-32, 2009. URL: https://doi.org/10.1109/FMCAD.2009.5351147.
  5. M. Codish, C. Fuhs, J. Giesl, and P. Schneider-Kamp. Lazy abstraction for size-change termination. In C. G. Fermüller and A. Voronkov, editors, Proc. LPAR (Yogyakarta), pages 217-232, 2010. URL: https://doi.org/10.1007/978-3-642-16242-8_16.
  6. Community. Termination competition (TermCOMP). URL: https://termination-portal.org/wiki/Termination_Competition.
  7. Community. The termination problem database (TPDB). URL: https://github.com/TermCOMP/TPDB.
  8. L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In C.R. Ramakrishnan and J. Rehof, editors, Proc. TACAS, pages 337-340, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  9. 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.
  10. S. Falke and D. Kapur. A term rewriting approach to the automated termination analysis of imperative programs. In R. A. Schmidt, editor, Proc. CADE, pages 277-293, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_22.
  11. S. Falke, D. Kapur, and C. Sinz. Termination analysis of C programs using compiler intermediate languages. In M. Schmidt-Schauß, editor, Proc. RTA, pages 41-50, 2011. URL: https://doi.org/10.4230/LIPIcs.RTA.2011.41.
  12. C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke. Proving termination of integer term rewriting. In R. Treinen, editor, Proc. RTA, pages 32-47, 2009. URL: https://doi.org/10.1007/978-3-642-02348-4_3.
  13. 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.
  14. C. Fuhs, C. Kop, and N. Nishida. Verifying procedural programs via constrained rewriting induction. ACM TOCL, 18(2):14:1-14:50, 2017. URL: https://doi.org/10.1145/3060143.
  15. 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(1):3-31, 2017. URL: https://doi.org/10.1007/s10817-016-9388-y.
  16. J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for Haskell by term rewriting. ACM TOPLAS, 33(2):7:1-7:39, 2011. URL: https://doi.org/10.1145/1890028.1890030.
  17. J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs. Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs. In A. King, editor, Proc. PPDP, pages 1-12, 2012. URL: https://doi.org/10.1145/2370776.2370778.
  18. 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.
  19. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and improving dependency pairs. JAR, 37(3):155-203, 2006. URL: https://doi.org/10.1007/s10817-006-9057-7.
  20. L. Guo, K. Hagens, C. Kop, and D. Vale. Higher-order constrained dependency pairs for (universal) computability. pre-publication Arxiv copy of [Guo et al., 2024] with additional appendix. URL: https://doi.org/10.48550/arXiv.2406.19379.
  21. L. Guo, K. Hagens, C. Kop, and D. Vale. Higher-order constrained dependency pairs for (universal) computability. In R. Královič and A. Kučera, editors, Proc. MFCS, pages 57:1-57:15, 2024. URL: https://doi.org/10.4230/LIPIcs.MFCS.2024.57.
  22. 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.
  23. N. Hirokawa and A. Middeldorp. Automating the dependency pair method. IC, 199(1-2):172-199, 2005. URL: https://doi.org/10.1016/J.IC.2004.10.004.
  24. N. Hirokawa and A. Middeldorp. Tyrolean Termination Tool: techniques and features. IC, 205(4):474-511, 2007. URL: https://doi.org/10.1016/j.ic.2006.08.010.
  25. C. Kop. WANDA - a higher order termination tool (system description). In Z. M. Ariola, editor, Proc. FSCD, pages 36:1-36:19, 2020. URL: https://doi.org/10.4230/LIPICS.FSCD.2020.36.
  26. 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.
  27. C. Kop et al. The Cora analyzer. URL: https://github.com/hezzel/cora.
  28. C. Kop et al. hezzel/cora: FSCD 2025. URL: https://doi.org/10.5281/zenodo.15318964.
  29. 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.
  30. C. Kop and F. van Raamsdonk. Dynamic dependency pairs for algebraic functional systems. LMCS, 8(2), 2012. URL: https://doi.org/10.2168/LMCS-8(2:10)2012.
  31. M. R. K. Krishna 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.
  32. M. R. K. Krishna 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.
  33. M. R. K. Krishna 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.
  34. K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE Trans. Inf. Syst., E92.D(10):2007-2015, 2009. URL: https://doi.org/10.1587/transinf.E92.D.2007.
  35. 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.
  36. K. Kusakari and M. Sakai. Static dependency pair method for simply-typed term rewriting and related techniques. IEICE Trans. Inf. Syst., E92.D(2):235-247, 2009. URL: https://doi.org/10.1587/transinf.E92.D.235.
  37. C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In C. Hankin and D. Schmidt, editors, Proc. POPL, pages 81-92, 2001. URL: https://doi.org/10.1145/360204.360210.
  38. S. Lucas. Context-sensitive computations in functional and functional logic programs. JFLP, 1998(1), 1998. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-01/A98-01.html.
  39. C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl. Automated termination analysis of Java bytecode by term rewriting. In C. Lynch, editor, Proc. RTA, pages 259-276, 2010. URL: https://doi.org/10.4230/LIPIcs.RTA.2010.259.
  40. S. Suzuki, K. Kusakari, and F. Blanqui. Argument filterings and usable rules in higher-order rewrite systems. IPSJ Online Trans., 4:114-125, 2011. URL: https://doi.org/10.2197/ipsjtrans.4.114.
  41. R. Thiemann. The DP framework for proving termination of term rewriting. PhD thesis, RWTH Aachen University, Germany, 2007. URL: http://darwin.bth.rwth-aachen.de/opus3/volltexte/2007/2066/.
  42. R. Thiemann and J. Giesl. The size-change principle and dependency pairs for termination of term rewriting. AAECC, 16(4):229-270, 2005. URL: https://doi.org/10.1007/S00200-005-0179-7.
  43. J. van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering, K. Meinke, B. Möller, and T. Nipkow, editors, Proc. HOA, pages 305-325, 1993. URL: https://doi.org/10.1007/3-540-58233-9_14.
  44. F. van Raamsdonk. Translating logic programs into conditional rewriting systems. In L. Naish, editor, Proc. ICLP, pages 168-182, 1997. URL: https://doi.org/10.7551/mitpress/4299.003.0018.
  45. H. Zantema. Termination of term rewriting by semantic labelling. FI, 24(1/2):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