Full Abstraction and Fixed-Point Principles for Indeterminate Computation
Russell, James R.
Recently, there has been much interest in the problem of finding semantic models for various kinds of concurrent systems. A common property of concurrent systems is indeterminate behavior, either because of unpredictable interactions between processes, or because of abstractions removing the temporal details of the interaction. As a result, the study of the semantics of indeterminacy is necessary and important to the understanding of concurrency. The goal of any semantic model is that is capture our intuitions about the operational behavior of the underlying system and aid in our reasoning about it. Two properties of semantic models that we find useful in achieving this goal are full abstraction and fixed-point principles. In this thesis we investigate the problem of finding semantic descriptions with these properties for indeterminate systems. We begin by looking at a simple imperative language containing unbounded indeterminacy, based on one studied by Apt and Plotkin. We use category-theoretic techniques to develop a fixed-point semantics that, while not fully abstract, reduces to a fully abstract semantics via a simple abstraction functor. We then concentrate on the more general setting of dataflow networks and the hierarchy of indeterminate merge primitives. We show that the straighforward generalization of Kahn's semantics based on the input-output relations fails to be compositional for any class of indeterminate dataflow networks, thereby providing a model considerably more general than Kahn's. This generalization has the drawback that it does not have a simple fixed-point principle. We proceed to study a class of networks that models purely internal indeterminacy, called oraclizable networks, and show that for this class a generalization of Kahn's semantics to sets of functions is both fully abstract and has a natural fixed-point principle. We also show that the oraclizable networks are in fact universal for this representation. Finally, we use this representation to compare the class of oraclizable networks to other classes, and discover new relations among the classes.
computer science; technical report
Previously Published As