License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2022.7
URN: urn:nbn:de:0030-drops-184501
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18450/
Go to the corresponding LIPIcs Volume Portal

Mull, Nathan

An Irrelevancy-Eliminating Translation of Pure Type Systems

pdf-format:
LIPIcs-TYPES-2022-7.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{mull:LIPIcs.TYPES.2022.7,
  author =	{Mull, Nathan},
  title =	{{An Irrelevancy-Eliminating Translation of Pure Type Systems}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{7:1--7:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18450},
  URN =		{urn:nbn:de:0030-drops-184501},
  doi =		{10.4230/LIPIcs.TYPES.2022.7},
  annote =	{Keywords: pure type systems, normalization, reduction-path-preserving translations, Barendregt-Geuvers-Klop conjecture}
}

Keywords: pure type systems, normalization, reduction-path-preserving translations, Barendregt-Geuvers-Klop conjecture
Collection: 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Issue Date: 2023
Date of publication: 28.07.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI