Stable and sequential functions on Scott domains
CMU SCS Tech reports 92-121, School of Computer Science, Carnegie Mellon
University, June 1992
Submitted for publication
The search for a general semantic characterization of sequential functions is
motivated by the full abstraction problem for sequential programming
languages such as PCF. We present here some new developments towards such a
theory of sequentiality. We give a general definition of sequential functions
on Scott domains, characterized by means of a generalized form of topology,
based on sequential open sets. Our notion of sequential function coincides
with the Kahn-Plotkin notion of sequential function when restricted to
distributive concrete domains, and considerably expands the class of domains
for which sequential functions may be defined.
We show that the sequential
functions between two dI-domains, ordered stably, form a dI-domain. The
analogous property fails for Kahn-Plotkin sequential functions. Our category
of dI-domains and sequential functions is not cartesian closed, because
application is not sequential. We attribute this to certain operational
assumptions underlying our notion of
sequentiality. We show that the Scott domains satisfying a certain
``finite meet'' property are closed under the pointwise-ordered stable
function space, so that we obtain a new stable model based on the pointwise
order. We discuss some issues arising in the search for a class of domains
closed under the pointwise-ordered sequential function space.
We discuss the relationship between our ideas and the full abstraction
problem for PCF, and indicate directions for further development.
Keywords: Theory, applicative (functional) programming,
semantics, topology, sequentiality.
BRICS WWW home page