Relational Interpretations of Recursive Types in an Operational Setting

摘要

Relational interpretations of type systems are useful for establishing propertiesof programming languages. For languages with recursive types it is usually difficult to establish the existence of a relational interpretation. The usual approach is to give a denotational semantics of the language in a domain theoretic model given by an inverse limit construction, and to construct relations over the model by a similar inverse limit construction. However, in passing to a denotational semantics we incur the obligation to prove its adequacy with respect to the operational semantics of the language, which is itself often proved using a relational interpretation of types. In this paper we investigate the construction of relational interpretations of recursive types in a purely operational setting, drawing on recent ideas from domain theory and operational semantics as a guide. We establish a syntactic minimal invariance property for an ML like language with a recursive type that is a syntactic analog of Freyd's universal characterization of the canonical solution of a domain equation. As Pitts has shown in the setting of domains, minimal invariance suffices to establish the existence of relational interpretations of recursive types. We give two applications of this construction. First, we derive a notion of logical equivalence for expressions of the language that we show coincides with contextual equivalence and which, by virtue of its construction, validates useful induction and conduction principles for reasoning about the recursive type. Second, we give a relational proof of correctness of the continuation passing transformation which is used in some compilers for functional languages. The proof relies on the construction of a family of simulation relations whose existence follows from syntactic minimal invariance.