Le système F avec paires a-t-il de fortes propriétés de normalisation et de réduction du sujet?

Il est facile de regarder dans beaucoup de manuels les preuves de réduction de sujet et de forte normalisation pour le système F, aussi, il existe parfois des définitions du système F avec des paires, où (t, r) est un terme, pas seulement un encodage. La question est, quelle serait la référence pour ce système?

Le traitement des paires donné par l'encodage, comme celui des preuves et des types , n'est pas ce que vous voulez habituellement car ce ne sont pas des "paires surjectives", c'est-à-dire qu'il n'y a pas de règle ETA. Appelons paires surjectives, produits.

Une extension du système F avec des produits et des unités est donnée dans: Di Cosmo, 1995, Isomorphisms of types: from lambda-calculus to retrieval information and language design , Birkhauser: Basel.

Vous pouvez ajouter des types inductifs arbitraires (positifs) au système F et montrer que le système avec les éliminateurs appropriés est SN. Ceci est traité dans la thèse de Mendler ici .