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
Abstract
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.