Probabilistic Concurrent Constraint Programming: Towards a Fully Abstract Model

This paper presents a Banach space based approach towards a denotational semantics of a probabilistic constraint programming language. This language is based on the concurrent constraint programming paradigm, where randomness is introduced by means of a probabilistic choice construct. As a result, we obtain a declarative framework, in which randomised algorithms can be expressed and formalised. The denotational model we present is constructed by using functional-analytical techniques. As an example, the existence of fixed-points is guaranteed by the Brouwer-Schauder Fixed-Point Theorem. A concrete fixed-point construction is also presented which corresponds to a notion of observables capturing the exact results of both finite and infinite computations