Semantic models for concurrent logic languages (Q1177921)

As the title suggests this paper discusses various semantic models for a class of concurrent logic languages. In fact, four semantic models are treated: an operational model and a declarative one modelling the success set (i.e. the set of computed answer substitutions corresponding to all successfully terminating computations), and an operational model and a denotational one modelling all computations including deadlocking and infinite ones. Both operational semantics are defined via transition relations on configurations consisting of goals to be achieved (proved) and results (substitutions) that have been obtained so far. Both declarative and denotational semantics are based on fixed-point constructions. The declarative semantics is based on finite streams of substitutions, whereas the denotational semantics is based on tree-like structures of unification steps (using metric space techniques). Although all this seems to be rather heterogeneous (and, to be honest, it really is to some extent), the authors show that the declarative semantics is equivalent with the first operational one, and that the denotational model is correct with respect to the second operational semantics (i.e. this operational semantics is an abstraction of the denotational one). The denotational model is not fully abstract, however, leaving the construction of such a model is an open issue.