On the Relation Between Direct and Continuation Semantics

The use of continuations in the definition of programming languages has gained considerable currency recently, particularly in conjunction with the lattice-theoretic methods of D. Scott. Although continuations are apparently needed to provide a mathematical semantics for non-applicative control features, they are unnecessary for the definition of a purely applicative language, even when call-by-value occurs. This raises the question of the relationship between the direct and the continuation semantic functions for a purely applicative language. We give two theorems which specify this relationship and show that, in a precise sense, direct semantics are included in continuation semantics. The heart of the problem is the construction of a relation which must be a fixed-point of a non-monotonic "relational functor." A general method is given for the construction of such relations between recursively defined domains.