Abstract

When presenting a denotational semantics of a language with recursion, it is necessary to show that the semantics is computationally adequate, i.e. that every divergent term denotes the “bottom” element of its associated domain.

We will explain how to view such a theorem as a purely syntactic result. Any theory (congruence) that includes basic laws and is closed under an infinitary rule that we call “rational continuity” has the property that every divergent term is equated with the divergent constant. Therefore, to prove a model adequate, it suffices to show that it validates the basic laws and the rational continuity rule. While this approach was inspired by the categorical, ordered framework of Abramsky et. al., neither category theory nor order is needed.

To show the applicability of our approach, we will present this syntactic result in various contexts: we will start with PCF ; then we will see what complications arise when we try to add sum types; these complications will be much amplified when we handle our next target, Levy’s Call-by-push-value; and, finally, time-permitting, we will talk briefly about polymorphic types.