Oracles and Confluence - A Fixpoint Semantics for Concurrent Constraint Programming

We consider the problem of giving a fixpoint semantics for a parallel and non-deterministic programming language with fairness and arbitrary recursion, in which both finite and infinite computations are taken into account. We first define an operational semantics based on oracles (finite and infinite strings over a countable alphabet), in which the non-deterministic choices are determined by the oracle. The oracle-based operational semantics associates an oracle with each computation, conversely there is for each oracle a set (possibly empty) of computations. We show that the oracle semantics satisfies certain confluence properties, which are to be later used in the correctness proof of the fixpoint semantics. We give a fixpoint semantics for the language in which the semantics of an agent is given as a function from oracles to a pair consisting of a closure operator over the domain of constraints and a set of conditions which describe when it is legal to select a particular branch. It..