[TYPES] polymorphic isomorphisms
Paul B Levy
P.B.Levy at cs.bham.ac.uk
Wed Jan 23 14:09:43 EST 2008
Dear all,
Do the following System F isomorphisms appear in the literature, and
are they validated by the standard models?
(1)
Prod X. ((X -> B) -> A) cong A [ nu X. B / X ]
where X is negative in A and positive in B
(2)
Prod X. ((B -> X) -> A) cong A [ mu X. B / X ]
where X is positive in A and B
Also, are any other isomorphisms (beyond the obvious beta-eta ones) known?
(By "isomorphism" I mean definable both ways by terms that are inverse up
to observational equivalence.)
The following isomorphisms are similar, but they're already derivable from
(1)-(2).
(3)
Sum X. ((X -> B) x A) cong A [ nu X. B / X ]
where X is positive in A and B
(4)
Sum X. ((B -> X) x A) cong A [ mu X. B / X ]
where X is negative in A and positive in B
regards,
Paul
--
Paul Blain Levy email: pbl at cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K. tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl
More information about the Types-list
mailing list