A FULLY ABSTRACT SEMANTICS FOR CONCURRENT CONSTRAINT PROGRAMMING

A compositional and fully abstract semantics for concurrent constraint programming is developed. It is the first fully abstract semantics wh ich takes into account both non-determinism, infinite computations, an d fairness. We present a simple concurrent constraint programming lang uage, whose semantics is given by a set of reduction rules augmented w ith fairness requirements. In the fully abstract semantics we consider two aspects of a trace, viz. the function computed by the trace (the functionality) and the set of input and output data (the limit of the trace). We then derive the fully abstract semantics from the set of tr aces using a closure operation. We give two proofs of full abstraction ; the first relies on the use of a syntactically infinite context. The second proof requires only a finite context, but assumes as input a r epresentation of the function to be computed by the context. Finally, we examine the algebraic properties of the programming language with r espect to the fully abstract semantics. It turns out that the non-dete rministic selection operation can be defined using operations derived from parallel composition and the usual set-theoretic operations on se ts of traces. (C) 1998 Academic Press.