Asynchronous Nature of Communication in Concurrent Logic Languages: A Fully Abstract Model Based on Sequences

摘要

The paper shows that the nature of the communication mechanism of concurrent logic languages is essentially different from imperative concurrent languages. The authors 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, they prove that this model is fully abstract, namely that the information encoded by these sequences is necessary. Regarding fully abstractness, the observation criterion consists of all the possible finite results, namely the computed answer substitution together with the termination mode (success, failure, or suspension). The operations they consider are parallel composition of goals and disjoint union of programs. They define a compositional operational semantics delivering sequences of input-output substitutions. Starting from this they 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.