On the asynchronous nature of communication in concurrent logic languages: A fully abstract model based on sequences

The main contribution of this paper is to show that the nature of the communication mechanism of concurrent logic languages is essentially different from imperative concurrent languages. We show this by defining a compositional model based on sequences of input-output substitutions. This is to be contrasted with the compositionality in languages like CCS and TCSP, which requires more complicated structures, like trees and failure sets. Moreover, we prove that this model is fully abstract, namely that the information encoded by these sequences is necessary. Regarding fully abstractness, our observation criterium consists of all the possible finite results, namely the computed answer substitution together with the termination mode (success, failure, or suspension). The operations we consider are parallel composition of goals and disjoint union of programs. We define a compositional operational semantics delivering sequences of input-output substitutions. Starting from this we obtain a fully abstract denotational semantics by requiring some closure conditions on sequences, that essentially model the monotonic nature of communication in concurrent logic languages. The correctness of this model is proved by refining the operational semantics in order to embody these closure conditions.