We study notions of equivalence and refinement for
probabilistic programs formalized in the second-order fragment of
Probabilistic Idealized Algol. Probabilistic programs implement
randomized algorithms: a given input yields a probability distribution
on the set of possible outputs. Intuitively, two programs are
equivalent if they give rise to identical distributions for all
inputs. We show that equivalence is decidable by studying the fully
abstract game semantics of probabilistic programs and relating it to
probabilistic finite automata. For terms in β-normal form our
decision procedure runs in time exponential in the syntactic size of
programs; it is moreover fully compositional in that it can handle
open programs (probabilistic modules with unspecified
components).
In contrast, we show that the natural notion of program refinement, in
which the input-output distributions of one program uniformly dominate
those of the other program, is undecidable.
Proceedings of CONCUR 05, LNCS 3653, 2005. 15 pages.
PostScript /
PDF
© 2005
Springer-Verlag.