Document Open Access Logo

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Authors Frédéric Blanqui, Guillaume Genestier, Olivier Hermant

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.9.pdf
  • Filesize: 0.59 MB
  • 21 pages

Document Identifiers

Author Details

Frédéric Blanqui
  • INRIA, France
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
Guillaume Genestier
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
  • MINES ParisTech, PSL University, Paris, France
Olivier Hermant
  • MINES ParisTech, PSL University, Paris, France

Acknowledgements

The authors thank the anonymous referees for their comments, which have improved the quality of this article.

Cite AsGet BibTex

Frédéric Blanqui, Guillaume Genestier, and Olivier Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.9

Abstract

Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous results by Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Type theory
Keywords
  • termination
  • higher-order rewriting
  • dependent types
  • dependency pairs

Metrics

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

References

  1. A. Abel. MiniAgda: integrating sized and dependent types. In Proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers, Electronic Proceedings in Theoretical Computer Science 43, 2010. URL: http://dx.doi.org/10.4204/EPTCS.43.2.
  2. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133-178, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(99)00207-8.
  3. H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of logic in computer science. Volume 2. Background: computational structures, pages 117-309. Oxford University Press, 1992. Google Scholar
  4. F. Blanqui. Théorie des types et récriture. PhD thesis, Université Paris-Sud, France, 2001. 144 pages. URL: http://tel.archives-ouvertes.fr/tel-00105522
  5. F. Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1):37-92, 2005. URL: http://dx.doi.org/10.1017/S0960129504004426.
  6. F. Blanqui. Termination of rewrite relations on λ-terms based on Girard’s notion of reducibility. Theoretical Computer Science, 611:50-86, 2016. URL: http://dx.doi.org/10.1016/j.tcs.2015.07.045.
  7. F. Blanqui. Size-based termination of higher-order rewriting. Journal of Functional Programming, 28(e11), 2018. 75 pages. URL: http://dx.doi.org/10.1017/S0956796818000072.
  8. W. N. Chin and S. C. Khoo. Calculating sized types. Journal of Higher-Order and Symbolic Computation, 14(2-3):261-300, 2001. URL: http://dx.doi.org/10.1023/A:1012996816178.
  9. T. Coquand. Pattern matching with dependent types. In Proceedings of the International Workshop on Types for Proofs and Programs, 1992. URL: http://www.lfcs.inf.ed.ac.uk/research/types-bra/proc/proc92.ps.gz
  10. D. Cousineau and G. Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 4583, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_9
  11. P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525-549, 2000. URL: http://www.jstor.org/stable/2586554
  12. G. Genestier. SizeChangeTool, 2018. URL: https://github.com/Deducteam/SizeChangeTool
  13. J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: combining techniques for automated termination proofs. In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science 3452, 2004. URL: http://dx.doi.org/10.1007/978-3-540-32275-7_21.
  14. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37(3):155-203, 2006. URL: http://dx.doi.org/10.1007/s10817-006-9057-7.
  15. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and types. Cambridge University Press, 1988. URL: http://www.paultaylor.eu/stable/prot.pdf
  16. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. URL: http://dx.doi.org/10.1145/138027.138060.
  17. N. Hirokawa and A. Middeldorp. Tyrolean Termination Tool: techniques and features. Information and Computation, 205(4):474-511, 2007. URL: http://dx.doi.org/10.1016/j.ic.2006.08.010.
  18. J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Proceedings of the 23th ACM Symposium on Principles of Programming Languages, 1996. URL: http://dx.doi.org/10.1145/237721.240882.
  19. P. Hyvernat. The size-change termination principle for constructor based languages. Logical Methods in Computer Science, 10(1):1-30, 2014. URL: http://dx.doi.org/10.2168/LMCS-10(1:11)2014.
  20. P. Hyvernat and C. Raffalli. Improvements on the "size change termination principle" in a functional language. In 11th International Workshop on Termination, 2010. URL: https://lama.univ-savoie.fr/~raffalli/pdfs/wst.pdfhttps://lama.univ-savoie.fr/ raffalli/pdfs/wst.pdf.
  21. N. D. Jones and N. Bohr. Termination analysis of the untyped lambda-calculus. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 3091, 2004. URL: http://dx.doi.org/10.1007/978-3-540-25979-4_1.
  22. J.-P. Jouannaud and J. Li. Termination of Dependently Typed Rewrite Rules. In Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, Leibniz International Proceedings in Informatics 38, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.257.
  23. J. W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121:279-308, 1993. URL: http://dx.doi.org/10.1016/0304-3975(93)90091-7.
  24. C. Kop. Higher order termination. PhD thesis, VU University Amsterdam, 2012. URL: http://hdl.handle.net/1871/39346http://hdl.handle.net 39346.
  25. K. Kusakari and M. Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting systems. Applicable Algebra in Engineering Communication and Computing, 18(5):407-431, 2007. URL: http://dx.doi.org/10.1007/s00200-007-0046-9.
  26. C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages, 2001. URL: http://dx.doi.org/10.1145/360204.360210.
  27. R. Lepigre and C. Raffalli. Practical subtyping for System F with sized (co-)induction, 2017. URL: http://arxiv.org/abs/1604.01990.
  28. G. Markowsky. Chain-complete posets and directed sets with applications. Algebra Universalis, 6:53-68, 1976. Google Scholar
  29. R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(2):3-29, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(97)00143-6.
  30. C. Roux. Refinement Types as Higher-Order Dependency Pairs. In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics 10, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2011.299.
  31. R. Saillard. Type checking in the Lambda-Pi-calculus modulo: theory and practice. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180
  32. D. Sereni and N. D. Jones. Termination analysis of higher-order functional programs. In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems, Lecture Notes in Computer Science 3780, 2005. URL: http://dx.doi.org/10.1007/11575467_19.
  33. TeReSe. Term rewriting systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  34. R. Thiemann and J. Giesl. The size-change principle and dependency pairs for termination of term rewriting. Applicable Algebra in Engineering Communication and Computing, 16(4):229-270, 2005. URL: http://dx.doi.org/10.1007/s00200-005-0179-7.
  35. V. van Oostrom. Confluence for abstract and higher-order rewriting. PhD thesis, Vrije Universiteit Amsterdam, NL, 1994. URL: http://www.phil.uu.nl/~oostrom/publication/ps/phdthesis.pshttp://www.phil.uu.nl/ oostrom/publication/ps/phdthesis.ps.
  36. V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00173-9.
  37. D. Wahlstedt. Dependent type theory with first-order parameterized data types and well-founded recursion. PhD thesis, Chalmers University of Technology, Sweden, 2007. URL: http://www.cse.chalmers.se/alumni/davidw/wdt_phd_printed_version.pdf
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