Document Open Access Logo

T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations

Authors Raphael Douglas Giles , Vincent Jackson , Christine Rizkallah

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.139.pdf
  • Filesize: 0.84 MB
  • 19 pages

Document Identifiers

Author Details

Raphael Douglas Giles
  • The University of Melbourne, Australia
Vincent Jackson
  • The University of Melbourne, Australia
Christine Rizkallah
  • The University of Melbourne, Australia

Cite AsGet BibTex

Raphael Douglas Giles, Vincent Jackson, and Christine Rizkallah. T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 139:1-139:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.139

Abstract

We introduce a powerful termination algorithm for structurally recursive functions that improves on the core ideas behind lexicographic termination algorithms for functional programs. The algorithm generates linear-lexicographic combinations of primitive measure functions measuring the recursive structure of terms. We introduce a measure language that enables the simplification and comparison of measures and we prove meta-theoretic properties of our measure language. Moreover, we demonstrate our algorithm, on an untyped first-order functional language and prove its soundness and that it runs in polynomial time. We also provide a Haskell implementation. As part of this work, we also show how to solve the maximisation of negative vector-components as a linear program.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
Keywords
  • Termination
  • Recursive functions

Metrics

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

Supplementary Materials

References

  1. Andreas Abel. Termination checking with types. RAIRO - Theoretical Informatics and Applications, 38(4):277-319, 2004. URL: https://doi.org/10.1051/ita:2004015.
  2. Andreas Abel and Thorsten Altenkirch. A predicative analysis of structural recursion. Journal of Functional Programming, 12(1):1-41, 2002. URL: https://doi.org/10.1017/S0956796801004191.
  3. Wilhelm Ackermann. Zum hilbertschen aufbau der reellen zahlen. Mathematische Annalen, 99:118-133, 1928. URL: https://api.semanticscholar.org/CorpusID:123431274.
  4. Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotnỳ. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proceedings of the ACM on Programming Languages, 2(POPL):1-32, 2017. Google Scholar
  5. Bengt Aspvall and Richard E Stone. Khachiyan’s linear programming algorithm. Journal of Algorithms, 1(1):1-13, 1980. URL: https://doi.org/10.1016/0196-6774(80)90002-4.
  6. Amir M Ben-Amram and Samir Genaim. Ranking functions for linear-constraint loops. Journal of the ACM (JACM), 61(4):1-55, 2014. Google Scholar
  7. Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow. Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics, volume 4732, pages 38-53. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. ISSN: 0302-9743, 1611-3349 Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-540-74591-4_5.
  8. Alonzo Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58:354-363, 1936. Google Scholar
  9. Raphael Douglas Giles and Vincent Jackson. T-Rex. Software, version 1.0.0., swhId: https://archive.softwareheritage.org/swh:1:dir:c7dd8ada9bdd696f86cd11bc6751817ed37ad120;origin=https://github.com/vjackson725/term_check;visit=swh:1:snp:07ec14cdddac6edf61e39a952fb12b8ead2016a7;anchor=swh:1:rev:febbde1e4ad3af86aa44f97ce5cabcde2e23f594 (visited on 2024-06-18). URL: https://github.com/vjackson725/term_check.
  10. R. W. Floyd. Assigning meaning to programs. In J. T. Schwartz, editor, Mathematical aspects of computer science: Proc. American Mathematics Soc. symposia, volume 19, pages 19-31, Providence RI, 1967. American Mathematical Society. Google Scholar
  11. Jürgen Giesl. Automated termination proofs with measure functions. In Ipke Wachsmuth, Claus-Rainer Rollinger, and Wilfried Brauer, editors, KI-95: Advances in Artificial Intelligence, pages 149-160, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-60343-3_33.
  12. Pierre Hyvernat. The size-change termination principle for constructor based languages. Log. Methods Comput. Sci., 10(1), 2014. URL: https://doi.org/10.2168/LMCS-10(1:11)2014.
  13. Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A Whiteland, and James Worrell. What’s decidable about linear loops? Proceedings of the ACM on Programming Languages, 6(POPL):1-25, 2022. Google Scholar
  14. Shmuel M. Katz and Zohar Manna. A closer look at termination. Acta Informatica, 5(4):333-352, December 1975. Google Scholar
  15. Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, and Jürgen Giesl. Termination of Isabelle functions via termination of rewriting. In Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving, pages 152-167, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-22863-6_13.
  16. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 81-92, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/360204.360210.
  17. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Number 2283 in Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  18. Rozsa Peter. Über die verallgemeinerung der theorie der rekursiven funktionen für abstrakte mengen geeigneter struktur als definitionsbereiche. Acta Mathematica Academiae Scientiarum Hungaricae, 12:271-314, 1962. URL: https://api.semanticscholar.org/CorpusID:121988998.
  19. Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 239-251. Springer, 2004. Google Scholar
  20. Ashish Tiwari. Termination of linear programs. In Rajeev Alur and Doron A. Peled, editors, Computer Aided Verification, pages 70-82, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  21. Alan M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42:230-265, 1936. Google Scholar
  22. Christoph Walther. Argument-bounded algorithms as a basis for automated termination proofs. In Ewing Lusk and Ross Overbeek, editors, 9th International Conference on Automated Deduction, pages 602-621, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact