The encodability hierarchy for PCF types

Abstract

Working with the simple types over a base type of natural numbers (including product types), we consider the question of when a type $σ$ is encodable as a definable retract of $τ$: that is, when there are $λ$-terms $e:σ\rightarrowτ$ and $d:τ\rightarrowσ$ with $d \circ e = id$. In general, the answer to this question may vary according to both the choice of $λ$-calculus and the notion of equality considered; however, we shall show that the encodability relation $\preceq$ between types actually remains stable across a large class of languages and equality relations, ranging from a very basic language with infinitely many distinguishable constants $0,1,\ldots$ (but no arithmetic) considered modulo computational equality, up to the whole of Plotkin's PCF considered modulo observational equivalence. We show that $σ\preceq τ\preceq σ$ iff $σ\cong τ$ via trivial isomorphisms, and that for any $σ,τ$ we have either $σ\preceq τ$ or $τ\preceq σ$. Furthermore, we show that the induced linear order on isomorphism classes of types is actually a well-ordering of type $ε_0$, and indeed that there is a close syntactic correspondence between simple types and Cantor normal forms for ordinals below $ε_0$. This means that the relation $\preceq$ is readily decidable, and that terms witnessing a retraction $σ\lhd τ$ are readily constructible when $σ\preceq τ$ holds.