DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2022.7

An Irrelevancy-Eliminating Translation of Pure Type Systems

Authors: Nathan Mull

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

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.

Cite as

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.TYPES.2022.7},
  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}
}

Search Results

Documents authored by Mull, Nathan

An Irrelevancy-Eliminating Translation of Pure Type Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message