Document Open Access Logo

Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions

Authors Andrej Dudenhefner , Daniele Pautasso

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.8.pdf
  • Filesize: 0.84 MB
  • 20 pages

Document Identifiers

Author Details

Andrej Dudenhefner
  • TU Dortmund University, Germany
Daniele Pautasso
  • University of Turin, Italy

Acknowledgements

The authors are grateful to Simona Ronchi Della Rocca for many insightful discussions, and to the anonymous referees for their careful reading and suggestions.

Cite AsGet BibTex

Andrej Dudenhefner and Daniele Pautasso. Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.8

Abstract

We provide a new, purely syntactical proof of strong normalization for the simply typed λ-calculus. The result relies on a novel proof of the equivalence between typability in the simple type system and typability in the uniform intersection type system (a restriction of the non-idempotent intersection type system). For formal verification, the equivalence is mechanized using the Coq proof assistant. In the present work, strong normalization of a given simply typed term M is shown in four steps. First, M is reduced to a normal form N via a suitable reduction strategy with a decreasing measure. Second, a uniform intersection type for the normal form N is inferred. Third, a uniform intersection type for M is constructed iteratively via subject expansion. Fourth, strong normalization of M is shown by induction on the size of the type derivation. A supplementary contribution is a family of perpetual reduction strategies, i.e. strategies which preserve infinite reduction paths. This family allows for subject expansion in the intersection type systems of interest, and contains a reduction strategy with a decreasing measure in the simple type system. A notable member of this family is Barendregt’s F_∞ reduction strategy.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • lambda-calculus
  • simple types
  • intersection types
  • strong normalization
  • mechanization
  • perpetual reductions

Metrics

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

Supplementary Materials

References

  1. Pablo Barenbaum and Cristian Sottile. Two decreasing measures for simply typed λ-terms. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 11:1-11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.11.
  2. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. URL: http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types.
  3. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:7)2018.
  4. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/JIGPAL/JZX018.
  5. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for λ-terms. Arch. Math. Log., 19(1):139-156, 1978. URL: https://doi.org/10.1007/BF02011875.
  6. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the lambda-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  7. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Mathematical Logic Quarterly, 27(2-6):45-58, 1981. URL: https://doi.org/10.1002/malq.19810270205.
  8. René David. Normalization without reducibility. Ann. Pure Appl. Log., 107(1-3):121-130, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00030-0.
  9. Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. North-Holland, 1972. Google Scholar
  10. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  11. Philippe de Groote. The conservation theorem revisited. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 163-178. Springer, 1993. URL: https://doi.org/10.1007/BFB0037105.
  12. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Commun. ACM, 22(8):465-476, 1979. URL: https://doi.org/10.1145/359138.359142.
  13. Jean H. Gallier. On Girard’s "Candidats de Reductibilité". University of Pennsylvania, 1989. URL: https://api.semanticscholar.org/CorpusID:14688391.
  14. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, volume 789 of Lecture Notes in Computer Science, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  15. Jean-Yves Girard. Une extension de l'interpretation de Gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 63-92. Elsevier, 1971. URL: https://doi.org/10.1016/S0049-237X(08)70843-7.
  16. Inge Li Gørtz, Signe Reuss, and Morten Heine Sørensen. Strong normalization from weak normalization by translation into the lambda-I-calculus. High. Order Symb. Comput., 16(3):253-285, 2003. URL: https://doi.org/10.1023/A:1025693307470.
  17. Assaf J. Kfoury and Joe B. Wells. Addendum to "New notions of reduction and non-semantic proofs of strong beta-normalization in typed lambda calculi", 1995. URL: https://open.bu.edu/handle/2144/1568.
  18. Assaf J. Kfoury and Joe B. Wells. New notions of reduction and non-semantic proofs of beta-strong normalization in typed lambda-calculi. In Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 311-321. IEEE Computer Society, 1995. URL: https://doi.org/10.1109/LICS.1995.523266.
  19. Jan Willem Klop. Combinatory reduction systems. PhD thesis, Univ. Utrecht, 1980. Google Scholar
  20. Robert Pieter Nederpelt Lazarom. Strong normalization in a typed lambda calculus with lambda structured types. PhD thesis, TU Eindhoven, 1973. Google Scholar
  21. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université de Paris 7, 1978. Google Scholar
  22. Peter Møller Neergaard. Theoretical pearls: A bargain for intersection types: a simple strong normalization proof. J. Funct. Program., 15(5):669-677, 2005. URL: https://doi.org/10.1017/S0956796805005587.
  23. Daniele Pautasso and Simona Ronchi Della Rocca. A quantitative version of simple types. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1-29:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.29.
  24. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism, pages 561-577, 1980. Google Scholar
  25. Helmut Schwichtenberg. An upper bound for reduction sequences in the typed λ-calculus. Arch. Math. Log., 30(5-6):405-408, 1991. URL: https://doi.org/10.1007/BF01621476.
  26. Morten Heine Sørensen. Strong normalization from weak normalization in typed lambda-calculi. Inf. Comput., 133(1):35-71, 1997. URL: https://doi.org/10.1006/INCO.1996.2622.
  27. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 166-180. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294101.
  28. William W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  29. William W. Tait. A realizability interpretation of the theory of species. In Rohit Parikh, editor, Logic Colloquium, pages 240-251, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg. Google Scholar
  30. The Coq Development Team. The Coq proof assistant, July 2023. URL: https://doi.org/10.5281/zenodo.8161141.
  31. Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen, and Hongwei Xi. Perpetual reductions in lambda-calculus. Inf. Comput., 149(2):173-225, 1999. URL: https://doi.org/10.1006/INCO.1998.2750.
  32. Hongwei Xi. Weak and strong beta normalisations in typed lambda-calculi. In Philippe de Groote, editor, Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings, volume 1210 of Lecture Notes in Computer Science, pages 390-404. Springer, 1997. URL: https://doi.org/10.1007/3-540-62688-3_48.
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