Stable and sequential functions on Scott domains

Steven Brookes
Shai Geva

CMU SCS Tech reports 92-121, School of Computer Science, Carnegie Mellon University, June 1992
Submitted for publication

Available as PostScript.

Abstract:

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