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.

Description

CiteSeerX — Polynat in PER-models

Links and resources

Tags

community

  • @t.uemura
  • @dblp
@t.uemura's tags highlighted