<p>You can add arbitrary (positive) inductive types to system F, and show that the system with appropriate eliminators is SN. This is treated in Mendler's thesis <a href="http://www.cs.cornell.edu/info/Projects/Nuprl/documents/Mendler/InductiveDefinition.html" rel="noreferrer">here</a>.</p>

CC BY-SA 3.0
2011-06-11T08:59:50.510Z
This is also treated, albeit in somewhat sketchy detail, in sections 11.4 and 11.5 of *[Proofs and Types](http://www.paultaylor.eu/stable/Proofs+Types.html)*.
Charles Stewart
CC BY-SA 3.0
2011-06-09T13:05:31.840Z
2011-06-09T13:05:31.840Z
cody
<p>The treatment of pairs given by encoding, such as that in <em>Proofs and Types</em>, isn't what you usually want since they aren't "surjective pairs", i.e., there is no eta rule.  Let's call surjective pairs, products.</p>

<p>An extension of system F with products and unit is given in: Di Cosmo, 1995,  <em>Isomorphisms of types: from lambda-calculus to information retrieval and language design</em>,  Birkhauser: Basel.</p>

CC BY-SA 2.5
2010-09-02T17:59:19.867Z
2010-09-02T20:59:10.480Z
2010-09-02T20:59:10.480Z
Charles Stewart
<p>It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not only an encoding. The question is, what would be the reference for this system?</p>

<reference-request><lo.logic><type-theory><lambda-calculus><polymorphism>
Does the System F with pairs have the strong normalisation and subject reduction properties?
Alejandro DC
# Does the System F with pairs have the strong normalisation and subject reduction properties?

(Asked by: username_0 on 2010-09-02)

It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not only an encoding. The question is, what would be the reference for this system?

**Tags:** reference-request, lo.logic, type-theory, lambda-calculus, polymorphism


---

## 2 answers

### Answer by username_2 on 2010-09-02. Score: 14 | Accepted answer

The treatment of pairs given by encoding, such as that in *Proofs and Types*, isn't what you usually want since they aren't "surjective pairs", i.e., there is no eta rule. Let's call surjective pairs, products.

An extension of system F with products and unit is given in: Di Cosmo, 1995, *Isomorphisms of types: from lambda-calculus to information retrieval and language design*, Birkhauser: Basel.


---

### Answer by username_1 on 2011-06-09. Score: 6

You can add arbitrary (positive) inductive types to system F, and show that the system with appropriate eliminators is SN. This is treated in Mendler's thesis [here](http://www.cs.cornell.edu/info/Projects/Nuprl/documents/Mendler/InductiveDefinition.html).

> **Comments:**
> **username_2**: This is also treated, albeit in somewhat sketchy detail, in sections 11.4 and 11.5 of *[Proofs and Types](http://www.paultaylor.eu/stable/Proofs+Types.html)*.  

---

