Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation

Alessandra Di Pierro and Herbert Wiklicky

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


We present a method for approximating the semantics of probabilistic programs to the purpose of constructing semantics-based analyses of various properties of such programs. The method resembles the one based on Galois connection used in abstract interpretation, the main difference being the choice of linear space structures instead of order-theoretic ones as semantical (concrete and abstract) domains. Linear spaces reflect the quantitative aspects of probabilistic computation and are therefore of fundamental importance in the semantics and the semantics-based analysis of probabilistic programs. We show the optimality of our method according to an appropriate notion of precision defined in terms of a norm. Moreover, if recasted in a cpo setting our method generates correct approximations in the sense of classical abstract interpretation theory. We use Concurrent Constraint Programming as a reference programming paradigm. The basic concepts and ideas can nevertheless be applied to any other paradigm. The results we present intend to be the first step towards a general theory of probabilistic abstract interpretation, in which the classical theory is extended so as to allow (among others) for both a qualitative and a quantitative reasoning about programs.