Operational domain theory and topology of sequential functional languages
Weng Kin Ho · OpenGrey (Institut de l'Information Scientifique et Technique) · 2006
We develop an operational domain theory to reason about programs in sequential functional languages. The central idea is to export domaintheoretic techniques of the Scott denotational semantics directly to the study of contextual pre-order and equivalence. We investigate to what extent this can be done for two deterministic functional programming languages: PCF (Programming-language for Computable Functionals) and FPC (Fixed Point Calculus). Traditionally, domain theory and topology in programming languages have been applied to manufacture and study denotational models, for instance, the Scott model of PCF. For a sequential language like this, it is well-known that the match of the model with the operational semantics is imprecise: computational adequacy holds but full abstraction fails. One of the main achievements is a reconciliation of a good deal of domain theory and topology with sequential computation. This is accomplished by side-stepping denotational semantics and reformulating domain-theoretic and topological notions directly in terms of programming concepts, interpreted in an operational way. Regarding operational domain theory, we introduce operational finiteness. The upshot is the SFP theorem: Every PCF type has an SFP structure. In particular, the set of finite elements of each type forms a basis. Regarding operational topology, we work with an operational notion of compactness. The elegance of the theory lies not only in the interplay of these two notions but also in the reasoning principles that emerge. For instance, we show that total programs with values on certain types are uniformly continuous on compact sets of total elements. We apply this and other conclusions to prove the correctness of non-trivial PCF programs that manipulate infinite data. For FPC, an operational domain theory is developed for treating recursive types. The principal approach taken here deviates from classical domain theory in that we do not produce recursive types via inverse limit constructions we have it for free by working directly with the operational semantics of FPC. The important step taken in this work is to extend type expressions to legitimate n-ary functors on suitable ‘syntactic’ categories. To achieve this, we rely on operational versions of the Plotkin’s uniformity principle and the minimal