The paper shows the equivalence of two semantics for a version of Concurrent Prolog with non-flat guards: an operational semantics based on a transition system and a denotational semantics which is a metric semantics (the domains are metric spaces. It does this in the following manner: First a an uniform language Lambda is considered, that is a language where the atomic actions have arbitrary interpretations. For this language it proves that a denotational semantics is correct with respect to the operational semantics. The result relies on Banach's fixed point theorem. Techniques stemming from imperative languages are used. Then it shows how to translate a Concurrent Prolog program in Lambda by selecting certain basic sets for Lambda and then instantiating the interpretation function for the atomic actions. In this way it indices the two semantics for Concurrent Prolog and the equivalence between the two semantics.
展开▼
