Hat das System F mit Paaren die starken Normalisierungs- und Subjektreduktionseigenschaften?

In vielen Lehrbüchern ist es einfach, die Beweise für die Reduzierung des Subjekts und die starke Normalisierung für System F zu lesen. Manchmal gibt es auch Definitionen von System F mit Paaren, wobei (t, r) ein Begriff ist, nicht nur eine Codierung. Die Frage ist, was wäre die Referenz für dieses System?

Die Behandlung von Paaren, die durch Codierung gegeben werden, wie die in Proofs und Typen , ist nicht das, was Sie normalerweise wollen, da es sich nicht um "surjektive Paare" handelt, dh es gibt keine eta-Regel. Nennen wir surjektive Paare Produkte.

Eine Erweiterung des Systems F um Produkte und Einheiten findet sich in: Di Cosmo, 1995, Isomorphismen von Typen: vom Lambda-Kalkül zum Informationsabruf und Sprachdesign , Birkhauser: Basel.

Sie können dem System F beliebige (positive) induktive Typen hinzufügen und zeigen, dass das System mit den entsprechenden Eliminatoren SN ist. Dies wird in Mendler Arbeit behandelt hier .