Document Open Access Logo

Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus

Author Yuta Takahashi

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.12.pdf
  • Filesize: 0.91 MB
  • 23 pages

Document Identifiers

Author Details

Yuta Takahashi
  • Ochanomizu University, Tokyo, Japan

Funding

  • Takahashi, Yuta: This work is supported by JSPS KAKENHI Grant Number JP21K12822.

Acknowledgements

I want to thank Frédéric Blanqui and Ralph Matthes for valuable discussions on size-based termination and non-strictly positive inductive types, respectively. I also thank the anonymous reviewers for their comments which improved the earlier version of this paper.

Cite AsGet BibTex

Yuta Takahashi. Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.12

Abstract

So far, several typed lambda-calculus systems were combined with algebraic rewrite rules, and the termination (in other words, strong normalisation) problem of the combined systems was discussed. By the size-based approach, Blanqui formulated a termination criterion for simply typed lambda-calculus with algebraic rewrite rules which guarantees, in some specific cases, the termination of the rewrite relation induced by beta-reduction and algebraic rewrite rules on strictly or non-strictly positive inductive types. Using the inflationary fixed-point construction, we extend this termination criterion so that it is possible to show the termination of the rewrite relation induced by some rewrite rules on types which are called non-positive types. In addition, we note that a condition in Blanqui’s proof can be dropped, and this improves the criterion also for non-strictly positive inductive types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Type theory
Keywords
  • termination
  • higher-order rewriting
  • non-positive types
  • inductive types

Metrics

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

References

  1. Andreas Abel. Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, Tallinn, Estonia, 24th March 2012, pages 1-11, 2012. URL: https://doi.org/10.4204/EPTCS.77.1.
  2. Andreas Abel and Brigitte Pientka. Well-founded recursion with copatterns and sized types. J. Funct. Program., 26:e2, 2016. URL: https://doi.org/10.1017/S0956796816000022.
  3. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  4. Franco Barbanera, Maribel Fernández, and Herman Geuvers. Modularity of strong normalization in the algebraic-lambda-cube. J. Funct. Program., 7(6):613-660, 1997. URL: https://doi.org/10.1017/s095679689700289x.
  5. Gilles Barthe and Herman Geuvers. Modular properties of algebraic type systems. In Higher-Order Algebra, Logic, and Term Rewriting, Second International Workshop, HOA '95, Paderborn, Germany, September 21-22, 1995, Selected Papers, pages 37-56, 1995. URL: https://doi.org/10.1007/3-540-61254-8_18.
  6. Gilles Barthe and Femke van Raamsdonk. Termination of algebraic type systems: The syntactic approach. In Algebraic and Logic Programming, 6th International Joint Conference, ALP '97 - HOA '97, Southampton, UK, Spetember 3-5, 1997, Proceedings, pages 174-193, 1997. URL: https://doi.org/10.1007/BFb0027010.
  7. Frédéric Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1):37-92, 2005. URL: https://doi.org/10.1017/S0960129504004426.
  8. Frédéric Blanqui. Inductive types in the calculus of algebraic constructions. Fundamenta Informaticae, 65(1-2):61-86, 2005. Google Scholar
  9. Frédéric Blanqui. Size-based termination of higher-order rewriting. J. Funct. Program., 28:e11, 2018. URL: https://doi.org/10.1017/S0956796818000072.
  10. 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, June 24-30, 2019, Dortmund, Germany, pages 9:1-9:21, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.9.
  11. Frédéric Blanqui, Jean-Pierre Jouannaud, and Mitsuhiro Okada. Inductive-data-type systems. Theoretical Computer Science, 272(1):41-68, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00347-9.
  12. Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic strong normalization and confluence. In Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simonetta Ronchi Della Rocca, editors, ICALP 1989: Automata, Languages and Programming, pages 137-150, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0035757.
  13. Jesper Cockx. Type theory unchained: Extending agda with user-defined rewrite rules. In 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway, pages 2:1-2:27, 2019. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.2.
  14. Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. The taming of the rew: a type theory with computational assumptions. Proc. ACM Program. Lang., 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434341.
  15. Carsten Fuhs and Cynthia Kop. Polynomial interpretations for higher-order rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, pages 176-192, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.176.
  16. Guillaume Genestier. Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting. PhD thesis, University of Paris-Saclay, France, 2020. URL: https://tel.archives-ouvertes.fr/tel-03167579.
  17. Jean-Pierre Jouannaud and Mitsuhiro Okada. Abstract data type systems. Theoretical Computer Science, 173(2):349-391, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00161-2.
  18. Cynthia Kop and Femke van Raamsdonk. Dynamic dependency pairs for algebraic functional systems. Log. Methods Comput. Sci., 8(2), 2012. URL: https://doi.org/10.2168/LMCS-8(2:10)2012.
  19. Ralph Matthes. Lambda Calculus: A Case for Inductive Definitions. Unpublished lecture notes, 2000. Google Scholar
  20. Nax Paul Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1):159-172, 1991. URL: https://doi.org/10.1016/0168-0072(91)90069-X.
  21. Mitsuhiro Okada. Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC '89, Portland, Oregon, USA, July 17-19, 1989, pages 357-363, 1989. URL: https://doi.org/10.1145/74540.74582.
  22. Erik Palmgren. On universes in type theory. In Giovanni Sambin and Jan M. Smith, editors, Twenty Five Years of Constructive Type Theory, Oxford Logic Guides, pages 191-204. Oxford University Press, 1998. Google Scholar
  23. Anton Setzer. Extending Martin-Löf type theory by one Mahlo-universe. Arch. Math. Log., 39(3):155-181, 2000. URL: https://doi.org/10.1007/s001530050140.
  24. Christoph Sprenger and Mads Dam. On the structure of inductive reasoning: Circular and tree-shaped proofs in the μ-calculus. In Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pages 425-440, 2003. URL: https://doi.org/10.1007/3-540-36576-1_27.
  25. Daria Walukiewicz-Chrząszcz. Termination of rewriting in the calculus of constructions. J. Funct. Program., 13(2):339-414, 2003. URL: https://doi.org/10.1017/S0956796802004641.
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