Probabilistic programming languages have emerged as a powerful tool for
modeling complex and uncertain systems. Widely applied in fields like artificial
intelligence, machine learning, robotics but also in non-technical domains as,
e.g., healthcare, social and climate sciences, economic and psychology, these
languages allow us to succinctly represent probabilistic processes, including
those involving loops, recursion, and other intricate structures. However,
reasoning about such programs, particularly those with infinite loops or non-
terminating behavior, poses significant challenges.
This dissertation introduces a novel approach to address these challenges by
developing a denotational probability generating function (PGF) semantics for
discrete probabilistic programs with loops. This semantics provides an exact
and compact representation of program behaviors, enabling exact Bayesian
inference where prior methods often relied on approximations. A central
contribution of this work is the introduction of invariant-based reasoning
techniques, which facilitate the systematic derivation of posterior distributions
and hence also properties like expectations and higher-order moments, even
for possibly unbounded loops.
Furthermore, we present a syntactic characterization of a class of proba-
bilistic programs for which the distributions they describe can be expressed
as rational closed-form generating functions. This characterization ensures
that exact inference is preserved within this class, allowing for efficient alge-
braic manipulation and direct computation of quantities such as tail bounds
and moments. By linking program syntax to the algebraic tractability of their
semantics, this work establishes a foundational framework for exact reasoning
in probabilistic programming.
This framework not only enhances the capacity for exact Bayesian inference
enabling decision-making under uncertainty but also broadens the applicability
of probabilistic programming to domains where formal verification is inevitable.
It combines theoretical rigor with practical utility, offering a unified perspective
on the structure and behavior of discrete probabilistic programs.