Abstract: |
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 directlly 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 invariance property. This provides a basis for us to
introduce the operational notion of algebraic compactness. We then
establish algebraic compactness results in this operational setting.
In addition, a "pre-deflationary" structure is derived on closed FPC
types and this is used to generalise the "Generic Approximation Lemma"
recently developed by Huttons and Gibbons. This lemma provided a
powerful tool for proving program equivalence by simple inductions,
where previously various other more complex methods had been employed.
|