Document Open Access Logo

WANDA - a Higher Order Termination Tool (System Description)

Author Cynthia Kop

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2020.36.pdf
  • Filesize: 0.65 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • higher-order term rewriting
  • termination
  • automatic analysis
  • dependency pair framework
  • higher-order recursive path ordering

Metrics

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

Abstract

Wanda is a fully automatic termination analysis tool for higher-order term rewriting. In this paper, we will discuss the methodology used in Wanda. Most pertinently, this includes a higher-order dependency pair framework and a variation of the higher-order recursive path ordering, as well as some non-termination analysis techniques and delegation to a first-order tool. Additionally, we will discuss Wanda’s internal rewriting formalism, and how to use Wanda in practice for systems in two different formalisms. We also present experimental results that consider both formalisms.

Cite As Get BibTex

Cynthia Kop. WANDA - a Higher Order Termination Tool (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.36

Author Details

Cynthia Kop
  • Radboud University, The Netherlands

Funding

The author is supported by the NWO TOP project "ICHOR", NWO 612.001.803/7571.

Acknowledgements

Thanks go to Carsten Fuhs both for proof-reading and for creating a customised version of AProVE which gives an explicit example term for non-termination; to Julian Nagele for using CSIasciicircum ho to translate the pattern HRSs in COPS to AFSMs; and to the anonymous reviewers of FSCD 2020 whose thorough feedback helped to improve the paper.

Supplementary Materials

References

  1. P. Aczel. A general Church-Rosser theorem, 1978. Unpublished Manuscript, University of Manchester. URL: http://www.ens-lyon.fr/LIP/REWRITING/MISC/AGeneralChurch-RosserTheorem.pdf.
  2. T. Aoto and Y. Yamada. Argument filterings and usable rules for simply typed dependency pairs. In Proceedings of FroCoS, volume 5749 of LNAI, pages 117-132. Springer, 2009. Google Scholar
  3. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1-2):133-178, 2000. Google Scholar
  4. F. Blanqui. HOT - an automated termination prover for higher-order rewriting. URL: http://rewriting.gforge.inria.fr/hot.html.
  5. F. Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. In Proceedings of RTA, volume 3091 of LNCS, pages 24-39. Springer, 2004. Google Scholar
  6. F. Blanqui, J. Jouannaud, and M. Okada. Inductive-data-type systems. Theoretical Computer Science, 272(1-2):41-68, 2002. Google Scholar
  7. F. Blanqui, J. Jouannaud, and A. Rubio. The computability path ordering: The end of a quest. In Proceedings of CSL, volume 5213 of LNCS, pages 1-14. Springer, 2008. Google Scholar
  8. C. Borralleras and A. Rubio. THOR - an automatic tool for proving termination of higher-order rewriting. URL: https://www.cs.upc.edu/~albert/term.html.
  9. C. Borralleras and A. Rubio. A monotonic higher-order semantic path ordering. In Proceedings of LPAR, volume 2250 of LNAI, pages 531-547. Springer, 2001. Google Scholar
  10. Community. Confluence Problems (COPS). URL: https://cops.uibk.ac.at/?q=prs.
  11. Community. The international Confluence Competition (CoCo). URL: http://coco.nue.riec.tohoku.ac.jp/.
  12. Community. Termination Portal. URL: http://www.termination-portal.org/wiki/Termination_Competition.
  13. Community. Termination Problem DataBase (TPDB). URL: http://termination-portal.org/wiki/TPDB.
  14. N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279-301, 1982. Google Scholar
  15. J. Doménech, S. Genaim, E.B. Johnsen, and R. Schlatte. EasyInterface: A toolkit for rapid development of GUIs for research prototype tools. In Proceedings of FASE, volume 10202 of LNCS, pages 379-383. Springer, 2017. Google Scholar
  16. N. Eén and N. Sörensson. An extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT '03), volume 2919 of LNCS, pages 502-518. Springer, 2004. See also URL: http://minisat.se/.
  17. F. Emmes, T. Enger, and J. Giesl. Proving non-looping non-termination automatically. In Proceedings of IJCAR, volume 7364 of LNAI, pages 225-240. Springer, 2012. Google Scholar
  18. M. Ferreira and H. Zantema. Syntactical analysis of total termination. In Proceedings of ALP, volume 850 of LNCS, pages 204-222. Springer, 1994. Google Scholar
  19. C. Fuhs, J. Giesl, M. Parting, P. Schneider-Kamp, and S. Swiderski. Proving termination by dependency pairs and inductive theorem proving. Journal of Automated Reasoning, 47(2):133-160, 2011. Google Scholar
  20. C. Fuhs and C. Kop. Harnessing first order termination provers using higher order dependency pairs. In Proceedings of FroCoS, volume 6989 of LNAI, pages 147-162. Springer, 2011. Google Scholar
  21. C. Fuhs and C. Kop. Polynomial interpretations for higher-order rewriting. In Proceedings of RTA, volume 15 of LIPIcs, pages 176-192. Dagstuhl, 2012. Google Scholar
  22. C. Fuhs and C. Kop. A static higher-order dependency pair framework. In Proceedings of ESOP, volume 11423 of LNCS, pages 752-782, 2019. Google Scholar
  23. G. Genestier. SizeChangeTool: A termination checker for rewriting dependent types. In Proceedings of HOR, pages 14-19, 2019. URL: https://hal.archives-ouvertes.fr/hal-02442465/document.
  24. 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. Journal of Automated Reasoning, 58(1):3-31, 2017. Google Scholar
  25. J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Proceedings of LPAR, volume 3452 of LNAI, pages 301-331. Springer, 2005. Google Scholar
  26. J. Giesl, R. Thiemann, and P. Schneider-Kamp. Proving and disproving termination of higher-order functions. In Proceedings of FroCoS, volume 3717 of LNAI, pages 216-231. Springer, 2005. Google Scholar
  27. B. Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, 24(1-2):3-23, 1995. Google Scholar
  28. M. Hamana. PolySOL - an automatic tool for confluence and termination of polymorphic second-order systems. URL: http://www.cs.gunma-u.ac.jp/hamana/polysol/.
  29. J. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proceedings of LICS, IEEE, pages 402-411, 1999. Google Scholar
  30. S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering, 1980. Unpublished Manuscript, University of Illinois. Google Scholar
  31. D. Kapur, P. Musser, D. Narendran, and J. Stillman. Semi-unification. In Proceedings of FSTTCS, volume 338 of LNCS, pages 435-454, 1988. Google Scholar
  32. J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121(1-2):279-308, 1993. Google Scholar
  33. J.W. Klop, V. van Oostrom, and R. de Vrijer. Iterative lexicographic path orders. In Essays dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday, volume 4060 of LNCS, pages 541-554. Springer, 2006. Festschrift. Google Scholar
  34. C. Kop. Simplifying algebraic functional systems. In Proceedings of CAI, volume 6742 of LNCS, pages 201-215. Springer, 2011. Google Scholar
  35. C. Kop. Higher Order Termination. PhD thesis, VU University Amsterdam, 2012. Google Scholar
  36. C. Kop and F. van Raamsdonk. A higher-order iterative path ordering. In Proceedings of LPAR, volume 5330 of LNAI, pages 697-711, 2008. Google Scholar
  37. 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. Special Issue for RTA '11. Google Scholar
  38. 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
  39. K. Kusakari, M. Nakamura, and Y. Toyama. Argument filtering transformation. In Proceedings of PPDP, volume 1702 of LNCS, pages 47-61. Springer, 1999. Google Scholar
  40. S. Lucas, C. Marché, and J. Meseguer. Operational termination of conditional term rewriting systems. Information Processing letters, 95(4):446-453, 2005. Google Scholar
  41. D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497-536, 1991. Google Scholar
  42. J. Nagele. CoCo 2016 participant: CSIasciicircum ho 0.2. ; tool webpage: http://cl-informatik.uibk.ac.at/software/csi/ho/. URL: http://coco.nue.riec.tohoku.ac.jp/2016/papers/csiho.pdf.
  43. T. Nipkow. Higher-order critical pairs. In Proceedings of LICS, pages 342-349. IEEE, 1991. Google Scholar
  44. K. Onozawa, K. Kikuchi, T. Aoto, and Y. Toyama. ACPH: System description for CoCo 2016. URL: http://coco.nue.riec.tohoku.ac.jp/2016/papers/acph.pdf.
  45. É. Payet. Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science, 403(2-3):307-327, 2008. Google Scholar
  46. É. Payet. Guided unfoldings for finding loops in standard term rewriting. In Proceedings of LOPSTR, volume 11408 of LNCS, pages 22-37, 2018. Google Scholar
  47. J.C. van de Pol. Termination of Higher-order Rewrite Systems. PhD thesis, University of Utrecht, 1996. Google Scholar
  48. R. Thiemann, G. Allais, and J. Nagele. On the formalization of termination techniques based on multiset orderings. In Proceedings of RTA, volume 15 of LIPIcs, pages 339-354. Dagstuhl, 2012. Google Scholar
  49. R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In Proceedings of TPHOLs, volume 5674 of LNCS, pages 452-468. Springer, 2009. Google Scholar
  50. Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25(1):141-143, 1987. Google Scholar
  51. H. Zantema. Termination of context-sensitive rewriting. In Proceedings of RTA, volume 1232 of LNCS, pages 172-186, 1997. 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