A compositional semantics for Concurrent Prolog

Abstract

Concurrent logic languages like Concurrent Prolog have mechanisms in common with imperative concurrent languages: concurrency, communication, synchronization and indeterminacy, finite and infinite behaviour. A goal statement can be considered as a network of processes which run in parallel and can communicate. For imperative concurrent languages a lot of research on the semantics has been done. In this paper we show that a model, which was originally designed for imperative languages, can be used to give a formal description of Concurrent Prolog. This model is compositional: for any two conjunctions C ₁, C ₂ the meaning of C ₁ ⋀ C ₂ can be obtained by applying a function to the meanings of C ₁ and C ₂. To be more specific: we shall employ a domain where some choices made during the computation are recorded in certain tree-like structures, and which allows for interleaving. We use tree like structures because it is not possible to use flat structures (like traces or sequences of substitutions). They do not contain enough information to handle deadlock or infinite computations. Such phenomena require that we know at a certain moment in time all the alternatives. The domain is obtained as a solution of a domain equation. We apply metric topological tools to find a solution of the domain equation, and to define operations on elements of the domain. The semantic function maps goals, given a program P, to elements of the domain. This function is defined recursively. The model is able to handle both finite and infinite computations.

Note: this work is partially supported by by the Netherlands Organization for the Advancement of Pure Research (Z.W.O.), grant 125-20-04.