Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk)
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.
Termination
Modularity
Higher-order term rewriting
Dependency Pairs
Algebra Interpretations
Theory of computation~Equational logic and rewriting
1:1-1:17
Invited Talk
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.
Cynthia
Kop
Cynthia Kop
Department of Software Science, Radboud University Nijmegen, The Netherlands
https://www.cs.ru.nl/~cynthiakop/
https://orcid.org/0000-0002-6337-2544
10.4230/LIPIcs.FSCD.2022.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.
T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1-2):133-178, 2000.
F. Blanqui. Termination and confluence of higher-order rewrite systems. In Proc. RTA '00, volume 1833 of LNCS, pages 47-61, 2000.
F. Blanqui, J. Jouannaud, and M. Okada. Inductive-data-type systems. Theoretical Computer Science, 272(1-2):41-68, 2002.
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.
F. Blanqui, J. Jouannaud, and A. Rubio. The computability path ordering. Logical Methods in Computer Science, 11(4), 2015.
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.
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.
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.
C. Fuhs and C. Kop. Polynomial interpretations for higher-order rewriting. In Proc. RTA '12, volume 15 of LIPIcs, pages 176-192, 2012.
C. Fuhs and C. Kop. A static higher-order dependency pair framework. In Proc. ESOP '19, volume 11423 of LNCS, pages 752-782, 2019.
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.
M. Hamana. Modular termination for second-order computation rules and application to algebraic effect handlers. Arxiv preprint arXiv:1912.03434, 2019.
J. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proc. LICS '99, IEEE, pages 402-411, 1999.
C. Kop. WANDA - a higher-order termination tool. In Proc. FSCD 20, volume 167 of LIPIcs, pages 36:1-36:19, 2020.
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.
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.
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.
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.
J. van de Pol. Termination proofs for higher-order rewrite systems. In Proc. HOA 94, volume 816 of LNCS, pages 305-325, 1994.
Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25(3):141-143, 1987.
Wiki. Termination Problems DataBase (TPDB). URL: http://termination-portal.org/wiki/TPDB.
http://termination-portal.org/wiki/TPDB
Wiki. The International Termination Competition (TermComp). 2018. URL: http://termination-portal.org/wiki/Termination_Competition.
http://termination-portal.org/wiki/Termination_Competition
A. Yamada. Multi-dimensional interpretations for termination of term rewriting. In Proc. CADE 21, volume 12699 of LNAI, pages 273-290, 2021.
Cynthia Kop
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode