%0 Journal Article %1 rummelhoff2004polynat %A Rummelhoff, Ivar %D 2004 %J Theoretical Computer Science %K lambda model polymorphism %P 224 %T Polynat in PER-models %U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.108.5998 %V 316 %X The polymorphic lambda-calculus can be modelled using PERs on a partial combinatory algebra. We say that the type of natural numbers (polynat) is polymorphically standard in such a model if the interpretation of the type only contains (the interpretations of) the Church numerals. We show that this is not always the case by constructing an explicit counterexample. On the other hand, when the PCA has either (strong) equality or weak equality plus a form of continuity, we show polynat is standard.

@article{rummelhoff2004polynat, abstract = {The polymorphic lambda-calculus can be modelled using PERs on a partial combinatory algebra. We say that the type of natural numbers (polynat) is polymorphically standard in such a model if the interpretation of the type only contains (the interpretations of) the Church numerals. We show that this is not always the case by constructing an explicit counterexample. On the other hand, when the PCA has either (strong) equality or weak equality plus a form of continuity, we show polynat is standard.}, added-at = {2015-03-15T06:10:09.000+0100}, author = {Rummelhoff, Ivar}, biburl = {https://www.bibsonomy.org/bibtex/204071973babaeda0ea65382be5ed9abf/t.uemura}, description = {CiteSeerX — Polynat in PER-models}, interhash = {c23e210d235fdc701f865ad14c254180}, intrahash = {04071973babaeda0ea65382be5ed9abf}, journal = {Theoretical Computer Science}, keywords = {lambda model polymorphism}, pages = 224, timestamp = {2015-03-15T06:10:09.000+0100}, title = {Polynat in PER-models}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.108.5998}, volume = 316, year = 2004 }