Article,

Polynat in PER-models

.
Theoretical Computer Science, (2004)

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.

Tags

Users

  • @t.uemura
  • @dblp

Comments and Reviews