Document Open Access Logo

An Irrelevancy-Eliminating Translation of Pure Type Systems

Author Nathan Mull

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.7.pdf
  • Filesize: 0.72 MB
  • 21 pages

Document Identifiers

Author Details

Nathan Mull
  • University of Chicago, IL, USA

Acknowledgements

I'd like to thank Stuart Kurtz for many useful discussions as well as the reviewers for their incredibly helpful comments.

Cite As Get BibTex

Nathan Mull. An Irrelevancy-Eliminating Translation of Pure Type Systems. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.TYPES.2022.7

Abstract

I present an infinite-reduction-path-preserving typability-preserving translation of pure type systems which eliminates rules and sorts that are in some sense irrelevant with respect to normalization. This translation can be bootstrapped with existing results for the Barendregt-Geuvers-Klop conjecture, extending the conjecture to a larger class of systems. Performing this bootstrapping with the results of Barthe et al. [Barthe et al., 2001] yields a new class of systems with dependent rules and non-negatable sorts for which the conjecture holds. To my knowledge, this is the first improvement in the state of the conjecture since the results of Roux and van Doorn [Roux and Doorn, 2014] (which can be used for the same sort of bootstrapping argument) albeit a somewhat modest one; in essence, the translation eliminates clutter in the system that does not affect normalization. This work is done in the framework of tiered pure type systems, a simple class of persistent systems which is sufficient to study when concerned with questions about normalization.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • pure type systems
  • normalization
  • reduction-path-preserving translations
  • Barendregt-Geuvers-Klop conjecture

Metrics

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

References

  1. TLCA List of Open Problems, 2014. http://tlca.di.unito.it/opltlca/. Google Scholar
  2. Henk Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125-154, 1991. Google Scholar
  3. Henk Barendregt. Lambda Calculi with Types. In Handbook of Logic in Computer Science, Volume II, pages 117-309. Oxford University Press, 1993. Google Scholar
  4. Gilles Barthe, John Hatcliff, and Morten Heine Sørensen. Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theoretical Computer Science, 269(1-2):317-361, 2001. Google Scholar
  5. Stefano Berardi. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt’s cube. Technical report, Carnegie Mellon University, Universita di Torino, 1988. Google Scholar
  6. Stefano Berardi. Type Dependence and Constructive Mathematics. PhD thesis, Dipartimento di Informatica, Torino, Italy, 1990. Google Scholar
  7. Herman Geuvers. The Calculus of Constructions and Higher Order Logic. In The Curry-Howard Isomorphism, volume 8 of Cahiers du Centre de Logique (Universit'e catholique de Louvain), Academia, Louvain-la-Neuve (Belgium), pages 131-191, 1995. Google Scholar
  8. Herman Geuvers and Mark-Jan Nederhof. Modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming, 1(2):155-189, 1991. Google Scholar
  9. Jan Herman Geuvers. Logic and Type Systems. PhD thesis, University of Nijmegen, 1993. Google Scholar
  10. Robert Harper, Furio Honsell, and Gordon Plotkin. A Framework for Defining Logics. Journal of the ACM, 40(1):143-184, 1993. Google Scholar
  11. Gérard Huet. Residual Theory in λ-Calculus: A Formal Development. Journal of Functional Programming, 4(3):371-394, 1994. Google Scholar
  12. Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. A Modern Perspective on Type Theory: From its Origins until Today, volume 29 of Applied Logic Series. Springer, 2004. Google Scholar
  13. Jeroen Ketema, Jan Willem Klop, and V van Oostrom. Vicious Circles in Rewriting Systems. Artificial Intelligence Preprint Series, 52, 2004. Google Scholar
  14. Jean-Jacques Lévy. Réductions Correctes et Optimales dans le Lambda-Calcul. PhD thesis, L'Université Paris VII, 1978. Google Scholar
  15. Zhaohui Luo. An extended calculus of constructions. PhD thesis, University of Edinburgh, 1990. Google Scholar
  16. Cody Roux and Floris van Doorn. The Structural Theory of Pure Type Systems. In Rewriting and Typed Lambda Calculi, pages 364-378. Springer, 2014. Google Scholar
  17. Morten Heine Sørensen. Strong Normalization from Weak Normalization in Typedλ-Calculi. Information and Computation, 133(1):35-71, 1997. Google Scholar
  18. Jan Terlouw. Een nadere bewijstheoretische analyse van GSTT’s. Technical report, Department of Computer Science, University of Nijmege, 1989. Google Scholar
  19. Hongwei Xi. On Weak and Strong Normalisations. Technical report, Carnegie Mellon University, Department of Mathematics, 1996. Google Scholar
  20. Hongwei Xi. Development Separation in Lambda-Calculus. Electronic Notes in Theoretical Computer Science, 143:207-221, 2006. 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 About DROPS Imprint Privacy Contact