Full Abstraction for Nominal Scott Domains
We develop a domain theory within nominal sets and present programming
language constructs and results that can be gained from this
approach. The development is based on the concept of orbit-finite
subset, that is, a subset of a nominal sets that is both finitely
supported and contained in finitely many orbits. This concept appears
prominently in the recent research programme of Bojanczyk et al. on
automata over infinite languages, and our results establish a
connection between their work and a characterisation of topological
compactness discovered, in a quite different setting, by Winskel and
Turner as part of a nominal domain theory for concurrency. We use this
connection to derive a notion of Scott domain within nominal sets. The
functionals for existential quantification over names and "definite
description" over names turn out to be compact in the sense
appropriate for nominal Scott domains. Adding them, together with
parallel-or, to a programming language for recursively defined
higher-order functions with name abstraction and locally scoped names,
we prove a full abstraction result for nominal Scott domains analogous
to Plotkin's classic result about PCF and conventional Scott domains:
two program phrases have the same observable operational behaviour in
all contexts if and only if they denote equal elements of the nominal
Scott domain model. This is the first full abstraction result we know
of for higher-order functions with local names that uses a domain
theory based on ordinary extensional functions, rather than using the
more intensional approach of game semantics.
Last modified: Fri Oct 26 21:52:40 BST 2012