It is commonly known that any Bayesian network can be implemented as a probabilistic program, but the reverse direction is not so clear. In this work, we address the open question to what extent a probabilistic program with user-labelled sample statements and while loops – features found in languages like Gen, Turing, and Pyro – can be represented graphically. To this end, we extend existing operational semantics to support these language features. By translating a program to its control-flow graph, we define a sound static analysis that approximates the dependency structure of the random variables in the program. As a result, we obtain a static factorisation of the implicitly defined program density, which is equivalent to the known Bayesian network factorisation for programs without loops and constant labels, but constitutes a novel graphical representation for programs that define an unbounded number of random variables via loops or dynamic labels. We further develop a sound program slicing technique to leverage this structure to statically enable three well-known optimisations for the considered program class: we reduce the variance of gradient estimates in variational inference and we speed up both single-site Metropolis Hastings and sequential Monte Carlo. These optimisations are proven correct and empirically shown to match or outperform existing techniques.

@article{paperbot3816,
  title = {Static Factorisation of Probabilistic Programs with User-Labelled Sample Statements and While Loops},
  author = {Markus Böck and Jürgen Cito},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {OOPSLA1},
  year = {2026},
  doi = {10.1145/3798223}
}