Document Open Access Logo

Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk)

Author Cynthia Kop

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2022.1.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Termination
  • Modularity
  • Higher-order term rewriting
  • Dependency Pairs
  • Algebra Interpretations

Metrics

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

Abstract

This paper discusses a number of methods to prove termination of higher-order term rewriting systems, with a particular focus on large systems. In first-order term rewriting, the dependency pair framework can be used to split up a large termination problem into multiple (much) smaller components that can be solved individually. This is important because a large problem may take exponentially longer to solve in one go than solving each of its components.
Unfortunately, while there are higher-order versions of several of these methods, they often fail to simplify a problem enough. Here, we will explore some of these techniques and their limitations, and discuss what else can be done to incrementally build a termination proof for higher-order systems.

Cite As Get BibTex

Cynthia Kop. Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk). In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.1

Author Details

Cynthia Kop
  • Department of Software Science, Radboud University Nijmegen, The Netherlands

Funding

The author is supported by the NWO TOP project "ICHOR", NWO 612.001.803/7571 and the NWO VIDI project "CHORPE", NWO VI.Vidi.193.075.

References

  1. T. Aoto and Y. Yamada. Dependency pairs for simply typed term rewriting. In Proc. RTA '05, volume 3467 of LNCS, pages 120-134, 2005. Google Scholar
  2. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1-2):133-178, 2000. Google Scholar
  3. F. Blanqui. Termination and confluence of higher-order rewrite systems. In Proc. RTA '00, volume 1833 of LNCS, pages 47-61, 2000. Google Scholar
  4. F. Blanqui, J. Jouannaud, and M. Okada. Inductive-data-type systems. Theoretical Computer Science, 272(1-2):41-68, 2002. Google Scholar
  5. F. Blanqui, J. Jouannaud, and A. Rubio. The computability path ordering: The end of a quest. In Proc. CSL '08, volume 5213 of LNCS, pages 1-14, 2008. Google Scholar
  6. F. Blanqui, J. Jouannaud, and A. Rubio. The computability path ordering. Logical Methods in Computer Science, 11(4), 2015. Google Scholar
  7. C. Borralleras, S. Lucas, A. Oliveras, E. Rodríguez-Carbonell, and A. Rubio. SAT modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning, 48(1):107-131, 2012. Google Scholar
  8. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl. SAT solving for termination analysis with polynomial interpretations. In Proc. SAT '07, volume 4501 of LNCS, pages 340-354. Springer, 2007. Google Scholar
  9. C. Fuhs and C. Kop. Harnessing first order termination provers using higher order dependency pairs. In Proc. FroCoS '11, volume 6989 of LNAI, pages 147-162, 2011. Google Scholar
  10. C. Fuhs and C. Kop. Polynomial interpretations for higher-order rewriting. In Proc. RTA '12, volume 15 of LIPIcs, pages 176-192, 2012. Google Scholar
  11. C. Fuhs and C. Kop. A static higher-order dependency pair framework. In Proc. ESOP '19, volume 11423 of LNCS, pages 752-782, 2019. Google Scholar
  12. J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Proc. LPAR '04, volume 3452 of LNAI, pages 301-331, 2005. Google Scholar
  13. M. Hamana. Modular termination for second-order computation rules and application to algebraic effect handlers. Arxiv preprint arXiv:1912.03434, 2019. Google Scholar
  14. J. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proc. LICS '99, IEEE, pages 402-411, 1999. Google Scholar
  15. C. Kop. WANDA - a higher-order termination tool. In Proc. FSCD 20, volume 167 of LIPIcs, pages 36:1-36:19, 2020. Google Scholar
  16. C. Kop and F. van Raamsdonk. Dynamic dependency pairs for algebraic functional systems. Logical Methods in Computer Science, 8(2):10:1-10:51, 2012. Google Scholar
  17. C. Kop and D. Vale. Tuple interpretations for higher-order complexity. In Proc. FSCD '21, volume 195 of LIPIcs, pages 31:1-31:22. Dagstuhl, 2021. 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, 92(10):2007-2015, 2009. Google Scholar
  19. K. Kusakari and M. Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting. Applicable Algebra in Engineering, Communication and Computing, 18(5):407-431, 2007. Google Scholar
  20. J. van de Pol. Termination proofs for higher-order rewrite systems. In Proc. HOA 94, volume 816 of LNCS, pages 305-325, 1994. Google Scholar
  21. Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25(3):141-143, 1987. Google Scholar
  22. Wiki. Termination Problems DataBase (TPDB). URL: http://termination-portal.org/wiki/TPDB.
  23. Wiki. The International Termination Competition (TermComp). 2018. URL: http://termination-portal.org/wiki/Termination_Competition.
  24. A. Yamada. Multi-dimensional interpretations for termination of term rewriting. In Proc. CADE 21, volume 12699 of LNAI, pages 273-290, 2021. Google Scholar
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