  Probabilistic programs are typically normal-looking programs describing
posterior probability distributions. They intrinsically code up randomized
algorithms and have long been at the heart of modern machine learning and
approximate computing. We explore the theory of generating functions [19] and
investigate its usage in the exact quantitative reasoning of probabilistic
programs. Important topics include the exact representation of program
semantics [13], proving exact program equivalence [5], and -- as our main focus
in this extended abstract -- exact probabilistic inference. In probabilistic
programming, inference aims to derive a program's posterior distribution. In
contrast to approximate inference, inferring exact distributions comes with
several benefits [8], e.g., no loss of precision, natural support for symbolic
parameters, and efficiency on models with certain structures. Exact
probabilistic inference, however, is a notoriously hard task [6,12,17,18]. The
challenges mainly arise from three program constructs: (1) unbounded
while-loops and/or recursion, (2) infinite-support distributions, and (3)
conditioning (via posterior observations). We present our ongoing research in
addressing these challenges (with a focus on conditioning) leveraging
generating functions and show their potential in facilitating exact
probabilistic inference for discrete probabilistic programs.
