# Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops
**Authors**: Markus Böck, Jürgen Cito
> TU Wien Vienna Austria
(2025)
## Abstract
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.
Probabilistic programming, operational semantics, static program analysis, factorisation, Bayesian networks copyright: acmlicensed journalyear: 2025 doi: XXXXXXX.XXXXXXX conference: ACM Conference; July 2025; Washington, DC, USA isbn: 978-1-4503-XXXX-X/18/06 ccs: Theory of computation Operational semantics ccs: Theory of computation Program analysis ccs: Mathematics of computing Bayesian computation ccs: Mathematics of computing Bayesian networks
## 1. Introduction
Probabilistic programming provides an intuitive means to specify probabilistic models as programs. Typically, probabilistic programming systems also come with machinery for automatic posterior inference. This enables practitioners without substantial knowledge in Bayesian inference techniques to work with complex probabilistic models.
Besides these practical aspects, there is also a long history of studying probabilistic programming languages (PPLs) from a mathematical perspective (Kozen, 1979; Barthe et al., 2020). It is commonly known that any Bayesian network (Koller and Friedman, 2009) can be implemented as a probabilistic program (Gordon et al., 2014), but the reverse direction is not so clear. The understanding is that first-order probabilistic programs without loops can be compiled to Bayesian networks, because the number of executed sample statements is fixed and finite, such that each sample statement corresponds to exactly one random variable (van de Meent et al., 2018; Borgström et al., 2011; Sampson et al., 2014). Generally, a graphical representation of a probabilistic program is desirable as it lends itself for optimising inference algorithms by exploiting the dependency structure between random variables. In fact, many probabilistic programming languages require the user to explicitly construct the model in a graphical structure (Salvatier et al., 2016; Minka, 2012; McCallum et al., 2009; Lunn et al., 2000; Milch et al., 2007).
However, in the universal probabilistic programming paradigm probabilistic constructs are embedded in a Turing-complete language (Goodman et al., 2012). While loops and recursive function calls easily lead to an unbounded number of executed sample statements which makes the typical compilation to a graph with one node per random variable impossible. Even more, many PPLs allow the user to label each sample statement with a dynamic address. This further complicates matters, because in this case even a single sample statement may correspond to a potentially infinite number of random variables. As a consequence, many approaches resort to dynamic methods to leverage the dependency structure of this kind of probabilistic programs for efficient inference (Wu et al., 2016; Yang et al., 2014; Chen et al., 2014).
Sample statements with dynamic address expressions constitute a valuable language feature, as they allow the definition of random variables whose identifiers differ from the program variables to which values are assigned to. This permits the specification of a broader model class relative to PPLs that lack this feature. Below we give examples of such user-labelled sample statements in Gen (Cusumano-Towner et al., 2019), Pyro (Bingham et al., 2019), and Turing (Ge et al., 2018), where the address expressions are highlighted with red:
⬇
x = {: x => i} ~ Normal (0.,1.) # Gen
x = pyro. sample (f "x{i}", Normal (0.,1.)) # Pyro
x [i] ~ Normal (0.,1.) # Turing
x = sample (" x"+str(i), Normal (0.,1.)) # our formal syntax
In this work, we address the open question to what extent a probabilistic program with user-labelled sample statements and while loops can be represented graphically. We prove that that the density of a probabilistic program with $K$ user-labelled sample statements decomposes into $K$ factors. This finite factorisation holds even if the program contains while loops. Moreover, the dependency structure implied by the factorisation can be computed statically which, as we will show, enables new opportunities for the optimisation of inference algorithms.
### 1.1. Overview
Section 2. Address-Based Semantics For Probabilistic Programs generalises the operational semantics of Core Stan (Gorinova et al., 2019). Instead of interpreting the program density $p$ as a function over only a fixed set of finite variables, we extend this approach to interpret the density as a function over traces. In contrast to Gorinova et al. (2019), this allows us to consider programs with dynamic addresses and while loops. These language features greatly expand the class of expressible probabilistic models, for instance, models with an infinite number of random variables. The described semantics can be seen as an operational analog to the denotational models of Pyro (Lee et al., 2019) and Gen (Lew et al., 2023).
Section 3. Static Factorisation for Programs Without Loops examines the factorisation of the program density for the simplified case where programs do not contain while loops.
In Section 3.2, building on standard data and control flow analysis techniques, we present a static provenance analysis that finds the dependencies of a program variable $x$ at any program state $\sigma$ . The dependencies are described by specifying for which addresses a trace $\mathtt{tr}$ needs to be known to also know the value of $x$ in $\sigma$ . This analysis forms the basis for finding the factorisation over addresses and operates on the control-flow graph (CFG) of a program.
In Section 3.3, we derive a novel factorisation from the static analysis, $p(\mathtt{tr})=\prod_{k=1}^{K}p_{k}(\mathtt{tr})$ , for programs without loops by explicitly constructing one factor $p_{k}$ per sample statement. If we further restrict the program to constant addresses, we arrive at the language of Gorinova et al. (2019), where our factorisation theorem implies a known equivalence to Bayesian networks. However, we show that already in the case of dynamic addresses, programs are only equivalent to Markov networks, because of the possibility of cyclic dependencies and an infinite number of random variables.
Section 4. Static Factorisation for Programs With Loops describes a way to generalise the factorisation result of Section 3 to the much more challenging case where programs may contain while loops. The idea is to mathematically unroll while loops to obtain a directed acyclic graph, the unrolled CFG, that essentially represents all possible program paths. Our main theoretical contribution is to show that even in this case, the density still factorises into a finite number of terms – one factor for each of the $K$ sample statements. Like dynamic addresses, while loops may also be used to model an infinite number of random variables and thus, the resulting factorisation in general implies the equivalence of programs to Markov networks.
Section 5. Optimising Posterior Inference Algorithms presents a novel and sound program slicing method building on the factorisation theory established in Section 4. By generating sub-programs for each factor, we can 1. decrease the runtime of a Metropolis Hastings algorithm by speeding up the acceptance probability computation; 2. construct a lower-variance gradient estimator for Black-Box Variational Inference; 3. facilitate an iterative implementation of sequential Monte Carlo. Each of the considered optimisations are known, but have been either realised dynamically or were reserved for PPLs that require the explicit graphical construction of probabilistic models. Our approach is the first to enable them statically for the considered program class. We evaluate our approach on a benchmark set of 16 probabilistic programs, the majority of which make use of while loops to define an unbounded number of random variables.
### 1.2. Contributions
We briefly summarise the key contributions of this work:
- A static provenance analysis in the context of our formal PPL building on standard data and control flow techniques,
- A novel density factorisation for the considered program class, which can be computed statically and subsumes a known equivalence to Bayesian networks in a restricted setting,
- A novel and sound program slicing method derived from the factorisation theory,
- An application of the slicing method to enable well-known optimisations statically and provably correct for the considered program class and three inference algorithms: Metropolis Hastings, variational inference, and sequential Monte Carlo,
- An open-source implementation and empirical evaluation of our proposed approach (Böck, 2025).
## 2. Address-Based Semantics For Probabilistic Programs
First, we introduce the syntax of our formal probabilistic programming language in terms of expressions and statements similar to Gorinova et al. (2019) and Hur et al. (2015). We assume that the constants of this language range over a set of values including booleans, integers, real numbers, immutable real-valued vectors, finite-length strings, and a special $\mathtt{null}$ value. We define $\mathcal{V}$ to be the set of all values. A program contains a finite set of program variables denoted by $x$ , $x_{i}$ , $y$ , or $z$ . We further assume a set of built-in functions $g$ . We assume that functions $g$ are total and return $\mathtt{null}$ for erroneous inputs. The only non-standard construct in the language are sample statements. For sample statements, the expression $E_{0}$ corresponds to the user-defined sample address, which is assumed to evaluate to a string. The symbol $f$ ranges over a set of built-in distributions which are parameterised by arguments $E_{1},\dots,E_{n}$ .
| Syntax of Expressions: | | |
| --- | --- | --- |
| $E::=$ | | expression |
| $c$ | | constant |
| $x$ | | variable |
| $g(E_{1},\dots,E_{n})$ | | function call |
| Syntax of Statements: | | |
| --- | --- | --- |
| $S::=$ | | statement |
| $x=E$ | | assignment |
| $S_{1};S_{2}$ | | sequence |
| $$ | | if statement |
| skip | | skip |
| $$ | | while loop |
| $$ | | sample |
### 2.1. Operational Semantics
The meaning of a program is the density implicitly defined by its sample statements. This density is evaluated for a program trace and returns a real number. A program trace is a mapping from finite-length addresses to numeric values, $\mathtt{tr}\colon\mathbf{Strings}\to\mathcal{V}$ . We denote the set of all traces with $\mathcal{T}$ . How the value at an address is determined is not important for this work and in practice typically depends on the algorithm that is used to perform posterior inference for the program. For instance, if an address $\alpha$ corresponds to an observed variable, the value $\mathtt{tr}(\alpha)$ is fixed to the data. If an address $\alpha$ does not appear in a program, then its value can be assumed to be $\mathtt{tr}(\alpha)=\mathtt{null}$ .
For each trace $\mathtt{tr}$ , the operational semantics of our language are defined by the big-step relation $(\sigma,S)\Downarrow^{\mathtt{tr}}\sigma^{\prime}$ , where $S$ is a statement and $\sigma\in\Sigma$ is a program state – a finite map from program variables to values
$$
\sigma::=x_{1}\mapsto V_{1},\dots,x_{n}\mapsto V_{n},\quad\,x_{i}\;\text{distinct},\;V_{i}\in\mathcal{V}.
$$
A state can be naturally lifted to a map from expressions to values $\sigma\colon\mathbf{Exprs}\to\mathcal{V}$ :
$$
\sigma(x_{i})=V_{i},\quad\sigma(c)=c,\quad\sigma(g(E_{1},\dots,E_{n}))=g(\sigma(E_{1}),\dots,\sigma(E_{n})).
$$
The operational semantics for the non-probabilistic part of our language are standard:
Above, $\sigma[x\mapsto V]$ denotes the updated program state $\sigma^{\prime}$ , where $\sigma^{\prime}(x)=V$ and $\sigma^{\prime}(y)=\sigma(y)$ for all other variables $y\neq x$ . The inference rules are to be interpreted inductively such that the semantics of a while loop can be rewritten as
| | $$ | $\displaystyle\exists n\in\mathbb{N}_{0}\colon\left((\sigma,\textnormal{repeat}_{n}(S))\Downarrow^{\mathtt{tr}}\sigma^{\prime}\land\sigma^{\prime}(E)=\mathtt{false}\right)\land$ | | |
| --- | --- | --- | --- | --- |
| $\displaystyle\quad\forall m<n\colon\left((\sigma,\textnormal{repeat}_{m}(S))\Downarrow^{\mathtt{tr}}\sigma^{\prime}_{m}\land\sigma^{\prime}_{m}(E)=\mathtt{true}\right),$ | | | | |
where $\textnormal{repeat}_{n}(S)=(S;...;S)$ repeated $n$ -times. In particular, if a while loop does not terminate for state $\sigma$ then $$ . This makes the presented operational semantics partial, where errors and non-termination are modelled implicitly. Formally, $\Downarrow^{\mathtt{tr}}$ is the least-relation closed under the stated rules.
At sample statements, we inject the value of the trace at address $V_{0}={\sigma(E_{0})}$ . We multiply the density, represented by the reserved variable p, with the value of function $\textnormal{pdf}_{f}$ evaluated at $\mathtt{tr}(V_{0})$ . Note that the function $\textnormal{pdf}_{f}$ may be an arbitrary function to real values. However, in the context of probabilistic programming, we interpret $\textnormal{pdf}_{f}$ as the density function of distribution $f$ with values in $\mathbb{R}_{\geq 0}$ . Lastly, the value $\mathtt{tr}(V_{0})$ is stored in the program state at variable $x$ . The semantics of sample statements are summarised in the following rule:
Finally, the meaning of a program $S$ is defined as the mapping of trace to density. This definition is well-defined, because the semantics are deterministic for each trace. If a trace leads to errors or non-termination, then the density is undefined.
** Definition 0**
*The density of a program $S$ is the function $\bar{p}_{S}\colon\mathcal{T}\times\Sigma\to\mathbb{R}_{\geq 0}$ given by
$$
\bar{p}_{S}(\mathtt{tr},\sigma_{0})\coloneqq\begin{cases}\sigma(\textbf{p})&\text{if }\;\exists\,\sigma\in\Sigma\colon(\sigma_{0},S)\Downarrow^{\mathtt{tr}}\sigma\\
\textnormal{undefined}&\text{otherwise}\end{cases}
$$
For the initial program state $\sigma_{0}=(x_{1}\mapsto\mathtt{null},\dots,x_{n}\mapsto\mathtt{null},\textbf{p}\mapsto 1)$ , mapping all program variables to $\mathtt{null}$ , we define $p_{S}\colon\mathcal{T}\to\mathbb{R}_{\geq 0}$ with $p_{S}(\mathtt{tr})=\bar{p}_{S}(\mathtt{tr},\sigma_{0}).$*
Listing 1: Simple probabilistic program with stochastic branching.
⬇
p = sample ("p", Uniform (0,1))
x = sample ("x", Bernoulli (p))
if x == 1 then
y = sample ("y", Bernoulli (0.25))
else
z = sample ("z", Bernoulli (0.75))
Listing 2: Program of LABEL:lst:semantics rewritten with dynamic addresses.
⬇
p = sample ("p", Uniform (0,1))
x = sample ("x", Bernoulli (p))
if x == 1 then
addr = "y"; prob = 0.25;
else
addr = "z"; prob = 0.75;
r = sample (addr, Bernoulli (prob))
Consider the simple probabilistic program in LABEL:lst:semantics (Note that we slightly deviate from the formal syntax in listings for better readability). The density defined by our operational semantics is given below, where $\delta_{v}$ denotes the delta function whose value is 1 if $v$ equals $\mathtt{true}$ and 0 otherwise.
| | $\displaystyle p(\mathtt{tr})$ | $\displaystyle=\textnormal{pdf}_{\textnormal{Uniform}}(\mathtt{tr}(\textnormal{"p"});0,1)$ | |
| --- | --- | --- | --- |
As the addresses in LABEL:lst:semantics are constant and identical to the program variables, the program is well-described by many existing PPL semantics. However, in LABEL:lst:semantics2, we rewrite the program with dynamic addresses which results in the same above density. Most formal PPLs studied in prior work do not support user-defined addresses for sample statements and cannot interpret a program with three sample statements as a four-dimensional joint density. In contrast, address-based semantics like those of Lee et al. (2019) and Lew et al. (2023), denotationally modelling Pyro and Gen, respectively, correctly interpret the program with dynamic addresses. This is also true for our extensions of Gorinova et al. (2019). While closely related to the aforementioned denotational models, we opted for an operational approach to more directly model the implementations of imperative PPLs.
Listing 3: Program with random address.
⬇
n = sample ("n", Poisson (5))
x = sample ("x_" + str (n), Normal (0.,1.))
Listing 4: Program with while loop implementing a Geometric distribution.
⬇
b = true; i = 0;
while b do
i = i + 1
b = sample ("b_" + i, Bernoulli (0.25))
Note that probabilistic programs with dynamic addresses and while loops pose a significant theoretical challenge, because both cases easily lead to an unbounded number of addresses as can be seen in LABEL:lst:poisson and LABEL:lst:geometric.
### 2.2. Remark on a Measure-theoretic Interpretation
Even though it suffices to consider the explicit computation of the density of a probabilistic program in this work, a measure-theoretic interpretation of the presented operational semantics is still worth exploring. The density of a measure $\mu$ with respect to some reference measure $\nu$ is formally given by the Radon-Nikodym derivative $p$ such that $\mu(A)=\int_{A}p\;d\nu$ . Thus, the measure-theoretic interpretation of the operational semantics is described by a construction of a measure space of traces $(\mathcal{T},\Sigma_{\mathcal{T}},\nu)$ such that the density $p_{S}$ is measurable. Then, $\mu_{S}(A)=\int_{A}p_{S}\;d\nu$ is the measure denoted by the program $S$ . As our results do not rely on measure theoretic assumptions, we refer to Appendix C for a sketch of this measure space.
### 2.3. Remark on Conditioning
In the presented semantics conditioning is only supported via soft-constraints (Staton et al., 2016). This means that the input trace $\mathtt{tr}$ is assumed to be fixed to observed data at certain addresses. If those addresses are encountered during execution at sample statements the data likelihood is multiplied to $\sigma(\textbf{p})$ . Informally, the program density $p_{S}$ corresponds to the unnormalised posterior density. Again, a rigorous treatment of the normalisation of $p_{S}$ is not required for our results.
## 3. Static Factorisation for Programs Without Loops
The goal of this work is to statically find a factorisation of the density implicitly defined by a probabilistic program in terms of addresses. This static analysis will operate on the control-flow graph (CFG) of a program. We begin by considering programs without loops first and describe how we can formally translate such a program to its corresponding CFG. We will equip this CFG with semantics equivalent to the operational semantics of the original program. The following construction is fairly standard but necessary for formally verifying the correctness of the factorisation.
### 3.1. Control-Flow Graph
A CFG has five types of nodes: start, end, assign, branch, and join nodes. Branch nodes have two successor nodes, end nodes have no successor, all other nodes have one. Only join nodes have multiple predecessors. The CFG contains exactly one start node from which every other node is reachable. Further, it contains exactly one end node that is reachable from any other node. We describe the recursive translation rules for program $S$ as diagrams, which serve to convey the general idea of the construction. For a formal description see Appendix A. Sub-graphs are drawn by circular nodes. Branch and join nodes are drawn as diamond nodes, the latter filled black. Assign, start, and end nodes have rectangular shape. In text, branch nodes are written as $\text{Branch}(E)$ . Assign nodes are denoted with $\text{Assign}(x=E)$ and $$ .
- The CFG of a skip-statement, $$ , consists of only start and end node:
<details>
<summary>x1.png Details</summary>
### Visual Description
Icon/Small Image (106x19)
</details>
- The CFG of an assignment, $x=E$ , or sample statement $$ , is a sequence of start, assign, and end node:
<details>
<summary>x2.png Details</summary>
### Visual Description
Icon/Small Image (167x19)
</details>
<details>
<summary>x3.png Details</summary>
### Visual Description
Icon/Small Image (302x22)
</details>
- The CFG for a sequence of statements, $S=S_{1};S_{2}$ , is recursively defined by ”stitching together” the CFGs $G_{1}$ and $G_{2}$ of $S_{1}$ and $S_{2}$ :
<details>
<summary>x4.png Details</summary>
### Visual Description
Icon/Small Image (212x32)
</details>
- The CFG of an if statement, $$ , is also defined in terms of the CFGs of $S_{1}$ and $S_{2}$ together with a branch node $B=\textnormal{Branch}(E)$ and a join node $J$ :
<details>
<summary>x5.png Details</summary>
### Visual Description
## Diagram: Process Flow with Conditional Branching
### Overview
The image displays a simple process flow diagram or directed graph, illustrating a sequence that begins, undergoes a decision or evaluation point with two possible paths, and then converges to a conclusion. The diagram uses standard flowchart symbols: rectangles for start/end points, a diamond for a decision, circles for intermediate states or goals, and a filled diamond for a merge or termination point.
### Components/Axes
The diagram is composed of the following labeled nodes and connecting arrows, arranged horizontally from left to right:
1. **START Node**: A rectangle on the far left containing the text "START".
2. **Decision Node (E)**: A diamond shape to the right of START, labeled with the letter "E".
3. **Path Labels**: Two arrows originate from the right point of the "E" diamond:
* The upper arrow is labeled with the text "consequent".
* The lower arrow is labeled with the text "alternative".
4. **Intermediate Nodes (G₁ & G₂)**:
* The "consequent" arrow points to a circle labeled "G₁" (G with a subscript 1).
* The "alternative" arrow points to a circle labeled "G₂" (G with a subscript 2).
5. **Merge/Termination Node**: A solid black diamond shape is positioned to the right of the G₁ and G₂ circles. Both circles have arrows pointing to this black diamond.
6. **END Node**: A rectangle on the far right containing the text "END". An arrow points from the black diamond to this node.
### Detailed Analysis
* **Flow Direction**: The process flows unidirectionally from left to right.
* **Sequence**:
1. The process initiates at `START`.
2. It proceeds to a decision or evaluation point `E`.
3. At `E`, the path splits based on a condition:
* One path, labeled `consequent`, leads to state `G₁`.
* The other path, labeled `alternative`, leads to state `G₂`.
4. Regardless of whether `G₁` or `G₂` is reached, the flow converges at the subsequent black diamond node.
5. The process concludes at `END`.
### Key Observations
* **Symmetry**: The diagram is symmetric about the horizontal axis running through START, E, the black diamond, and END. The `G₁` and `G₂` branches are mirror images.
* **Symbol Semantics**: The use of a hollow diamond for `E` typically represents a decision point. The solid black diamond is less standard but often signifies a merge point, a synchronization barrier, or a terminal state in some notations.
* **Label Clarity**: All text is clear and legible. The subscripts in `G₁` and `G₂` are distinct.
### Interpretation
This diagram models a logical or procedural flow with a single bifurcation. The node `E` represents an evaluation or condition. The outcome of this evaluation determines which of two possible states or goals (`G₁` or `G₂`) is achieved. The labels "consequent" and "alternative" suggest that `G₁` is the expected or primary outcome following from `E`, while `G₂` is a secondary or fallback path.
The convergence at the black diamond before `END` indicates that both paths are valid and lead to the same termination point. This structure is common in algorithms, business process models, or state machines where a system can handle different scenarios but must reach a common conclusion. The diagram does not specify the nature of `E`, `G₁`, or `G₂`, serving as a generic template for a conditional process.
</details>
We denote the successor nodes of the branch node $B$ as $\textnormal{consequent}(B)$ and $\textnormal{alternative}(B)$ . Furthermore, we say the tuple $(B,J)$ is a branch-join pair and define $\text{BranchJoin}(G)$ to be the set of all branch-join pairs of $G$ . Lastly, let $\textnormal{condexp}(B)$ denote the conditional expression $E$ .
#### 3.1.1. CFG Semantics
For a control-flow graph $G$ we define the small-step semantics for a trace $\mathtt{tr}$ as a relation that models the transition from node to node depending on the current program state:
$$
(\sigma,N)\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime},N^{\prime})
$$
The semantics for the CFG of program $S$ are set-up precisely such that they are equivalent to the operational semantics of program $S$ . The transition rules depending on node type and program state are given below, where we denote the unique child of non-branch nodes $N$ in $G$ with successor(N):
$$
\frac{N=\text{START}\quad N^{\prime}=\text{successor}(N)}{(\sigma,N)\overset{\mathtt{tr}}{\longrightarrow}(\sigma,N^{\prime})}\quad\frac{N=\text{Assign}(x=E)\quad N^{\prime}=\text{successor}(N)}{(\sigma,N)\overset{\mathtt{tr}}{\longrightarrow}(\sigma[x\mapsto\sigma(E)],N^{\prime})}
$$
$$
\frac{N=\text{Join}\quad N^{\prime}=\text{successor}(N)}{(\sigma,N)\overset{\mathtt{tr}}{\longrightarrow}(\sigma,N^{\prime})}\,\frac{N=\text{Branch}(E)\quad\sigma(E)=\mathtt{true}}{(\sigma,N)\overset{\mathtt{tr}}{\longrightarrow}(\sigma,\text{consequent}(N))}\,\frac{N=\text{Branch}(E)\quad\sigma(E)=\mathtt{false}}{(\sigma,N)\overset{\mathtt{tr}}{\longrightarrow}(\sigma,\text{alternative}(N))}
$$
Finally, the meaning of a CFG is a mapping from trace to density. It is defined for traces $\mathtt{tr}$ if there exists a path of node transitions from start to end node.
** Definition 0**
*The density of a CFG $G$ is the function $\bar{p}_{G}\colon\mathcal{T}\times\Sigma\to\mathbb{R}_{\geq 0}$ given by
$$
\bar{p}_{G}(\mathtt{tr},\sigma_{0})\coloneqq\begin{cases}\sigma(\textbf{p})&\text{if}\;\;\exists\;\sigma\in\Sigma,n\in\mathbb{N}\colon\forall i=1,\dots,n\colon\exists\;\sigma_{i},N_{i}\colon\\
&(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\dots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},N_{i})\overset{\mathtt{tr}}{\longrightarrow}\dots\overset{\mathtt{tr}}{\longrightarrow}(\sigma,\text{END})\\
\textnormal{undefined}&\text{otherwise.}\end{cases}
$$
For initial program state $\sigma_{0}$ as in Definition 1, we define $p_{G}\colon\mathcal{T}\to\mathbb{R}_{\geq 0}$ with $p_{G}(\mathtt{tr})=\bar{p}_{G}(\mathtt{tr},\sigma_{0}).$*
** Proposition 0**
*For all programs $S$ without while loops and corresponding control-flow graph $G$ , it holds that for all traces $\mathtt{tr}$ and all initial states $\sigma_{0}$
$$
{\bar{p}_{S}(\mathtt{tr},\sigma_{0})=\bar{p}_{G}(\mathtt{tr},\sigma_{0}).}
$$*
* Proof*
By structural induction. See Appendix B.1. ∎
### 3.2. Static Provenance Analysis
The provenance of variable $x$ in CFG node $N$ are all the addresses $\subseteq\mathbf{Strings}$ that contribute to the computation of its value in node $N$ . In this section, we define an algorithm that operates on the CFG and statically determines the provenance for any variable $x$ at any node $N$ . As this is a static algorithm, it is an over-approximation of the true provenance. In Section 3.2.1, we will prove soundness of the presented algorithm. We show that indeed the value of variable $x$ at node $N$ can be computed from the values in the trace $\mathtt{tr}$ at the addresses which make up the provenance. But first, we introduce some useful concepts which are similar to definitions found in data-flow analysis (Cooper and Torczon, 2011; Hennessy and Patterson, 2011).
** Definition 0**
*For a CFG $G$ , let $\textnormal{AssignNodes}(G,x)$ be all nodes $N^{\prime}$ in $G$ that assign variable $x$ , $N^{\prime}=\textnormal{Assign}(x=\dots)$ . The set of reaching definitions for variable $x$ in node $N$ is defined as
$$
\textnormal{RD}(N,x)=\{N^{\prime}\in\textnormal{AssignNodes}(G,x):\exists\text{ path }(N^{\prime},N_{1},\dots,N_{n},N),\;N_{i}\notin\textnormal{AssignNodes}(G,x)\}.
$$*
Intuitively, the set of reaching definitions are all nodes that could have written the value of $x$ in the program state before executing node $N$ .
** Definition 0**
*For CFG $G$ and node $N$ the set of branch parents is defined as
$$
\textnormal{BP}(N)=\{B:(B,J)\in\textnormal{BranchJoin}(G)\land\exists\text{ path }(B,\dots,N,\dots,J)\}.
$$
A branch node $B$ and join node $J$ are a branch-join pair $(B,J)\in\textnormal{BranchJoin}(G)$ if they belong to the same if-statement (see the translation rule for if-statements to CFGs).*
The set of branch parents are all parent branch nodes of $N$ that determine if the program branch that $N$ belongs to is executed.
Lastly, we define the set of all strings that the address expression of a sample statement may evaluate to.
** Definition 0**
*For a sample CFG node $$ , we define the set of all possible addresses as
$$
\textnormal{addresses}(N)=\{\sigma(E_{0}):\sigma\in\Sigma\}\subseteq\mathbf{Strings}.
$$*
Algorithm 1 Computing the provenance set $\textnormal{prov}(N,x)$ statically from the CFG.
1: Input CFG node $N$ , variable $x$
2: ${\textnormal{result}}\leftarrow\emptyset$
3: queue $\leftarrow[(N,x)]$
4: while queue is not empty do
5: $(N,x)$ $\leftarrow$ queue.pop()
6: for $N^{\prime}\in\textnormal{RD}(N,x)$ do
7: if $$ then
8: ${\textnormal{result}}\leftarrow{\textnormal{result}}\cup\text{addresses}(N^{\prime})$ $\rhd$ in practice: ${\textnormal{result}}\leftarrow{\textnormal{result}}\cup\{N^{\prime}\}$
9: $E^{\prime}\leftarrow E_{0}$ $\rhd$ $E_{0}$ comes from pattern-matching $N^{\prime}$
10: else if $N^{\prime}=\text{Assign}(x=E)$ then
11: $E^{\prime}\leftarrow E$ $\rhd$ $E$ comes from pattern-matching $N^{\prime}$
12: for $y\in\text{vars}(E^{\prime})$ do
13: if is_unmarked( $(N^{\prime},y)$ ) then
14: mark( $(N^{\prime},y)$ )
15: queue.push( $(N^{\prime},y)$ )
16: for $N_{\text{bp}}\in\textnormal{BP}(N^{\prime})$ $\rhd$ $N_{\text{bp}}=\text{Branch}(E_{N_{\text{bp}}})$ do
17: for $y\in\text{vars}(E_{N_{\text{bp}}})$ do
18: if is_unmarked( $(N_{\text{bp}},y)$ ) then
19: mark( $(N_{\text{bp}},y)$ )
20: queue.push( $(N_{\text{bp}},y)$ )
21: return result
Now we are able to define the algorithm to statically approximate the provenance of any variable $x$ at any node $N$ denoted by $\textnormal{prov}(N,x)$ in Algorithm 1. This algorithm is inspired by standard methods for dependence analysis. In the algorithm, we use $\textnormal{vars}(E)$ , which is defined as the set of all program variables in expression $E$ . It is often useful to determine the provenance of an entire expression instead of only a single variable. For expressions $E$ , we lift the definition of prov
$$
\textnormal{prov}(N,E)=\textstyle\bigcup_{y\in\textnormal{vars}(E)}\textnormal{prov}(N,y). \tag{3}
$$
The algorithm works as follows. If we want to find $\textnormal{prov}(N,x)$ , we first have to find all reaching definitions for $x$ . If the reaching definition $N^{\prime}$ is a sample node, $$ , then the value of $x$ can only depend on the addresses generated by $E_{0}$ , $\textnormal{addresses}(N^{\prime})$ , and the provenance of $E_{0}$ . If $N^{\prime}$ is an assignment node, $x=E$ , we have to recursively find the provenance of the expression $E$ . Lastly, there can be multiple reaching definitions for $x$ in different branches and the value of $x$ also depends on the branching condition. Thus, we also find all branch parents and recursively determine their provenance and add it to the final result.
In practice the potentially infinite set $\textnormal{addresses}(N)$ can be represented by the CFG node $N$ itself. As remarked on line 8, an implementation of Algorithm 1 would return a set of CFG sample nodes rather than a potentially infinite set of strings. If we call this version of the algorithm provnode, we have $\textnormal{prov}(N,x)=\bigcup_{N^{\prime}\in\textnormal{provnode}(N,x)}\textnormal{addresses}(N^{\prime})$ .
We get a clearer sense of the introduced definitions and Algorithm 1 by considering a simple program in Figure 1. The right panel shows the CFG with reaching definitions and branch parents for several nodes drawn as arrows. These arrows illustrate how Algorithm 1 computes the provenance of variables m and s at the sample node for address ”x”. Note that if we were to change the if statement to (if (b == 1) then (m = 1) else (m = 1)), then the address ”b” would still be in the provenance set of m. This illustrates that the presented algorithm can only over-approximate the provenance and not compute it exactly.
⬇
b = sample ("b", Bernoulli (0.5))
s = sample ("s", InverseGamma (1.,1.))
if b == 1 then
m = sample ("mu", Normal (0.,1.))
else
m = 1
x = sample ("x", Normal (m, s))
| | $\displaystyle N_{7}=\textnormal{Assign}(\mathtt{x}=\dots),\,\,V^{N_{7}}_{\mathtt{s}}(\mathtt{tr})=\mathtt{tr}(\textnormal{"s"}),$ | |
| --- | --- | --- |
<details>
<summary>x6.png Details</summary>
### Visual Description
## Flowchart Diagram: Algorithmic Process Flow with Conditional Branching
### Overview
The image displays a vertical flowchart diagram representing an algorithmic or computational process. The flowchart consists of eight rectangular nodes (labeled N1 through N8) connected by directional arrows, indicating the sequence of operations. The process includes a conditional decision point (N4) that creates two distinct branches, which later converge. The diagram uses color-coded arrows (orange and blue) to differentiate between two proof or validation paths, as indicated by a legend in the bottom-right corner.
### Components/Axes
* **Nodes (Process Steps):** Eight rectangular boxes, each labeled with an identifier (N1 to N8) and containing a brief instruction or variable assignment.
* **Flow Arrows:** Directional lines connecting the nodes. They are primarily black, but two specific paths are highlighted in orange and blue.
* **Legend:** Located in the bottom-right quadrant. It defines the meaning of the colored arrows:
* Orange line: `prov(N7, m) = "T"`
* Blue line: `prov(N7, m) = "F"`
* **Spatial Layout:** The flowchart is arranged vertically from top (N1: START) to bottom (N8: END). The conditional branch at N4 creates a horizontal split, with the left path (blue arrow) leading to N5 and the right path (orange arrow) leading to N6. The legend is positioned to the right of the main flow, adjacent to the converging paths from N5 and N6.
### Detailed Analysis
**Node-by-Node Content:**
* **N1 (Top):** `START`
* **N2:** `b = ...` (An initialization or assignment for variable `b`)
* **N3:** `s = ...` (An initialization or assignment for variable `s`)
* **N4 (Decision):** `b = 1` (A conditional check. Two arrows exit this node):
* **Left (Blue Arrow):** Labeled `RD(N7, b)`. Leads to node N5.
* **Right (Orange Arrow):** Labeled `RD(N7, b)`. Leads to node N6.
* **N5 (Left Branch):** `m = 1`
* **N6 (Right Branch):** `m = ...` (An assignment for variable `m`)
* **Convergence Point:** Arrows from N5 and N6 merge before entering N7.
* **N7:** `x = ...` (An assignment for variable `x`)
* **N8 (Bottom):** `END`
**Arrow Labels and Paths:**
* A **blue arrow** originates from the left side of N7, loops back upwards, and points to the left side of N2. It is labeled `RD(N7, b)`.
* An **orange arrow** originates from the right side of N7, loops back upwards, and points to the right side of N2. It is labeled `RD(N7, b)`.
* The legend clarifies that the **blue path** (from the left branch at N4 through N5) corresponds to the condition `prov(N7, m) = "F"` (False).
* The legend clarifies that the **orange path** (from the right branch at N4 through N6) corresponds to the condition `prov(N7, m) = "T"` (True).
### Key Observations
1. **Conditional Logic:** The core of the process is the decision at N4 (`b = 1`). The outcome of this check determines whether the process follows the left path (setting `m = 1`) or the right path (setting `m = ...`).
2. **Looping Structure:** The process contains a loop. After executing N7 (`x = ...`), control flow returns to N2 (`b = ...`) via either the blue or orange feedback arrow, suggesting an iterative process.
3. **Color-Coded Proof States:** The diagram explicitly links the choice of branch (left/right at N4) to a resulting proof state (`prov(N7, m)`) for variable `m`. The left branch leads to a "False" proof state, and the right branch leads to a "True" proof state.
4. **Ambiguous Assignments:** Several nodes (N2, N3, N6, N7) contain ellipses (`...`), indicating that the specific values or expressions assigned to variables `b`, `s`, `m`, and `x` are not defined in this diagram. They are placeholders for operations to be specified elsewhere.
### Interpretation
This flowchart models a **conditional iterative algorithm** where the internal state (specifically the value of `b`) determines the computational path taken in each loop iteration. The key investigative insight is the relationship between the conditional check (`b = 1`), the assignment to `m`, and the resulting "proof" value `prov(N7, m)`.
The diagram suggests that:
* The system is designed to test a condition (`b = 1`).
* Based on the test, it sets `m` to a specific value (`1` or another value).
* This choice of `m` later results in a verifiable outcome (`"T"` or `"F"`) at the stage represented by N7.
* The process then repeats, using updated values for `b` and `s`.
The presence of the `prov` function and the `RD` labels (which may stand for "Read" or "Reduction") implies this could be a diagram from formal methods, program verification, or a logical proof system, where the flowchart tracks both the execution of an algorithm and the state of a corresponding proof or validation condition. The loop indicates the algorithm may run until a certain condition is met, with the proof state being tracked across iterations.
</details>
Figure 1. Reaching definitions, branch parents, and the provenance set for a simple example. The evaluation functions introduced in Section 3.2.1 are also given for node $N$ .
#### 3.2.1. Soundness
Recall that the purpose of finding the provenance of variable $x$ at node $N$ is to determine which addresses contribute to the computation of its value. To prove that Algorithm 1 indeed finds the correct set of addresses, first, we have to precisely define what we mean that a set of addresses contribute to the computation. Suppose that there is a function $f$ that maps a trace $\mathtt{tr}$ to a value $v$ . The set of addresses $A$ contribute to the computation of value $v$ , if any other trace $\mathtt{tr}^{\prime}$ that has the same values as $\mathtt{tr}$ for all addresses $\alpha\in A$ , gets mapped to the same value $f(\mathtt{tr}^{\prime})=v$ . In other words, if we change the trace $\mathtt{tr}$ at an address $\beta\in\mathbf{Strings}\setminus A$ , the value of $f(\mathtt{tr})$ remains unchanged.
** Definition 0**
*For a function from traces to an arbitrary set $B$ , $f:\mathcal{T}\to B$ , we write $f\in[\mathcal{T}|_{A}\to B]$ for a subset of addresses $A\subseteq\mathbf{Strings}$ , if and only if
$$
\forall\alpha\in A\colon\mathtt{tr}(\alpha)=\mathtt{tr}^{\prime}(\alpha)\implies f(\mathtt{tr})=f(\mathtt{tr}^{\prime}).
$$
That is, changing the values of $\mathtt{tr}$ at addresses $\beta\in\mathbf{Strings}\setminus A$ does not change the value $f(\mathtt{tr})$ .*
The next lemma states that we can always over-approximate the set of addresses that contribute to the computation of the values $f(\mathtt{tr})$ .
** Lemma 0**
*If $A\subseteq A^{\prime}$ and $f\in[\mathcal{T}|_{A}\to B]$ , then $f\in[\mathcal{T}|_{A^{\prime}}\to B]$ . In other words,
$$
A\subseteq A^{\prime}\implies[\mathcal{T}|_{A}\to B]\subseteq[\mathcal{T}|_{A^{\prime}}\to B]. \tag{4}
$$*
If we combine two functions with provenance $A_{1}$ and $A_{2}$ respectively, then the resulting function has provenance $A_{1}\cup A_{2}$ . This is shown in the following lemma.
** Lemma 0**
*Let $f_{1}\in[\mathcal{T}|_{A_{1}}\to B_{1}]$ , $f_{2}\in[\mathcal{T}|_{A_{2}}\to B_{2}]$ , $h\colon B_{1}\times B_{2}\to C$ . Then
$$
\mathtt{tr}\mapsto h(f_{1}(\mathtt{tr}),f_{2}(\mathtt{tr}))\in[\mathcal{T}|_{A_{1}\cup A_{2}}\to C].
$$*
This brings us to the main soundness result of Algorithm 1. Proposition 9 states that we can equip each CFG node $N$ with evaluation functions that depend on the addresses determined by prov in the sense of Definition 6. The evaluation functions directly map the trace $\mathtt{tr}$ to the values of variables at node $N$ such that the values agree with the small-step CFG semantics relation $\overset{\mathtt{tr}}{\longrightarrow}$ . Importantly, while the operational semantics are defined for each individual trace, the evaluation functions work for all traces. In Fig. 1, concrete examples of these evaluation functions for a simple program can be found.
** Proposition 0**
*Let $G$ be the CFG of a program $S$ without while loop statements. For each node $N$ and variable $x$ , there exists an evaluation function
$$
V^{N}_{x}\in[\mathcal{T}|_{\textnormal{prov}(N,x)}\to\mathcal{V}],
$$
such that for all traces $\mathtt{tr}$ , initial program state $\sigma_{0}$ as in Definition 1, and execution sequence
$$
(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},N_{i})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{l},\text{END})
$$
we have
$$
\sigma_{i}(x)=V^{N_{i}}_{x}(\mathtt{tr}).
$$*
* Proof*
The CFG $G$ of a program without while loops is a directed acyclic graph and the statement is proven by induction on $G$ . See Appendix B.2. ∎
Intuitively, $V^{N}_{x}$ computes the value of $x$ before executing $N$ . These evaluation functions $V^{N}_{x}$ can be lifted to evaluation functions for expressions $V^{N}_{E}$ :
$$
V^{N}_{c}(\mathtt{tr})=c,\quad V^{N}_{g(E_{1},\dots,E_{n})}(\mathtt{tr})=g(V^{N}_{E_{1}}(\mathtt{tr}),\dots,V^{N}_{E_{n}}(\mathtt{tr})).
$$
By Lemma 8, if $V^{N}_{y}\in[\mathcal{T}|_{\textnormal{prov}(N,y)}\to\mathcal{V}]$ for all $y\in\textnormal{vars}(E)$ , then $V^{N}_{E}\in[\mathcal{T}|_{\textnormal{prov}(N,E)}\to\mathcal{V}]$ .
### 3.3. Static Factorisation Theorem for Programs Without Loops
With Proposition 9, we can prove the first factorisation theorem by combining the evaluation functions $V^{N}_{x}$ to express the program density $p$ in a factorised form.
** Theorem 10**
*Let $G$ be the CFG for a program $S$ without while loop statements. Let $N_{1},\dots,N_{K}$ be all sample nodes in $G$ . For each sample node $$ , let
$$
A_{k}=\textnormal{addresses}(N_{k})\cup\textstyle\bigcup_{i=0}^{n_{k}}\textnormal{prov}(N_{k},E_{i}^{k})\cup\textstyle\bigcup_{N^{\prime}\in\textnormal{BP}(N_{k})}\textnormal{prov}(N^{\prime},{\textnormal{condexp}(N^{\prime})}).
$$
Then, there exist functions $p_{k}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}]$ such that for all $\mathtt{tr}\in\mathcal{T}$ , if $p_{S}(\mathtt{tr})\neq\textnormal{undefined}$ , then
$$
p_{S}(\mathtt{tr})=p_{G}(\mathtt{tr})=\prod_{k=1}^{K}p_{k}(\mathtt{tr}).
$$*
* Proof*
For each sample node $N_{k}$ , define $b_{k}(\mathtt{tr})\coloneqq\bigwedge_{N^{\prime}\in\textnormal{BP}(N_{k})}t^{k}_{N^{\prime}}(V^{N^{\prime}}_{{\textnormal{condexp}(N^{\prime})}}(\mathtt{tr}))$ where $t^{k}_{N^{\prime}}(v)=v$ if $N_{k}$ is in the consequent branch of $N^{\prime}$ and $t^{k}_{N^{\prime}}(v)=\neg v$ if $N_{k}$ is in the alternate branch. By Lemma 8, we have $b_{k}\in[\mathcal{T}|_{\textstyle\bigcup_{N^{\prime}\in\textnormal{BP}(N_{k})}\textnormal{prov}(N^{\prime},\textnormal{condexp}(N^{\prime}))}\to\{\mathtt{true},\mathtt{false}\}].$ Here, $V^{N^{\prime}}_{\textnormal{condexp}(N^{\prime})}(\mathtt{tr})$ are precisely the evaluations of the branch conditions for node $N_{k}$ . Thus, $b_{k}(\mathtt{tr})$ is $\mathtt{true}$ if $N_{k}$ is in the execution sequence for $\mathtt{tr}$ else $\mathtt{false}$ . Define the factor $p_{k}$ as
$$
p_{k}(\mathtt{tr})\coloneqq\delta_{b_{k}(\mathtt{tr})}\textnormal{pdf}_{f^{k}}\left(\mathtt{tr}(V^{N_{k}}_{E_{0}^{k}}(\mathtt{tr}));V^{N_{k}}_{E_{1}^{k}}(\mathtt{tr}),\dots,V^{N_{k}}_{E_{n_{k}}^{k}}(\mathtt{tr})\right)+(1-\delta_{b_{k}(\mathtt{tr})}). \tag{5}
$$
By Proposition 9, $V^{N_{k}}_{E_{i}^{k}}\in[\mathcal{T}|_{\textnormal{prov}(N_{k},E_{i}^{k})}\to\mathcal{V}]$ and $V^{N_{k}}_{E_{0}^{k}}\in[\mathcal{T}|_{\textnormal{prov}(N_{k},E_{0}^{k})}\to\textnormal{addresses}(N_{k})]$ . Thus, it follows from Lemma 8 that $p_{k}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}]$ by construction. Lastly, from Proposition 9 we know that for the end-state $\sigma_{l}(\textbf{p})=V^{\text{END}}_{\textbf{p}}(\mathtt{tr})=p_{G}(\mathtt{tr})$ . Since $b_{k}(\mathtt{tr})=\mathtt{true}$ if and only if $N_{k}$ is in the execution sequence for $\mathtt{tr}$ and since the $\textnormal{pdf}_{f^{k}}(\dots)$ term in (5) is precisely the value that gets multiplied to p at sample statements (1), we have $p_{G}(\mathtt{tr})=\prod_{k=1}^{K}p_{k}(\mathtt{tr})$ . ∎
Again, consider the example program in Fig. 1. The density of this model factorises like below:
| | $\displaystyle p(\mathtt{tr})=\textnormal{pdf}_{\text{Bernoulli}}(\mathtt{tr}(\textnormal{"b"});0.5)$ | $\displaystyle\in[\mathcal{T}|_{\{\textnormal{"b"}\}}\to\mathbb{R}_{\geq 0}]$ | |
| --- | --- | --- | --- |
This is exactly the factorisation obtained from Theorem 10. However, if we would replace the if-statement with a nonsensical one, (if (b == 1) then (m = 1) else (m = 1)), then the fourth factor is in $[\mathcal{T}|_{\{\textnormal{"x"},\textnormal{"b"},\textnormal{"s"}\}}\to\mathbb{R}_{\geq 0}]$ with $V^{N_{7}}_{\mathtt{m}}(\mathtt{tr})=\textnormal{ife}(\mathtt{tr}(\textnormal{"b"}),1,1)=1$ , where we use ife as a short-hand for the if-else case distinction. In this case, the static analysis over-approximates the true provenance with the spurious dependency on ”b”.
#### 3.3.1. Equivalence to Bayesian Networks
If we restrict the way sample statements are used in our PPL, we can establish a known equivalence to Bayesian networks. A Bayesian network (Koller and Friedman, 2009) is a directed acyclic graph $\mathcal{G}$ over a finite set of nodes $X_{1},\dots,X_{n}$ which represent random variables, such that the joint distribution factorises according to the graph $\mathcal{G}$ ,
$$
P(X_{1},\dots,X_{n})=\prod_{i=1}^{n}P(X_{i}\;|\;\textnormal{parents}_{\mathcal{G}}(X_{i})).
$$
If we assume that all sample statements of a program have a constant unique address $\alpha_{k}$ , $$ , then we can identify each factor $p_{k}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}]$ of Theorem 10 with the unique address $\alpha_{k}\in\mathbf{Strings}$ . We construct the Bayesian network $\mathcal{G}$ by mapping each address to a random variable $X_{\alpha_{k}}$ . Since $\alpha_{k}$ is unique, $p_{k}$ is the only relevant factor for $X_{\alpha_{k}}$ and can be interpreted as conditional density function of $X_{\alpha_{k}}$ . To see this, rewrite
$$
p_{k}(\mathtt{tr})=\delta_{b_{k}(\mathtt{tr})}\textnormal{pdf}_{f^{k}}\left(\mathtt{tr}(\alpha_{k});V^{N_{k}}_{E_{1}^{k}}(\mathtt{tr}),\dots,V^{N_{k}}_{E_{n_{k}}^{k}}(\mathtt{tr})\right)+(1-\delta_{b_{k}(\mathtt{tr})})\mathbf{1}_{\mathtt{null}}\left(\mathtt{tr}(\alpha_{k})\right),
$$
where the function $\mathbf{1}_{\mathtt{null}}(v)$ equals 1 if $v=\mathtt{null}$ else 0. If the node $N_{k}$ is not executed, then the value of $X_{\alpha_{k}}$ is assumed to be $\mathtt{null}$ and we add the $\mathbf{1}_{\mathtt{null}}\left(\mathtt{tr}(\alpha_{k})\right)$ term to $p_{k}$ . As $\textnormal{pdf}_{f_{k}}$ is a probability density function and $\mathbf{1}_{\mathtt{null}}$ is the density of a Dirac distribution centered at $\mathtt{null}$ , the factor $p_{k}$ is also a density function for each choice of values in $\mathtt{tr}$ at addresses $\alpha\in A_{k}\setminus\{\alpha_{k}\}$ . Thus, we introduce the edge $\alpha_{j}\to\alpha_{k}$ if $\alpha_{j}\in A_{k}\setminus\{\alpha_{k}\}$ , such that $\textnormal{parents}_{\mathcal{G}}(X_{\alpha_{k}})=A_{k}\setminus\{\alpha_{k}\}$ and
$$
P(X_{\alpha_{k}}\,|\,\textnormal{parents}_{\mathcal{G}}(X_{\alpha_{k}}))=p_{k}(\{\alpha\mapsto X_{\alpha}\colon\alpha\in A_{k}\}).
$$
In the above construction, it is important that each sample statement has a unique address. This guarantees no cyclic dependencies and a well-defined conditional probability distributions.
The Bayesian network equivalent to the example program of Fig. 1 is drawn below. Since the value of the program variable $\mathtt{m}$ depends on which program branch is taken during execution, the random variable $X_{\textnormal{"x"}}$ not only depends on $X_{\textnormal{"mu"}}$ , but also on $X_{\textnormal{"b"}}$ .
<details>
<summary>x7.png Details</summary>
### Visual Description
\n
## Directed Graph Diagram: Input-Output Relationship
### Overview
The image displays a simple directed graph (or flowchart) consisting of four nodes connected by directional arrows. The diagram illustrates a relationship where three distinct input elements converge to influence or produce a single output element. The structure is minimal, with no additional annotations, scales, or numerical data.
### Components/Axes
The diagram contains the following labeled components:
1. **Node "s"**: A circular node located in the top-left region of the diagram.
2. **Node "b"**: A circular node located in the top-center region.
3. **Node "mu"**: An oval-shaped node located in the top-right region. The label is written as `"mu"`.
4. **Node "x"**: A circular node located in the bottom-center region, serving as the convergence point.
**Connections (Arrows):**
* A directed arrow originates from node **"s"** and points to node **"x"**.
* A directed arrow originates from node **"b"** and points to node **"x"**.
* A directed arrow originates from node **"mu"** and points to node **"x"**.
### Detailed Analysis
The diagram is purely structural. It defines a system where:
* **Inputs:** The elements labeled `"s"`, `"b"`, and `"mu"` are all inputs or independent variables.
* **Output:** The element labeled `"x"` is the output or dependent variable.
* **Flow:** The flow of influence or causation is unidirectional, from the top row of nodes (`s`, `b`, `mu`) to the single bottom node (`x`). There are no feedback loops or connections between the input nodes themselves.
### Key Observations
* **Node Shape:** Three nodes (`s`, `b`, `x`) are represented as circles, while one (`mu`) is an oval. This could imply a categorical difference (e.g., `mu` might represent a parameter or a different type of variable).
* **Spatial Layout:** The inputs are arranged horizontally at the top, and the output is centered below them, creating a clear visual hierarchy of cause (top) and effect (bottom).
* **Simplicity:** The diagram contains no quantitative information, weights, or functional relationships. It only establishes connectivity.
### Interpretation
This diagram represents a fundamental **many-to-one relationship** or a **confluence model**. It suggests that the state or value of `"x"` is determined by the combined influence of `"s"`, `"b"`, and `"mu"`.
* **What it demonstrates:** It is a conceptual model for processes where multiple factors contribute to a single outcome. Common interpretations in technical fields could include:
* **Statistics/ML:** A linear model where `x = f(s, b, mu)`, with `s` and `b` as predictors and `mu` as a mean parameter or bias term.
* **Control Systems:** A system where the output `x` is controlled by three separate input signals.
* **Causal Modeling:** A directed acyclic graph (DAG) showing that `s`, `b`, and `mu` are direct causes of `x`.
* **Notable Absence:** The diagram does not specify the *nature* of the relationship (additive, multiplicative, etc.) or the relative importance of each input. The identical arrow styles suggest equal qualitative standing, but no quantitative weighting is implied.
* **Purpose:** The primary purpose is to visually communicate the architecture of dependency—that `x` is a function of three distinct elements—without specifying the function itself. It serves as a high-level schematic for further detailed modeling.
</details>
$\displaystyle P(X_{\textnormal{"b"}})$ $\displaystyle=\textnormal{pdf}_{\textnormal{Bernoulli}}(X_{\textnormal{"b"}};0.5)$ $\displaystyle P(X_{\textnormal{"s"}})$ $\displaystyle=\textnormal{pdf}_{\textnormal{InverseGamma}}(X_{\textnormal{"s"}};1,1)$ $\displaystyle P(X_{\textnormal{"mu"}}|X_{\textnormal{"b"}})$ $\displaystyle=\delta_{X_{\textnormal{"b"}}}\textnormal{pdf}_{\text{Normal}}(X_{\textnormal{"mu"}};0,1)+(1-\delta_{X_{\textnormal{"b"}}})\mathbf{1}_{\mathtt{null}}(X_{\textnormal{"mu"}})$ $\displaystyle P(X_{\textnormal{"x"}}|X_{\textnormal{"b"}},X_{\textnormal{"mu"}},X_{\textnormal{"s"}})$ $\displaystyle=\textnormal{pdf}_{\textnormal{Normal}}(X_{\textnormal{"x"}};\textnormal{ife}(X_{\textnormal{"b"}},X_{\textnormal{"mu"}},1),X_{\textnormal{"s"}})$
#### 3.3.2. Equivalence to Markov Networks
If the sample addresses are not unique or not constant, then the factorisation is in general not a Bayesian network. However, we can show equivalence to Markov networks. A Markov network (Koller and Friedman, 2009) is an undirected graph $\mathcal{H}$ over random variables $\vv{X}$ that represents their dependencies. We consider Markov networks where the joint distribution of $\vv{X}$ factorises over a set of cliques $\mathcal{D}=\{D_{1},\dots,D_{n}\}\subseteq\textnormal{cliques}(\mathcal{H})$ , with $\bigcup_{i=1}^{n}D_{i}=\vv{X}$ :
$$
P(\vv{X})=\prod_{i=1}^{n}\phi_{i}(D_{i}).
$$
We again identify a random variable $X_{\alpha}$ for each address $\alpha\in\textstyle\bigcup_{k=1}^{K}A_{k}$ and construct a Markov network $\mathcal{H}$ by connecting node $X_{\alpha}$ to $X_{\beta}$ if $\alpha\in A_{k}\land\beta\in A_{k}$ for any $k$ . Thus, $D_{k}=\{X_{\alpha}\colon\alpha\in A_{k}\}$ forms a clique and $p_{S}$ factorises over $\mathcal{H}$ with $\phi_{k}(D_{k})=p_{k}(\{\alpha\mapsto X_{\alpha}\colon\alpha\in A_{k}\})$ .
Consider the program with constant but non-unique sample addresses in LABEL:lst:hurricane1. With nine sample statements we get a Markov network over $\{X_{\textnormal{"F"}},X_{\textnormal{"P0"}},X_{\textnormal{"P1"}},X_{\textnormal{"D0"}},X_{\textnormal{"D1"}}\}$ . The nine factors correspond to the address sets $\{\textnormal{"F"}\}$ , $\{\textnormal{"F"},\textnormal{"P0"}\}$ , $\{\textnormal{"F"},\textnormal{"P1"}\}$ , $\{\textnormal{"F"},\textnormal{"D0"},\textnormal{"P1"}\}$ , $\{\textnormal{"F"},\textnormal{"D1"},\textnormal{"P0"}\}$ , $2\times\{\textnormal{"F"},\textnormal{"P0"},\textnormal{"D0"}\}$ , and $2\times\{\textnormal{"F"},\textnormal{"P1"},\textnormal{"D1"}\}$ . In the consequent branch of the program, the distribution in the sample statement with address ”P1” depends on ”D0”, while in the alternative branch, the distribution of ”P0” depends on ”D1”. Thus, there is the dependency cycle $\textnormal{"P0"}\to\textnormal{"D0"}\to\textnormal{"P1"}\to\textnormal{"D1"}\to\textnormal{"P0"}$ , which means the obtained factorisation is not a Bayesian network representation for the program. Note that the program can also be rewritten with dynamic addresses to eliminate the if statement. In this case, the factorisation still admits cyclic dependencies.
Listing 5: Probabilisitic program for the hurricane example of (Milch et al., 2005).
⬇
first_city_ixs = sample ("F", Bernoulli (0.5))
if first_city_ixs == 0 then
prep_0 = sample ("P0", Bernoulli (0.5))
damage_0 = sample ("D0", Bernoulli (prep_0 == 1 ? 0.20 : 0.80))
prep_1 = sample ("P1", Bernoulli (damage_0 == 1 ? 0.75 : 0.50))
damage_1 = sample ("D1", Bernoulli (prep_1 == 1 ? 0.20 : 0.80))
else
prep_1 = sample ("P1", Bernoulli (0.5))
damage_1 = sample ("D1", Bernoulli (prep_1 == 1 ? 0.20 : 0.80))
prep_0 = sample ("P0", Bernoulli (damage_1 == 1 ? 0.75 : 0.50))
damage_0 = sample ("D0", Bernoulli (prep_0 == 1 ? 0.20 : 0.80))
Lastly, while the programs considered up until this point were equivalent to finite Bayesian networks or finite Markov networks, note that the small program in LABEL:lst:poisson is equivalent to a Markov network with an infinite number of nodes $\{X_{\textnormal{"n"}}\}\cup\{X_{\textnormal{"x}\_i\textnormal{"}}\colon i\in\mathbb{N}\}$ .
## 4. Static Factorisation for Programs With Loops
In this section, we describe how the argument for proving the factorisation theorem for programs without loops, can be extended to generalise the result to programs with loops.
### 4.1. Unrolled Control-Flow Graph
The translation rules for programs to their CFG can be extended to support while loops as follows. Let $G_{S}$ be the sub-CFG of statement $S$ . The CFG of $$ is given below on the left:
<details>
<summary>x8.png Details</summary>
### Visual Description
\n
## Control Flow Diagram: CFG G
### Overview
The image displays a simple control flow graph (CFG) labeled "CFG G:". It is a directed graph consisting of four nodes connected by edges, representing the flow of control in a program or process. The diagram uses standard flowchart symbols to denote different types of operations or states.
### Components/Axes
The diagram is composed of the following labeled nodes and connecting edges:
**Nodes (Shapes and Labels):**
1. **START Node:** A rectangle labeled "START". Positioned at the far left of the diagram.
2. **Decision Node (E):** A diamond shape labeled "E". Positioned in the center of the diagram.
3. **Process/Loop Node (G5):** A circle labeled "G5". Positioned directly above the diamond node "E".
4. **END Node:** A rectangle labeled "END". Positioned at the far right of the diagram.
**Edges (Flow Direction):**
* A directed arrow flows from the right side of the "START" node to the left point of the diamond "E" node.
* A directed arrow flows from the right point of the diamond "E" node to the left side of the "END" node.
* A directed arrow flows from the top point of the diamond "E" node upward to the bottom of the circle "G5" node.
* A directed arrow flows from the right side of the circle "G5" node, curves downward, and connects to the top point of the diamond "E" node.
### Detailed Analysis
The graph defines a specific control flow structure:
1. **Entry Point:** Execution begins at the "START" node.
2. **Decision Point:** Control flows unconditionally to node "E". The diamond shape indicates this is a decision or conditional branch point.
3. **Paths from Decision Node "E":**
* **Path 1 (Forward):** One edge leads directly from "E" to the "END" node. This represents the path taken when the condition at "E" evaluates to a certain outcome (e.g., false, exit condition met).
* **Path 2 (Loop):** Another edge leads from "E" to node "G5". An edge then returns from "G5" back to "E". This creates a cycle or loop: `E -> G5 -> E`. This represents a path where a block of code (G5) is executed repeatedly as long as the condition at "E" evaluates to a different outcome (e.g., true, continue condition).
4. **Exit Point:** The only exit from the structure is via the edge from "E" to "END".
### Key Observations
* **Single Entry, Single Exit:** The graph has one entry point ("START") and one exit point ("END"), which is a common and well-structured pattern for a control flow region.
* **Loop Structure:** The cycle `E -> G5 -> E` forms a classic "while" or "repeat-until" loop structure. Node "G5" represents the loop body.
* **Decision Node Centrality:** Node "E" is the central hub of the graph. All control flow passes through it, and it determines whether to exit the structure or execute the loop body (G5).
* **Node Type Conventions:** The shapes follow common conventions: rectangles for start/end terminals, a diamond for a decision, and a circle for a process or basic block within a loop.
### Interpretation
This control flow graph represents a fundamental programming construct: a **loop with a pre-test condition**.
* **What it demonstrates:** The diagram models a process where a condition ("E") is checked. If the condition is met (e.g., a loop counter is within bounds, a flag is set), the process block ("G5") is executed, and the condition is re-evaluated. This cycle repeats until the condition at "E" is no longer met, at which point the process exits to "END".
* **Relationship between elements:** "START" initiates the process. "E" acts as the gatekeeper, controlling iteration. "G5" is the work performed during each iteration. "END" signifies completion. The arrows strictly define the permissible transitions between these states.
* **Notable patterns:** The structure is a canonical representation of a `while (E) { G5 }` loop in imperative programming. The absence of a direct path from "START" to "G5" confirms it is a pre-test loop; the condition is checked before the first execution of the loop body. There are no outliers or anomalies; the graph is a clean, textbook example of a single-exit loop structure.
</details>
<details>
<summary>x9.png Details</summary>
### Visual Description
## Control Flow Diagram: Unrolled CFG H
### Overview
The image displays a technical diagram representing an unrolled Control Flow Graph (CFG), labeled "unrolled CFG H:". It illustrates the flow of execution through a series of nodes connected by directional arrows, depicting a program's control structure with loops and conditional branches. The diagram is monochromatic, using black lines and text on a white background.
### Components/Axes
The diagram consists of the following labeled nodes and connectors, arranged in a left-to-right flow:
1. **START Node**: A rectangular box on the far left, labeled "START".
2. **E Nodes**: Diamond-shaped nodes labeled "E". There are three visible "E" nodes in the main sequence.
3. **G_S Nodes**: Circular nodes labeled "G_S". There are three visible "G_S" nodes in the main sequence.
4. **Ellipsis Node**: A circular node containing "...", indicating a repeated or omitted sequence.
5. **END Node**: A rectangular box on the far right, labeled "END".
6. **Merge Point**: A solid black diamond shape that acts as a convergence point for multiple paths before the END node.
7. **Connectors**: Solid arrows indicate the primary flow of control. A dashed arrow indicates an alternative or final path from the ellipsis node to the merge point.
### Detailed Analysis
**Spatial Layout and Flow:**
The flow originates at the **START** node (leftmost). The primary path proceeds as follows:
1. START → **E** (first diamond)
2. **E** → **G_S** (first circle)
3. **G_S** → **E** (second diamond)
4. **E** → **G_S** (second circle)
5. **G_S** → **E** (third diamond)
6. **E** → **G_S** (third circle)
7. **G_S** → **...** (ellipsis circle)
**Loop Structure:**
A critical feedback loop is present. From the third **E** node (diamond), a solid arrow points backward and upward to the first **G_S** node (circle). This creates a cycle: `G_S (1st) → E (2nd) → G_S (2nd) → E (3rd) → G_S (1st)`.
**Termination Paths:**
All paths eventually converge at the **Merge Point** (black diamond) before the **END** node:
* A solid arrow leads from the third **E** node directly to the merge point.
* A dashed arrow leads from the **...** node to the merge point.
* The merge point then connects to the **END** node.
### Key Observations
1. **Repetitive Pattern**: The core structure is a repeating sequence of an "E" (diamond) followed by a "G_S" (circle).
2. **Explicit Loop**: The diagram explicitly shows one iteration of a loop being "unrolled," with the backward arrow from the third "E" to the first "G_S" defining the loop's back-edge.
3. **Ellipsis Implication**: The "..." node suggests the pattern of `G_S → E` continues for an unspecified number of additional iterations beyond the three fully drawn.
4. **Multiple Exit Conditions**: The presence of two distinct paths to the merge point (from the third "E" and from the "...") implies the loop can terminate under at least two different conditions.
### Interpretation
This diagram is a visual representation of a program's control flow, specifically for a loop that has been partially unrolled for analysis or optimization.
* **What it represents**: The "E" nodes likely represent **Evaluation** or **Expression** points (e.g., checking a loop condition). The "G_S" nodes likely represent **Guard Statements** or **General Statements** (the body of the loop). The unrolling shows the first few iterations explicitly.
* **How elements relate**: The forward arrows show the sequential execution within an iteration. The backward arrow defines the loop. The ellipsis indicates the pattern repeats. The merge point collects all possible exit paths from the loop construct before proceeding to the program's end.
* **Notable Anomalies/Patterns**: The key technical insight is the visualization of the loop's **continuation condition** (the back-edge from "E" to "G_S") versus its **exit conditions** (the forward paths from "E" and "..." to the merge point). This is fundamental for understanding loop optimization, parallelization, or formal verification. The diagram abstracts away specific operations, focusing purely on the control structure.
</details>
For this CFG, $\textnormal{prov}(N,x)$ is still well-defined by Algorithm 1, but the proof of Proposition 9 does not work anymore since it requires a directed acyclic graph.
To establish Proposition 9 for programs with while loops, we introduce a second type of control-flow graph, the unrolled CFG, which again is a directed acyclic graph. All translation rules are as before except for while loops, which is given below and illustrated above on the right. The resulting graph $G$ contains for every $i\in\mathbb{N}$ branch nodes $B_{i}=\textnormal{Branch}(E)$ and copies of the sub-CFG $G_{i}$ of statement $S$ . It contains a single join node $J$ for which we have $(B_{i},J)\in\textnormal{BranchJoin}(G)$ for all $i$ . Let $N_{\textnormal{first}}^{i}$ be successor of the start node in $G_{i}$ and $N_{\textnormal{last}}^{i}$ the predecessor of the end node in $G_{i}$ . In the new graph $G$ , the first branch node $B_{1}$ is successor of the start node and the end node is the successor of the join node $J$ . The branch nodes $B_{i}$ have two successors $N_{\textnormal{first}}^{i}$ and $J$ . $N_{\textnormal{last}}^{i}$ , the last node of sub-graph $G_{i}$ , resumes in the next branch node $B_{i+1}$ .
This definition implies that the number of nodes of $G$ is countable. Furthermore, since the unrolled CFG consists only of start, end, branch, join, and assign nodes, we can equip it with the same semantics as the standard CFG. As before, the semantics are equivalent.
** Proposition 0**
*For all program $S$ with CFG $G$ and unrolled CFG $H$ , it holds that for all traces $\mathtt{tr}$ and initial states $\sigma_{0}$
$$
{\bar{p}_{S}(\mathtt{tr},\sigma_{0})=\bar{p}_{G}(\mathtt{tr},\sigma_{0})=\bar{p}_{H}(\mathtt{tr},\sigma_{0}).}
$$*
* Proof*
By structural induction. See Appendix B.3. ∎
As mentioned, Algorithm 1 still works for the unrolled CFG. However, since the unrolled CFG contains an infinite number of nodes, in practice, we run this algorithm on the standard CFG with a finite number of nodes avoiding loops by marking visited nodes. We will show that the computations on the standard CFG produce an over-approximation of the provenance set in the unrolled CFG. But first, we define the connection between the two graph types.
** Definition 0**
*Let $G$ be the CFG and $H$ the unrolled CFG of program $S$ . For each node $M\in H$ , we define $\iota_{\textnormal{cfg}}(M)\in G$ as the node from which $M$ was copied in the construction of $H$ .*
The definition of $\iota_{\textnormal{cfg}}$ is best understood when considering the example in Fig. 2, where the CFG and unrolled CFG of a program are depicted side-by-side and connected with the mapping $\iota_{\textnormal{cfg}}$ .
<details>
<summary>x10.png Details</summary>
### Visual Description
## Diagram: Parallel Process Flowchart with Conditional Branching
### Overview
The image displays a technical flowchart diagram illustrating two parallel, similar process flows. Each flow begins with a "START" node, initializes a variable `x` to 10, passes through a decision point labeled "E", undergoes one or more decrement operations (`x = x - 1`), and terminates at an "END" node. The diagram uses black and red lines to differentiate between two distinct execution paths or conditions within each parallel flow. A dashed line with an ellipsis suggests an omitted or iterative segment.
### Components/Axes
* **Node Types:**
* **Terminal Nodes:** Rectangles labeled "START" (left side) and "END" (right side).
* **Process Nodes:** Rectangles containing the assignment `x = 10` and `x = x - 1`.
* **Decision Nodes:** Diamond shapes labeled with the letter "E".
* **Connector/Annotation:** A circle containing an ellipsis (`...`) connected by a dashed line.
* **Connectors (Edges):**
* **Solid Black Lines:** Represent the primary or default flow of control.
* **Solid Red Lines:** Represent an alternative or conditional flow of control.
* **Dashed Black Line:** Connects a decision node to the ellipsis circle, indicating a skipped or variable path.
* **Text Labels:**
* `START` (appears twice, top-left and bottom-left).
* `x = 10` (appears twice, immediately right of each START).
* `E` (appears four times, inside diamond-shaped decision nodes).
* `x = x - 1` (appears four times, in rectangular process nodes).
* `...` (inside a circle, right-center).
* `END` (appears twice, top-right and bottom-right).
* `t_0%` (written vertically in red, to the left of the bottom START node).
### Detailed Analysis
The diagram is structured as two parallel horizontal flows, top and bottom.
**Top Flow:**
1. **Start:** Begins at the top-left "START" node.
2. **Initialization:** Proceeds right to a process node setting `x = 10`.
3. **First Decision:** Enters a diamond decision node labeled "E".
* **Black Path (Default):** Exits the right point of the diamond, travels horizontally to the right, and connects directly to the top "END" node.
* **Red Path (Conditional):** Exits the top point of the diamond, curves upward and right to a process node (`x = x - 1`), then continues right and down to connect to the top "END" node.
4. **End:** Terminates at the top-right "END" node.
**Bottom Flow:**
1. **Start:** Begins at the bottom-left "START" node. The annotation `t_0%` is positioned vertically to its left.
2. **Initialization:** Proceeds right to a process node setting `x = 10`.
3. **First Decision:** Enters a diamond decision node labeled "E".
* **Black Path (Default):** Exits the right point of the diamond, travels right to a second process node (`x = x - 1`), then to a second "E" decision node.
* From this second "E", the black path exits right, goes to another `x = x - 1` node, then to a circle with `...`, and finally via a dashed line to the bottom "END" node.
* **Red Path (Conditional):** Exits the top point of the first "E" diamond, travels upward to connect to the `x = x - 1` node in the *top* flow's red path. This creates a cross-connection between the two parallel flows.
4. **End:** Terminates at the bottom-right "END" node.
### Key Observations
1. **Cross-Flow Connection:** The most notable feature is the red line connecting the first decision ("E") of the bottom flow to a process step in the top flow. This indicates that a condition in the bottom process can trigger an action within the top process.
2. **Path Complexity:** The bottom flow is more complex, featuring a second decision node ("E") and an ellipsis (`...`) suggesting an iterative or undefined number of subsequent steps.
3. **Color-Coded Logic:** Red lines consistently denote a path that involves the `x = x - 1` operation before reaching the end, while the black line from the first decision in the top flow bypasses any decrement.
4. **Spatial Layout:** The two flows are aligned horizontally. The legend (implied by line color) is integrated directly into the diagram's flow rather than placed in a separate box. The `t_0%` annotation is uniquely placed and colored, possibly indicating a time or threshold parameter for the bottom process.
### Interpretation
This diagram likely models a concurrent or parallel algorithm where two processes share an initial state (`x=10`) and have decision points ("E") that can influence each other. The "E" probably stands for an "Event," "Evaluation," or "Error" check.
* **What it demonstrates:** It shows how a single condition (the red path from the bottom "E") can have a side effect on a separate process (triggering a decrement in the top flow). The top flow has a simple "fast path" (black) and a "decrement path" (red). The bottom flow is more complex, with potential for multiple decrements (suggested by the ellipsis) and can also trigger the top flow's decrement.
* **Relationships:** The processes are not independent; they are coupled through the shared conditional logic represented by the red cross-connection. The state of variable `x` is central to both.
* **Anomalies/Notable Points:** The `t_0%` label is ambiguous without context but may represent a time-based trigger or a probability threshold for the bottom process's initial decision. The dashed line to the ellipsis indicates an abstracted or variable-length sequence of operations, which is a key detail for understanding the full scope of the bottom process. The diagram effectively visualizes inter-process communication or shared state management in a system.
</details>
Figure 2. CFG and unrolled CFG for program (x = 10; while (x < 10) do (x = x - 1)) and their connection via the map $\iota_{\textnormal{cfg}}$ shown with red edges.
The following lemma states that we can over-approximate the provenance set for variable $x$ at node $M$ in the unrolled CFG $H$ by applying Algorithm 1 to the corresponding node $\iota_{\textnormal{cfg}}(M)$ in $G$ .
** Lemma 0**
*Let $G$ be the CFG and $H$ the unrolled CFG of program $S$ . For each node $M\in H$ following statements hold:
$$
\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{RD}(M,x)\}\subseteq\textnormal{RD}(\iota_{\textnormal{cfg}}(M),x) \tag{6}
$$
$$
\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{BP}(M)\}=\textnormal{BP}(\iota_{\textnormal{cfg}}(M)) \tag{7}
$$
$$
\textnormal{prov}(M,x)\subseteq\textnormal{prov}(\iota_{\textnormal{cfg}}(M),x) \tag{8}
$$*
* Proof*
See Appendix B.4. ∎
### 4.2. Static Factorisation Theorem for Programs With Loops
The unrolled CFG has the important property that it is a directed acyclic graph with a potentially infinite number of nodes, but with a single root node. Further, each node $N\neq\textnormal{START}$ still has exactly one predecessor except for join nodes. Therefore, Proposition 9 can be generalised to unrolled CFGs with only a slight modification to the proof.
** Proposition 0**
*Let $H$ be the unrolled CFG of a program $S$ . For each node $M$ and variable $x$ , there exists an evaluation function
$$
V^{M}_{x}\in[\mathcal{T}|_{\textnormal{prov}(M,x)}\to\mathcal{V}],
$$
such that for all traces $\mathtt{tr}$ , initial program state $\sigma_{0}$ as in Definition 1, and execution sequence
$$
(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},M_{i})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{l},\text{END})
$$
we have
$$
\sigma_{i}(x)=V^{M_{i}}_{x}(\mathtt{tr}).
$$*
* Proof*
The unrolled CFG $H$ is constructed in a way such that we can prove the statement by well-founded induction on the relation $M_{1}\prec M_{2}\Leftrightarrow M_{1}\textit{ is parent of }M_{2}$ (i.e. there is an edge from $M_{1}$ to $M_{2}$ in $H$ ) similar to the proof of Proposition 9. The full proof is given in Appendix B.5. ∎
As before, Proposition 4 allows us to explicitly construct the factorisation of the program density.
** Theorem 5**
*Let $G$ be the CFG for a program $S$ . Let $N_{1},\dots,N_{K}$ be all sample nodes in $G$ . For each sample node $$ , let
$$
[A_{k}=\textnormal{addresses}(N_{k})\cup\textstyle\bigcup_{i=0}^{n_{k}}\textnormal{prov}(N_{k},E_{i}^{k})\cup\textstyle\bigcup_{N^{\prime}\in\textnormal{BP}(N_{k})}\textnormal{prov}(N^{\prime},{\textnormal{condexp}(N^{\prime})}). \tag{9}
$$
Then, there exist functions $p_{k}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}]$ such that for all $\mathtt{tr}\in\mathcal{T}$ , if $p_{S}(\mathtt{tr})\neq\textnormal{undefined}$ , then
$$
p_{S}(\mathtt{tr})=p_{G}(\mathtt{tr})=p_{H}(\mathtt{tr})=\prod_{k=1}^{K}p_{k}(\mathtt{tr}).
$$*
* Proof*
We give a proof sketch and refer to Appendix B.6 for the full proof. For each sample node $M_{j}$ in the unrolled CFG $H$ , we construct $\tilde{p}_{j}\in[\mathcal{T}|_{\tilde{A}_{j}}\to\mathbb{R}_{\geq 0}]$ as in the proof of Theorem 10. Next, we group the nodes $M_{j}$ by their corresponding CFG node: $p_{k}=\prod_{j\colon\iota_{\textnormal{cfg}}(M_{j})=N_{k}}\tilde{p}_{j}$ . From Lemma 3, we have that if $\iota_{\textnormal{cfg}}(M_{j})=N_{k}$ , then $\tilde{A}_{j}\subseteq A_{k}$ . Thus, $p_{k}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}]$ . Like in the proof of Theorem 10 it follows from Proposition 4 that $p_{S}(\mathtt{tr})=p_{G}(\mathtt{tr})=\prod_{k=1}^{K}p_{k}(\mathtt{tr})$ . ∎
#### 4.2.1. Equivalence to Markov Networks
As in Section 3.3.2, Theorem 5 implies that a program $S$ with $K$ sample statements is equivalent to a Markov network $\mathcal{H}$ with nodes $\{X_{\alpha}\colon\alpha\in\textstyle\bigcup_{k=1}^{K}A_{k}\}$ even if it contains loops. Again, the sets $D_{k}=\{X_{\alpha}\colon\alpha\in A_{k}\}$ form cliques in $\mathcal{H}$ and $p_{S}$ factorises over $\mathcal{H}$ with $\phi_{k}(D_{k})=p_{k}(\{\alpha\mapsto X_{\alpha}\colon\alpha\in A_{k}\})$ : $P(\vv{X})=\prod_{k=1}^{K}\phi_{k}(D_{k}).$
## 5. Optimising Posterior Inference Algorithms
While the statically obtained factorisation is provably correct, it is natural to ask whether the quality of the factorisation is good enough to be of practical use. To answer this question, we have developed a program transformation based on the static factorisation that generates sub-programs for each factor (described in Section 5.1). This program transformation operates on probabilistic programs that are implemented in our research PPL which models the formal language introduced in Section 2. It is implemented in Julia and can be viewed as a subset of PPLs like Gen, Turing, or Pyro. Many posterior inference algorithms can be improved by exploiting the factorisation of the model density. In Section 5.2, we demonstrate that if the change to the current program trace is small as in the light-weight Metropolis Hastings kernel (Wingate et al., 2011), then we can leverage the sub-programs to compute the acceptance probability faster. In Section 5.3, we show that we can reduce the variance of the ELBO gradient estimation in variational inference. Lastly, in Section 5.4, we compile sub-programs to enable an iterative implementation of sequential Monte Carlo. The realised optimisation tricks are well-known but typically restricted to programs with a finite number of random variables, PPLs that require the user to explicitly construct the graphical structure, or dynamic approaches. In contrast, our novel transformation operates on the source code and makes the optimisations statically available for programs containing while loops and dynamic addresses. We evaluate our implementation (Böck, 2025) on a benchmark set of 16 probabilistic programs, the majority of which make use of while loops to declare an unbounded number of random variables.
### 5.1. Generating Sub-programs from the Static Factorisation
We generate a sub-program for each sample statement (and thus for each factor) by deriving a program slicing method from the static provenance analysis. We want to generate a sub-program for each sample node $$ that
1. enables us to continue execution directly from $N_{k}$ from any state $\sigma$ ,
1. stops execution once all dependencies of $N_{k}$ were reached,
1. supports multiple inference algorithms.
To realise (1) and (2), we collect all sample nodes that depend on $N_{k}$ . From Theorem 5 we know that a sample node $N_{j}$ depends on $N_{k}$ if $N_{k}$ contributes to the provenance $A_{j}$ of the factor $p_{j}\in[\mathcal{T}|_{A_{j}}\to\mathbb{R}_{\geq 0}]$ as defined in Eq. 9. As explained in Section 3.2, these nodes can be found by modifying Algorithm 1 on line 8 to collect sample nodes instead of their addresses. For this modified algorithm provnode, we have $\textnormal{prov}(N,x)=\bigcup_{N^{\prime}\in\textnormal{provnode}(N,x)}\textnormal{addresses}(N^{\prime})$ and $N_{j}$ depends on $N_{k}$ if any variable $y$ in any expression $E_{i}^{j}$ in the sample statement of $N_{j}$ or in the conditional expression of any branch parent of $N_{j}$ depends on $N_{k}$ . We write $j\in\mathcal{J}_{k}$ if $N_{j}$ depends on $N_{k}$ .
We slice the program to only retain nodes that lie on a path from $N_{k}$ to $N_{j}$ for some $j\in\mathcal{J}_{k}$ . More formally, let $G_{k}$ be the CFG that contains node $N$ if there exists $j\in\mathcal{J}_{k}$ such that there is a path from $N_{k}$ to $N_{j}$ that visits $N$ and does not revisit $N_{k}$ . The start node of $G_{k}$ has successor $N_{k}$ and the nodes $N_{j}$ , $j\in\mathcal{J}_{k}$ , are connected to the end node of $G_{k}$ if they have no successor in $G_{k}$ . Lastly, sample nodes $N_{j}$ in $G_{k}$ that do not depend on $N_{k}$ , $j\notin\mathcal{J}_{k}$ , are transformed to read nodes for which $$ . This construction is made precise in Appendix D.1, where we also prove following correctness theorems as consequences of Theorem 5.
** Theorem 1**
*Let $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ be traces that only differ at address $\alpha$ , i.e. $\mathtt{tr}_{1}(\alpha)\neq\mathtt{tr}_{2}(\alpha)$ and $\forall\beta\neq\alpha\colon\mathtt{tr}_{1}(\beta)=\mathtt{tr}_{2}(\beta).$ Let the execution sequences in the unrolled CFG $H$ be equal up to sample node $$ and state $\sigma$ , such that $\alpha=\sigma(E_{0})$ :
| | $\displaystyle(\sigma_{0},\text{START})\overset{\mathtt{tr}_{1}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{1}}{\longrightarrow}(\sigma,M_{\alpha})\overset{\mathtt{tr}_{1}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{1}}{\longrightarrow}(\sigma_{l_{1}},\text{END}),$ | |
| --- | --- | --- |
If $M_{\alpha}$ is the only sample node in the execution sequences whose address expression evaluates to $\alpha$ , then for the sliced CFG $G_{k}$ of sample node $N_{k}=\iota_{\textnormal{cfg}}(M_{\alpha})$ , it holds that
$$
\log p_{G}(\mathtt{tr}_{1})-\log p_{G}(\mathtt{tr}_{2})=\log\bar{p}_{G_{k}}(\mathtt{tr}_{1},\sigma)-\log\bar{p}_{G_{k}}(\mathtt{tr}_{2},\sigma).
$$*
* Proof*
Follows from Theorem 5 and two technical lemmas. See Appendix D.2. ∎
** Corollary 0**
*Assume that for each trace $\mathtt{tr}$ there is at most one sample node $M_{\alpha}$ in its execution sequences such that the address expression of $M_{\alpha}$ evaluates to $\alpha$ . For initial program state $\sigma_{0}$ as in Definition 1, define
$$
p_{\alpha}(\mathtt{tr})\coloneqq\begin{cases}\bar{p}_{G_{k}}(\mathtt{tr},\sigma)&\text{ if }\exists\,\sigma\in\Sigma,M_{\alpha}\colon(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma,M_{\alpha})\land\iota_{\textnormal{cfg}}(M_{\alpha})=N_{k}\\
1&\text{ otherwise.}\end{cases}
$$
Then, $\Delta_{\alpha}(\mathtt{tr})\coloneqq\log p_{G}(\mathtt{tr})-\log p_{\alpha}(\mathtt{tr})$ is independent of address $\alpha$ , $\Delta_{\alpha}\in[\mathcal{T}|_{\mathbf{Strings}\setminus\{\alpha\}}\to\mathbb{R}_{\geq 0}].$*
* Proof*
Follows directly from Theorem 1. See Appendix D.3. ∎
Lastly, to fulfill (3), we further transform the program to take as input an execution context ctx. The context controls the behavior when executing a sample statement, e.g. to resample a variable or to accumulate the density. To actually handle the effects of different inference algorithms, we replace sample statements in the original program with three abstract methods that delegate the behavior to the context ctx. In $G_{k}$ , the statement of $N_{k}$ is transformed to visit, the statements of the nodes that depend on $N_{k}$ to score, and all other sample nodes that are on a path between $N_{k}$ and some $N_{j}$ , $j\in\mathcal{J}_{k}$ , but do not depend on $N_{k}$ , are transformed to read. Concrete instances of such contexts will be presented in the following sections and formalised in Appendix D.
We have implemented the sub-program generation as a compilation to the Julia programming language making use of multiple dispatch for contextualised execution. To enable continuation from any program state $\sigma$ we also inject a mutable state struct $\rho$ . As the CFG slicing implementation is a fairly standard graph traversal algorithm, we refer to our implementation (Böck, 2025) for further details like the translation from CFGs to source code.
The sub-program generation process is best illustrated with three examples. Consider program 1 in Figure 3. To generate a sub-program for the factor of sample statement ”B”, we omit the sample statements ”A” and ”E” as they do not lie on a path from ”B” to ”D” — the only sample statement that depends on ”B”. However, we still need to read the value of program variable A from the cached program state $\rho$ and we read the value for random variable ”C” from the trace. Continuing execution directly from a sample statement by caching the program state means that we can continue a loop from a specific iteration as exemplified by program 2 in Figure 3. This is particularly powerful, if the only dependency of a sample statement belongs to the same loop iteration. In this case, an entire while loop can be replaced by a single iteration which is shown for program 3 in Figure 3. Note that this form of loop-iteration independence is not captured by the factorisation of Proposition 4. Instead, it is product of the program slicing implementation.
Original formal program
Julia sub-program for factor (input: ctx and $\rho$ )
⬇
# Program 1
A = sample ("A", Norm (0.0,1.0))
B = sample ("B", Norm (A,1.0))
C = sample ("C", Norm (A,1.0))
D = sample ("D", Norm (B + C,1.0))
E = sample ("E", Norm (A,1.0))
⬇
# sub-program for factor of variable "B"
$\rho$ . B = visit (ctx, $\rho$ , "B", Norm ( $\rho$ . A,1.0))
$\rho$ . C = read (ctx, $\rho$ , "C")
$\rho$ . D = score (ctx, $\rho$ , "D", Norm ( $\rho$ . B + $\rho$ . C,1.0))
⬇
# Program 2
i = 0; b = 1;
while b do
b = sample ("b" + str (i), Bern (0.5))
i = i + 1
⬇
# sub-program for factor of variable "b"
$\rho$ . b = visit (ctx, $\rho$ , "b" * str ( $\rho$ . i), Bern (0.5))
$\rho$ . i = $\rho$ . i + 1
while b
$\rho$ . b = score (ctx, $\rho$ , "b" * str ( $\rho$ . i), Bern (0.5))
$\rho$ . i = $\rho$ . i + 1
end
⬇
# Program 3
i = 0;
while i < N do
z = sample ("z" + str (i), Bern (0.5))
m = (z == 1) ? -2.0 : 2.0
x = sample ("x" + str (i), Norm (m,1.0))
i = i + 1
⬇
# sub-program for factor of variable "z"
$\rho$ . z = visit (ctx, $\rho$ , "z" * str ( $\rho$ . i), Bern (0.5))
$\rho$ . m = ( $\rho$ . z == 1) ? -2.0 : 2.0
$\rho$ . x = score (ctx, $\rho$ , "x" * str ( $\rho$ . i), Norm ( $\rho$ . m,1.0))
Figure 3. Example Julia sub-programs generated from the static factorisation (with short-hands Norm = Normal, Bern = Bernoulli, str = string). Program variables are read from and stored to the program state struct $\rho$ .
### 5.2. Speeding-up Acceptance Probability Computation for Single-Site Trace Updates
In this section we introduce execution contexts to speed-up the single-site or light-weight Metropolis Hastings inference (LMH) algorithm (Wingate et al., 2011). The LMH algorithm works by selecting a single address $\alpha$ in each iteration at random and proposing a new value $v$ for the current trace $\mathtt{tr}(\alpha)$ . Even though we select a single address for the update, the proposal may have to produce additional values for sample statements that were not executed for trace $\mathtt{tr}$ , but due to stochastic branching or dynamic addressing are now executed for the new trace $\mathtt{tr}^{\prime}$ . For instance in Figure 3 program 2, if we change the value of the last random variable $\textnormal{"b}\_i\textnormal{"}$ from 0 to 1, then we may have to sample values for multiple $\textnormal{"b}\_j\textnormal{"}$ where $j>i$ until we get $\mathtt{tr}^{\prime}(\textnormal{"b}\_j\textnormal{"})=0$ .
The proposed trace $\mathtt{tr}^{\prime}$ is accepted (made current) with probability $A=\min\left(1,\frac{p(\mathtt{tr}^{\prime})\times Q_{\alpha}(\mathtt{tr}|\mathtt{tr}^{\prime})}{p(\mathtt{tr})\times Q_{\alpha}(\mathtt{tr}^{\prime}|\mathtt{tr})}\right),$ where $Q_{\alpha}$ captures the probability of the proposal process (sampling a value for $\alpha$ and all additional values as explained above). Then, the set of all generated traces is an approximation to the posterior distribution of the model.
In our approach, if the address comes from sample node $N_{k}$ , then we can optimise the runtime of this algorithm by noting that $\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})=\sum_{j=1}^{K}\log p_{j}(\mathtt{tr}^{\prime})-\log p_{j}(\mathtt{tr})=\sum_{j\in\mathcal{J}_{k}\cup\{k\}}\log p_{j}(\mathtt{tr}^{\prime})-\log p_{j}(\mathtt{tr})$ . Thus, by being able to compute the factors $p_{j}(\mathtt{tr}^{\prime})$ and $p_{j}(\mathtt{tr})$ separately, we can compute the ratio of densities $p(\mathtt{tr}^{\prime})/p(\mathtt{tr})$ by summing fewer terms.
By designing execution contexts for the sub-programs to handle the effect of the LMH kernel, we statically enable this optimisation for programs with an unbounded number of random variables and dynamic dependencies. In the following we informally describe the implementation of two execution contexts for resampling address $\alpha$ at sample node $N_{k}$ . A formal treatment can be found in Appendix D.1.
When executed with ForwardCtx, the sub-program is evaluated with respect to the proposed trace $\mathtt{tr}^{\prime}$ . At visit (ForwardCtx, $\rho$ , $E_{0}$ , $f(\dots$ )) we sample a new value $v$ for address $\alpha=\rho(E_{0})$ from some proposal distribution $q$ and return $v$ . As before, $\rho(E_{0})$ denotes $E_{0}$ evaluated with respect to $\rho$ . In the background, we accumulate the log-probability $\Delta P\leftarrow\Delta P+\log\textnormal{pdf}_{f}(v;\dots)$ and proposal log-probability $\Delta Q\leftarrow\Delta Q-\log\textnormal{pdf}_{q}(v;\dots)$ . At the start, $\Delta P$ and $\Delta Q$ are set to $0$ . At score (ForwardCtx, $\rho$ , $E_{0}$ , $f(\dots$ )) we propose a new value $v$ only if the address $\rho(E_{0})$ is not sampled for the current trace. We always update $\Delta P$ as before and only update $\Delta Q$ if we have proposed a new value. At read (ForwardCtx, $\rho$ , $E_{0}$ ), we simply return $\mathtt{tr}(\rho(E_{0}))$ . At each of the above statements we cache the program state in $\rho$ . This introduces book-keeping cost, but as we will see in Section 5.2.1, the cost is outweighed by the performance gained from only running sub-programs.
When executed with BackwardCtx, the sub-program is evaluated with respected to the current trace $\mathtt{tr}$ . At visit (BackwardCtx, $\rho$ , $E_{0}$ , $f(\dots$ )) we update $\Delta P\leftarrow\Delta P-\log\textnormal{pdf}_{f}(v;\dots)$ and proposal log-probability $\Delta Q\leftarrow\Delta Q+\log\textnormal{pdf}_{q}(v;\dots)$ with the current value $v=\mathtt{tr}(\rho(E_{0}))$ . At score (BackwardCtx, $\rho$ , $E_{0}$ , $f(\dots$ )) the same $\Delta P$ -updates are always performed while the $\Delta Q$ -updates are only performed if the address $\rho(E_{0})$ is not sampled for the proposed trace. At statement read (BackwardCtx, $\rho$ , $E_{0}$ ) we again return $\mathtt{tr}(\rho(E_{0}))$ . The program state does not have to be cached when executing with BackwardCtx.
Lastly, after executing the sub-program in both contexts, we have $A=\min(1,\exp(\Delta P+\Delta Q))$ . We accept the proposed trace with probability $A$ . In this case, we perform some book-keeping to update the inference state to the proposed trace with the cached program states. Building on the soundness of our provenance analysis and Theorem 1, we proof correctness of this approach in Appendix D.4:
** Corollary 0**
*Assume that the address expression of at most one sample node in the execution sequence evaluates to $\alpha$ for all traces. Let $\mathtt{tr}^{\prime}$ be the LMH proposal at address $\alpha$ for $\mathtt{tr}$ . Then, the execution sequences of $\mathtt{tr}$ and $\mathtt{tr}^{\prime}$ are equal up to $(\sigma,M_{\alpha})$ , where $M_{\alpha}$ is the first and only sample node whose address expression evaluates to $\alpha$ . For the sliced CFG $G_{k}$ , where $\iota_{\textnormal{cfg}}(M_{\alpha})=N_{k}$ , we have
$$
\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})=\log\bar{p}_{G_{k}}(\mathtt{tr}^{\prime},\sigma)-\log\bar{p}_{G_{k}}(\mathtt{tr},\sigma).
$$
The quantities $\log\bar{p}_{G_{k}}(\mathtt{tr}^{\prime},\sigma)$ , and $\log Q_{\alpha}(\mathtt{tr}^{\prime}|\mathtt{tr})$ are computed by ForwardCtx and the quantities $\log\bar{p}_{G_{k}}(\mathtt{tr},\sigma)$ and $\log Q_{\alpha}(\mathtt{tr}|\mathtt{tr}^{\prime})$ are computed by BackwardCtx. The new trace $\mathtt{tr}^{\prime}$ can be constructed from $\mathtt{tr}$ and the output of both contexts.*
#### 5.2.1. Experiment Results
Table 1. Average runtime of computing a single LMH iteration in microseconds (see Section 5.2). The column ”Baseline” reports the runtime when computing $p(\mathtt{tr}^{\prime})$ from scratch. The column ”Static Analysis” reports the runtime when updating the old density by computing $\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})$ with the generated sub-programs (see Section 5.1). The column ”Fixed-Finite” reports the runtime of updating the density with a hand-written factorisation that is representative of PPLs that explicitly construct a graphical model. The speed-up in relation to computing from scratch is given in the ”speed-up” and ”sp.up” columns. The number of random variables defined in each model can be found in column ”#RVs”. The number of samples produced and the acceptance rate are reported in the $N$ and $AR$ column, respectively.
| Model | #RVs | $N$ | $AR$ | Baseline $\mu s$ | Static Analysis $\mu s$ | Fixed-Finite-speed-up | $\mu s$ | sp.up | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| Aircraft | $\infty$ | $1\mathrm{e}{5}$ | 0.47 | 5.861 | 4.605 | 1.29 | $\nearrow$ | - | - |
| Bayesian Network | 37 | $1\mathrm{e}{5}$ | 0.93 | 25.580 | 4.680 | 5.47 | $\uparrow\uparrow$ | 3.344 | 7.65 |
| Captcha | $\infty$ | $1\mathrm{e}{3}$ | 0.81 | 774.287 | 355.382 | 2.18 | $\uparrow\uparrow$ | - | - |
| Dirichlet process | $\infty$ | $1\mathrm{e}{4}$ | 0.53 | 89.939 | 42.664 | 2.12 | $\uparrow\uparrow$ | - | - |
| Geometric | $\infty$ | $5\mathrm{e}{5}$ | 0.62 | 2.419 | 2.475 | 0.97 | $\rightarrow$ | - | - |
| GMM (fixed #clusters) | 209 | $5\mathrm{e}{4}$ | 0.60 | 71.136 | 7.027 | 10.01 | $\uparrow\uparrow$ | 4.564 | 15.58 |
| GMM (variable #clusters) | $\infty$ | $5\mathrm{e}{4}$ | 0.57 | 74.709 | 9.549 | 7.81 | $\uparrow\uparrow$ | - | - |
| HMM | 101 | $1\mathrm{e}{5}$ | 0.74 | 33.729 | 24.016 | 1.39 | $\nearrow$ | 2.551 | 13.22 |
| Hurricane | 5 | $1\mathrm{e}{6}$ | 0.86 | 2.121 | 1.918 | 1.13 | $\rightarrow$ | - | - |
| LDA (fixed #topics) | 551 | $1\mathrm{e}{4}$ | 0.81 | 209.046 | 24.526 | 8.52 | $\uparrow\uparrow$ | 18.341 | 11.40 |
| LDA (variable #topics) | $\infty$ | $1\mathrm{e}{4}$ | 0.83 | 218.614 | 25.732 | 8.50 | $\uparrow\uparrow$ | - | - |
| Linear regression | 102 | $1\mathrm{e}{5}$ | 0.53 | 4.477 | 8.006 | 0.56 | $\downarrow\downarrow$ | 7.504 | 0.60 |
| Marsaglia | $\infty$ | $5\mathrm{e}{5}$ | 0.93 | 1.699 | 2.159 | 0.79 | $\searrow$ | - | - |
| PCFG | $\infty$ | $1\mathrm{e}{5}$ | 0.75 | 10.220 | 8.437 | 1.21 | $\rightarrow$ | - | - |
| Pedestrian | $\infty$ | $1\mathrm{e}{5}$ | 0.37 | 3.709 | 3.645 | 1.02 | $\rightarrow$ | - | - |
| Urn | $\infty$ | $1\mathrm{e}{5}$ | 0.52 | 11.979 | 6.354 | 1.88 | $\nearrow$ | - | - |
To evaluate the speed-up made possible by our static factorisation, we gathered a benchmark set of 16 probabilistic programs. We specifically collected probabilistic programs from prior research that make use of while loops to define an unbounded number of random variables. References for the programs can be found in our replication package (Böck, 2025). Only 5 out of the 16 models define just a finite number of random variables with fixed dependency structure. It takes less than five seconds to generate the sub-programs for all models.
For each model, we run two implementations of the LMH inference algorithm. As a baseline, the standard implementation of LMH computes the acceptance probability $A$ by computing the density $p(\mathtt{tr}^{\prime})$ from scratch. Our optimised version of LMH leverages the sub-programs to compute $\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})$ when calculating $A$ . For the five finite models with fixed structure, we additionally implemented a factorisation that is representative of PPLs that explicitly construct a probabilistic graphical model. This factorisation enables LMH to exploit the full dependency structure of the model and serves as comparison. We have tested correctness of our LMH implementations by asserting that exactly the same acceptance probabilities and samples are computed.
In Table 1, we report the results of the experiment run a M2 Pro CPU. For each model and implementation, we ran LMH with 10 random starting traces for a total of $N$ samples and average the measurements over 10 experiment repetitions.
The first observation that we want to highlight is that computing $\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})$ with our approach can lead to longer runtime if there is no structure to exploit in the model. Consider the linear regression model in which the 100 observations depend on the slope and intercept variables. When changing the value of one of these variables, computing $\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})$ requires 100 additions and 100 subtractions, while $\log p(\mathtt{tr}^{\prime})$ only takes 100 additions. The same is true for the Marsaglia model which implements a rejection sampling method for the Normal distribution such that all variables depend on each other.
The factorisation approach shines when there is a lot of structure in the models like for the Aircraft, Captcha, Dirichlet Process, and Urn models, where the runtime is decreased up to a factor of 2. It is particularly powerful, when there are latent variables that only affect independent data variables. This is the case for the Gaussian mixture model (GMM) where there is one cluster allocation variable per data point and for the Latent Dirichlet Allocation model (LDA) where there is similar dependency structure. For these models we observe 8-10x speed-ups. Note that the handwritten ”fixed-finite” factorisations of the models are faster than the ”static analysis” factorisations, because LMH has to do less book-keeping for them. They do not leverage additional dependency structure.
The only model where our approach fails to effectively leverage the true dependency structure is the Hidden Markov Model (HMM). Even though the current state only affects the next state, our static analysis over-approximates this structure and outputs that the current state affects all future states. Now, if we modify the program by unrolling the while loop, i.e. repeating its body fifty times, our factorisation approach results in an improved runtime of 2.605 $\mu s$ (13x speed-up), because in this case the dependency structure is not over-approximated anymore due to loops. Note that the PCFG model essentially has the same structure as HMM, but can transition to a terminal state at every loop iteration. In this case, indeed the current state affects all future states and our static analysis is exact, but no significant improvements in runtime are measurable.
Lastly, we note that the Hurricane model is the only model in our benchmark with a finite number of random variables but a dynamic dependency structure (see Section 3.3.2). This model can also not be represented in a conventional Bayesian network structure, but our method is applicable and can slightly reduce the runtime.
#### 5.2.2. Comparison to Related Methods
The approach presented in Section 5 is the first to generate optimised MCMC kernels of models with unbounded number of random variables via a static program transformation. Importantly, its correctness follows from the theoretical foundation established in Section 4. Nevertheless, there exist methods that aim to accelerate MCMC kernels for a similar class of models with other approaches. In this section, our goal is to make a fair comparison to those methods by focusing on the relative speed-ups achieved. A direct runtime comparison is not meaningful due to differences in programming languages and the implementation of inference algorithms. More related approaches are described in Section 6.
Table 2. Relative speed-up for the LMH algorithm achieved with our static approach, combinators in Gen, and the C3 algorithm in WebPPL.
| Aircraft Bayesian Network Captcha | 1.29 5.47 2.18 | 1.41 4.14 2.93 | 1.02 0.93 1.05 | Hurricane LDA (fixed #topics) LDA (variable #topics) | 1.13 8.52 8.50 | 0.51 6.50 5.92 | 0.93 4.97 7.26 |
| --- | --- | --- | --- | --- | --- | --- | --- |
| Dirichlet process | 2.12 | - | 1.24 | Linear regression | 0.56 | 0.43 | 0.44 |
| Geometric | 0.97 | - | 0.74 | Marsaglia | 0.79 | - | 0.53 |
| GMM (fixed #clusters) | 10.01 | 6.26 | 1.90 | PCFG | 1.21 | - | 0.79 |
| GMM (variable #clusters) | 7.81 | 5.45 | 1.60 | Pedestrian | 1.02 | - | 0.52 |
| HMM | 1.39 | 1.31 | 3.82 | Urn | 1.88 | 2.05 | 0.69 |
First, Ritchie et al. (2016) presented the C3 approach to enable incrementalised re-execution of Metropolis Hastings kernels using continuations and function call caching. To be effective this methods requires programs to be implemented with recursion instead of while loops. We re-implemented the models in recursive form in WebPPL (Goodman and Stuhlmüller, 2014) to report the relative speed-up achieved with C3 in Table 2. Our approach achieves better speed-ups for all models except for the HMM. As explained before, our static analysis greatly over-approximates the dependency structure of this model. Note that Ritchie et al. (2016) report even more significant speed-ups for the GMM, LDA, and HMM models for larger data-set sizes. Our approach scales the same for GMM and LDA.
Further, modern probabilistic programming systems like Gen (Cusumano-Towner et al., 2019) include language constructs like Map, Unfold, and Recurse to model independence structure. Thus, we re-implemented LMH and the 16 models only in Gen with the so-called combinator constructs and report the results in Table 2. Gen’s inference backend can only leverage the combinator constructs if the root model function is written in the static modelling language – a non-universal subset of the language with no control statements. This effectively abstracts away loops as Map, Unfold, or Recurse nodes in an internal graphical representation. Note that at the time of writing Gen does not implement incremental computation for the Recurse combinator, a construct required for models where the condition of the while loop depends on the body like the Geometric model. We cannot apply our general LMH implementation to those models and mark them with ”-”. Overall, the order of magnitude of speed-up achieved with combinators is similar to our static approach. There seems to be more overhead in Gen as it supports general programmable inference in contrast to our research PPL. We emphasise that our approach achieves these speed-ups fully automatically from source code without the need to explicitly model independence structure with language constructs.
### 5.3. Reducing the Variance of an ELBO Gradient Estimator in Variational Inference
Variational inference takes a different approach to MCMC methods by fitting a so-called variational distribution $Q_{\phi}$ to the posterior, where $\phi$ is a set of parameters. The objective is to maximise the evidence lower-bound $\textnormal{ELBO}(\phi)=\mathbb{E}_{z\sim Q_{\phi}}{\left[\log P(z)-\log Q_{\phi}(z)\right]}$ via gradient ascent, where $P$ denotes a potentially unnormalised density. In this section, we consider Black-Box Variational Inference (BBVI) (Ranganath et al., 2014), which estimates the gradient of the ELBO with following identity $\nabla_{\phi}\textnormal{ELBO}(\phi)=\mathbb{E}_{z\sim Q_{\phi}}{\left[\nabla_{\phi}\log Q_{\phi}(z)\times(\log P(z)-\log Q_{\phi}(z))\right]}$ . Unfortunately, this estimator often exhibits high variance. To reduce the variance Ranganath et al. (2014) use a mean-field variational distribution $Q_{\phi}(z)=\prod_{i=1}^{n}q_{i}(z_{i}|\phi_{i})$ to derive the improved estimator
$$
\nabla_{\phi_{i}}\textnormal{ELBO}(\phi)=\mathbb{E}_{z_{(i)}\sim Q^{i}_{\phi}}{\left[\nabla_{\phi_{i}}\log q_{i}(z_{i}|\phi_{i})\times(\log P^{i}(z_{(i)})-\log q_{i}(z_{i}|\phi_{i}))\right]}. \tag{10}
$$
Note that the gradient is only with respect to $\phi_{i}$ and the expectation is with respect to the Markov blanket $z_{(i)}$ of $z_{i}$ . Including $z_{i}$ , this is the set of variables that directly influence $z_{i}$ according to $P$ , variables that are directly influenced by $z_{i}$ – children of $z_{i}$ – and variables that directly influence a child of $z_{i}$ . Then, $P^{i}$ is the density factoring out all other variables and $Q^{i}_{\phi}$ the variational distribution restricted to $z_{(i)}$ . This reduces the variance and we will replicate this trick with our factorisation.
In our sub-program setting, we achieve the same optimisation by defining the execution context BBVICtx, which we formalise in Appendix D.5. First, assume that a trace $\mathtt{tr}$ is generated from a variational distribution, where each address $\alpha$ is sampled from $\mathtt{tr}(\alpha)\sim q_{\alpha}(\mathtt{tr}(\alpha)|\phi_{\alpha})$ . The BBVICtx executes the program with respect to $\mathtt{tr}$ . Similar to the ForwardCtx, it accumulates $\Delta\leftarrow\Delta+\log\textnormal{pdf}_{f}(v;\dots)$ at score (BBVICtx, $\rho$ , $E_{0}$ , $f(\dots$ )) and returns $v=\mathtt{tr}(\rho(E_{0}))$ at read (BBVICtx, $\rho$ , $E_{0}$ )). At visit statement visit (BBVICtx, $\rho$ , $E_{0}$ , $f(\dots$ )) we additional substract the proposal density $\Delta\leftarrow\Delta+\log\textnormal{pdf}_{f}(v;\dots)-\log q_{\alpha}(v|\phi_{\alpha})$ , where we have $\alpha=\rho(E_{0})$ (compare Eq. 10). In Appendix D.5. we prove following correctness result as a consequence of Corollary 2:
** Corollary 0**
*Let $Q_{\phi}$ be a variational distribution over traces as formalised in Appendix D.5. Assume that the address expression of at most one sample node in the execution sequence evaluates to $\alpha$ for all traces. Under measurability assumptions given in Appendix D.5 and with $p_{\alpha}$ as in Corollary 2,
| | $\displaystyle\nabla_{\phi_{\alpha}}\mathbb{E}_{\mathtt{tr}\sim Q_{\phi}}{\left[\log p(\mathtt{tr})-\log Q_{\phi}(\mathtt{tr})\right]}=$ | |
| --- | --- | --- |
The quantity $\log p_{\alpha}(\mathtt{tr})-\log q_{\alpha}(\mathtt{tr}(\alpha)|\phi_{\alpha})$ is computed by BBVICtx.*
Note that in contrast to Equation 10, where the expectation is taken explicitly with respect to the Markov blanket $z_{(i)}$ , in Corollary 4 the dependencies are accounted for via $p_{\alpha}(\mathtt{tr})$ (computed with a sub-program). Replacing $p$ in the integrand with $p_{\alpha}$ reduces the variance, because $p_{\alpha}$ is constant with respect to addresses that are independent from a change to the trace at address $\alpha$ .
#### 5.3.1. Experiment Results
To evaluate the approach we have implemented our BBVI optimisation and compare the improved estimator against the standard estimator with respect to the average gradient variance across all parameters. In 10 experiment repetitions, we performed 1000 optimisation steps and used 100 samples to estimate the gradient in each step. In Table 3, we report our results, where we omit programs with random variables that have stochastic support dimension and are incompatible with BBVI.
We compare against Pyro’s TraceGraph_ELBO variance reduction technique, which follows Schulman et al. (2015) and makes use of dynamic data provenance analysis. This comes with the benefit of having no over-approximation issues, but also comes with the drawback of not being able to correctly account for control flow dependencies. For Pyro we decreased the number of samples to 100 and number of repetitions to 1 due to long runtime. In Table 3, we see that for programs with only data dependencies we achieve comparable variance reduction with lower runtime penalty. Furthermore, with our approach we were able to reduce the variance for two models with control flow dependencies Aircraft and Marsaglia. Note that for the same reasons as in LMH, the static optimisation is only effective for the unrolled version of the HMM.
Table 3. Average variance of the standard and improved ELBO gradient estimator in BBVI. The variance is averaged over all parameters, 1000 iterations, and 100 samples per iteration. The ”cost” column reports the factor by which the runtime increased for the improved estimator. For reference, we include the variance reduction factor achieved by Pyro’s TraceGraph_ELBO.
| Model | Baseline-avg. var. | Static Analysis-avg. var. | Pyro-red. factor | cost | red. factor | cost | |
| --- | --- | --- | --- | --- | --- | --- | --- |
| Aircraft | 7.922e+03 | 7.969e+01 | 99.29 | $\downarrow\downarrow$ | 1.89 | - | - |
| Bayesian Network | 4.160e+02 | 4.371e+00 | 95.06 | $\downarrow\downarrow$ | 1.94 | 95.09 | 7.52 |
| Geometric | 1.634e-01 | 1.726e-01 | 0.94 | $\rightarrow$ | 0.53 | - | - |
| GMM (fixed #clusters) | 8.043e+09 | 1.014e+06 | 8092.80 | $\downarrow\downarrow$ | 2.26 | 9848.79 | 8.69 |
| HMM | 2.116e+03 | 1.279e+03 | 1.65 | $\rightarrow$ | 7.49 | 1254.24 | 8.67 |
| HMM (no loop) | 2.116e+03 | 2.349e+00 | 901.01 | $\downarrow\downarrow$ | 1.50 | 1254.24 | 8.64 |
| Hurricane | 3.362e-01 | 3.609e-01 | 0.93 | $\rightarrow$ | 0.81 | - | - |
| LDA (fixed #topics) | 7.229e+04 | 1.172e+00 | 61646.02 | $\downarrow\downarrow$ | 5.92 | 59986.61 | 11.00 |
| Linear regression | 3.350e+05 | 3.341e+05 | 1.00 | $\rightarrow$ | 1.14 | 1.00 | 14.39 |
| Marsaglia | 7.274e-02 | 1.283e-02 | 5.38 | $\searrow$ | 0.51 | - | - |
| PCFG | 8.838e-03 | 1.989e-02 | 0.56 | $\rightarrow$ | 0.94 | - | - |
| Pedestrian | 3.108e+06 | 3.111e+06 | 1.00 | $\rightarrow$ | 2.01 | - | - |
### 5.4. Iteratively Running Sequential Monte Carlo
Lastly, we briefly describe how our slicing technique can be adapted to the setting of sequential Monte Carlo (SMC) (Chopin et al., 2020), which yet again takes a different approach to inference. In SMC a number of traces $\mathtt{tr}_{n}$ , so-called particles, are evaluated in parallel. Data points are added iteratively to the inference process and the particles are resampled according to their data likelihood. More precisely at time $t$ we have data set $\mathcal{D}_{1:t}$ and define the corresponding density $p_{t}$ . At inference step $t$ , the particle $\mathtt{tr}$ is logarithmically weighted according to $\log p_{t}({\mathtt{tr}_{n}})-\log p_{t-1}({\mathtt{tr}_{n}})$ and the particles are resampled (duplicated or discarded) with respect to these weights.
A ”naive” implementation of SMC would compute $\log p_{t}({\mathtt{tr}_{n}})$ from scratch, while an iterative implementation is able to compute $\log p_{t}({\mathtt{tr}_{n}})-\log p_{t-1}({\mathtt{tr}_{n}})$ directly. In probabilistic programming this is often realised by some mechanism that enables the interruption and continuation of program execution. We enable this optimisation by slightly adapting the slicing method of Section 5.1 to generate sub-programs which compute the difference directly.
Namely, for sample node $N_{k}$ let $G_{k}^{\texttt{SMC}}$ be the CFG that contains node $N$ if there exists a sample node $N_{j}$ such that $N$ lies on a path from $N_{k}$ to $N_{j}$ which contains no other sample nodes. Again, $N_{k}$ will be the successor of the start node of $G_{k}^{\texttt{SMC}}$ , but all other samples nodes will have the end node of $G_{k}^{\texttt{SMC}}$ as sole successor. As we only care about continuing execution from $N_{k}$ to the next sample node, this construction is independent of the provenance analysis and Theorem 5.
In our implementation, we again make use of an evaluation context which simply accumulates the density like the standard semantics. In Appendix D.6, we prove correctness:
** Proposition 0**
*Let $G$ be a CFG such that for initial program state $\sigma_{0}$ and trace $\mathtt{tr}$ , we have execution sequence $(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},M_{i})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{l},\text{END})$ in its unrolled version $H$ . Let $(\sigma^{\prime}_{1},M^{\prime}_{1})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{2},M^{\prime}_{2})$ be a sub-sequence such that $\iota_{\textnormal{cfg}}(M^{\prime}_{1})=N_{k}$ and $\iota_{\textnormal{cfg}}(M^{\prime}_{2})=N_{j}$ are the only sample nodes. Then, the execution sequence in the unrolled version of the sliced CFG $G_{k}^{\texttt{SMC}}$ matches the sub-sequence: $(\sigma^{\prime}_{1},\text{START})\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{1},M^{\prime}_{1})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{2},M^{\prime}_{2})\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{2},\text{END}).$*
Proposition 5 allows us to evolve the execution sequence of a particle $\mathtt{tr}_{n}$ from one sample node $N_{t}^{n}=N_{k}$ to the next $N_{t+1}^{n}=N_{j}$ by executing the corresponding sliced CFG $G_{k}^{\texttt{SMC}}$ . The weight of the particle is updated with $\log p_{t}(\mathtt{tr}_{n})-\log p_{t-1}(\mathtt{tr}_{n})=\log\sigma_{2}^{\prime}(\textbf{p})-\log\sigma_{1}^{\prime}(\textbf{p})$ and particles may be resampled even if the execution sequences were stopped at different sample nodes $N_{t}^{n}$ (Lundén et al., 2021).
Table 4. Average runtime of naive versus iterative implementations of SMC with 100 particles. For reference, we report the speed-up achieved by WebPPL’s CPS transformation.
| Model | #Data | Baseline $ms$ | Static Analysis $ms$ | WebPPL-speed-up | speed-up | |
| --- | --- | --- | --- | --- | --- | --- |
| Dirichlet process | 50 | 238.323 | 22.374 | 10.57 | $\uparrow\uparrow$ | 8.96 |
| GMM (fixed #clusters) | 100 | 166.480 | 31.260 | 5.26 | $\uparrow\uparrow$ | 9.23 |
| GMM (variable #clusters) | 100 | 189.529 | 31.263 | 5.95 | $\uparrow\uparrow$ | 9.18 |
| HMM | 50 | 31.951 | 7.394 | 4.13 | $\uparrow\uparrow$ | 7.66 |
| HMM (no loop) | 50 | 49.649 | 7.420 | 6.63 | $\uparrow\uparrow$ | 6.79 |
| LDA (fixed #topics) | 262 | 1319.553 | 397.074 | 3.33 | $\uparrow\uparrow$ | 7.25 |
| LDA (variable #topics) | 262 | 1412.182 | 410.781 | 3.44 | $\uparrow\uparrow$ | 8.18 |
#### 5.4.1. Experiment Results
To measure the performance gains achievable with our static approach, we compare the runtime of the iterative implementation of SMC based on the generated sub-programs against a naive implementation which computes $\log p_{t}(\mathtt{tr})$ from scratch. In Table 4 we report the speed-ups on the subset of models which can make use of iteratively adding data points in inference. For all models we set the number of particles to 100 and repeated the experiment 10 times. The measured speed-ups are significant and range from 3x - 10x. For reference, we benchmarked the runtimes achieved with WebPPL’s continuation passing style (CPS) approach against a naive SMC implementation in JavaScript. For most models this resulted in greater speed-ups compared to our static approach. This is due to the fact that, like in Section 5.2, in our approach computational overhead is introduced by caching and copying programs states when resampling particles.
## 6. Related Work
### 6.1. Semantics of Probabilistic Programming Languages
One of the first works to formally define the semantics of a probabilistic programming language was Kozen (1979). Derivatives of this semantics can be found throughout literature, for example see Hur et al. (2015), Dahlqvist and Kozen (2019), or Barthe et al. (2020). We give a brief (and incomplete) overview of existing semantic models for PPLs.
In recent years, a lambda calculus for probabilistic programming was presented by Borgström et al. (2016). This work and a domain theoretic approach for probabilistic programming (Vákár et al., 2019) had an influence on the development of the statistical PCF (Mak et al., 2021) (programming computable functions), which was used to prove differentiability of terminating probabilistic programs. Probabilistic programming was also examined from a categorical perspective (Heunen et al., 2017) and the semantics of higher order probabilistic programs is also researched (Dahlqvist and Kozen, 2019; Staton et al., 2016).
As mentioned, the semantics presented in this work generalise those of Gorinova et al. (2019) which formalises the core language constructs of Stan by interpreting a program as a function over a fixed set of finite variables. In our semantics, we interpret programs as functions over traces which are mappings from addresses to values similar to dictionaries. Another dictionary based approach to probabilistic programming can be found in Cusumano-Towner et al. (2020) and denotational semantics based on trace types are introduced in Lew et al. (2019). To the best of our knowledge there are only two existing semantic models that support user-defined addresses (Lew et al., 2023; Lee et al., 2019). Note that denotational semantics of a simplified version of the address-based PPL Gen are given in Cusumano-Towner (2020).
Furthermore, the connection of simple probabilistic programs to Bayesian networks is known (van de Meent et al., 2018). Borgström et al. (2011) consider a small imperative language and give semantics in terms of factor graphs – a concept related to Bayesian networks. Sampson et al. (2014) compile probabilistic programs to Bayesian networks by treating loops as black-box functions in order to verify probabilistic assertion statements. Previous work extended Bayesian networks to so-called contingent Bayesian networks in order to support models with an infinite number of random variables or cyclic dependencies (Milch et al., 2005), but they cannot be straightforwardly applied to PPLs with user-labelled sample statements and while loops. Paquet (2021) presented a interpretation of probabilistic programs in game semantics, which can be seen as a refinement of Bayesian networks. Most recently, Faggian et al. (2024) introduced a higher-order functional language for discrete Bayesian networks.
### 6.2. Graphical Representations, Optimisations, and Dependency Analysis
The advantages of representing a probabilistic model graphically are well-understood (Koller and Friedman, 2009). For this reason, some PPLs like PyMC (Salvatier et al., 2016), Factorie (McCallum et al., 2009), or Infer.NET (Minka, 2012) require the user to explicitly define their model as a graph. This is not possible if we want to support while loops in our programs. There are also other graphical representations that allow for optimised inference like binary decision diagrams (Holtzen et al., 2020) or sum-product networks (Saad et al., 2021). Venture (Mansinghka et al., 2018) represents traces graphically to facilitate efficient recomputation of subparts of the program. Similar to Gen (Cusumano-Towner et al., 2019), Pyro (Bingham et al., 2019) implements the plate and markov constructs to model independence and reduce variance in variational inference.
Modifying the Metropolis Hastings algorithm to exploit the structure of the model is also common practice. Wu et al. (2016) optimised BLOG to dynamically keep track of the Markov blanket of a variable among other improvements. For their Metropolis Hastings implementation, they reported significant speed-ups for the Hurricane model, instances of the Urn model, and GMMs with unknown number of clusters. The Shred system (Yang et al., 2014) traces Church (Goodman et al., 2012) programs and slices the them to identify the minimal computation needed to compute the MH acceptance probability, and translates them to C++. However, their approach comes with high compilation cost, is not proven correct nor open-source. Hur et al. (2014) developed a different theory for slicing probabilistic programs. In their unpublished implementation, they observe significant runtime improvements if statements irrelevant to the return expression are removed from the program. In contrast, we slice programs with respect to the dependencies between sample statements in the program and there are no redundancies in the programs of our benchmark set. Castellan and Paquet (2019) present a theoretical foundation for incremental computation in the Metropolis Hastings algorithm by graphically modelling the data-dependencies between sample statements. However, they only consider a first-order probabilistic programs and did not implement or evaluate their approach.
Furthermore, there are many more optimisation opportunities to reduce the variance in variational inference like control variates (Paisley et al., 2012) or path-derivatives (Roeder et al., 2017). For a review on advances in variational inference see Zhang et al. (2018). Also, there are many methods to facilitate iterative implementations of SMC: WebPPL (Goodman and Stuhlmüller, 2014) and Anglican (Tolpin et al., 2015) use a continuation-passing-style transform; Turing (Ge et al., 2018) uses a tape of instructions; some PPLs like Birch (Murray and Schön, 2018) require the user to explicitly write the model in an iterative fashion.
Lastly, the probabilistic dependency structure of programs has also been exploited for applications different from optimising inference. Baah et al. (2008) leverage the structure for fault diagnosis and Bernstein et al. (2020) extract the factor graph of programs to automate model checking for models implemented in Stan. In general, static analysis for probabilistic programming is an active research field. For instance, Lee et al. (2019) developed a static analysis to verify so-called guide programs for stochastic variational inference in Pyro. Gorinova et al. (2021) developed an information flow type system and program transformation to automatically marginalise out discrete variables in Stan. Another example is the extension of the Stan compiler with a pedantic mode that statically catches common pitfalls in probabilistic programming (Bernstein, 2023). Recently, a framework for statically analysing probabilistic programs in a language-agnostic manner was presented (Böck et al., 2024). For a 2019 survey on static analysis for probabilistic programming see Bernstein (2019).
## 7. Conclusion
In this work, we addressed the open question to what extent a probabilistic program with user-labelled sample statements and while loops can be represented graphically. We presented a generalisation of existing formal semantics to support these language features. We developed a sound static analysis that approximates the dependency structure of random variables in the program and used this structure to factorise the implicitly defined program density. The factorisation is equivalent to the known Bayesian network factorisation in a restricted case, but novel for programs with dynamic addresses and loops. Lastly, we demonstrated that by generating a sub-program for each factor based on the static dependency structure, we can 1. speed-up a single-site Metropolis Hastings algorithm; 2. reduce gradient variance in variational inference; 3. facilitate an iterative implementation of sequential Monte Carlo. This work is to first to make these optimisations statically available for the considered program class. We proved correctness and empirically showed that our approach performs comparably or better than existing methods.
## 8. Data-Availability Statement
The source code to reproduce the experiments of Section 5 is made available at the time of review (Böck, 2025), will be submitted to Artifact Evaluation, and will be published after the review period. The shared repository includes the implementation of the static provenance analysis (Section 3.2) for a research PPL, the generation of sub-programs according to the dependency structure (Section 5), as well as a standard and optimised implementations of the LMH, BBVI, and SMC algorithms. It also includes the 16 benchmark programs (Section 5.2.1) written in our research PPL, with and without combinators in Gen, in recursive fashion in WebPPL, and in Pyro.
## References
- (1)
- Baah et al. (2008) George K Baah, Andy Podgurski, and Mary Jean Harrold. 2008. The probabilistic program dependence graph and its application to fault diagnosis. In Proceedings of the 2008 international symposium on Software testing and analysis. 189–200.
- Barthe et al. (2020) Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva. 2020. Foundations of probabilistic programming. Cambridge University Press.
- Bernstein (2019) Ryan Bernstein. 2019. Static analysis for probabilistic programs. arXiv preprint arXiv:1909.05076 (2019).
- Bernstein (2023) Ryan Bernstein. 2023. Abstractions for Probabilistic Programming to Support Model Development. Ph. D. Dissertation. Columbia University.
- Bernstein et al. (2020) Ryan Bernstein, Matthijs Vákár, and Jeannette Wing. 2020. Transforming probabilistic programs for model checking. In Proceedings of the 2020 ACM-IMS on Foundations of Data Science Conference. 149–159.
- Bingham et al. (2019) Eli Bingham, Jonathan P Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul Szerlip, Paul Horsfall, and Noah D Goodman. 2019. Pyro: Deep universal probabilistic programming. The Journal of Machine Learning Research 20, 1 (2019), 973–978.
- Böck et al. (2024) Markus Böck, Michael Schröder, and Jürgen Cito. 2024. Language-Agnostic Static Analysis of Probabilistic Programs. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 78–90.
- Borgström et al. (2016) Johannes Borgström, Ugo Dal Lago, Andrew D Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. ACM SIGPLAN Notices 51, 9 (2016), 33–46.
- Borgström et al. (2011) Johannes Borgström, Andrew D Gordon, Michael Greenberg, James Margetson, and Jurgen Van Gael. 2011. Measure transformer semantics for Bayesian machine learning. In Programming Languages and Systems: 20th European Symposium on Programming, ESOP 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings 20. Springer, 77–96.
- Böck (2025) Markus Böck. 2025. Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops. https://doi.org/10.5281/zenodo.16900539
- Castellan and Paquet (2019) Simon Castellan and Hugo Paquet. 2019. Probabilistic programming inference via intensional semantics. In Programming Languages and Systems: 28th European Symposium on Programming, ESOP 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings 28. Springer, 322–349.
- Chen et al. (2014) Yutian Chen, Vikash Mansinghka, and Zoubin Ghahramani. 2014. Sublinear approximate inference for probabilistic programs. stat 1050 (2014), 6.
- Chopin et al. (2020) Nicolas Chopin, Omiros Papaspiliopoulos, et al. 2020. An introduction to sequential Monte Carlo. Vol. 4. Springer.
- Cooper and Torczon (2011) Keith D Cooper and Linda Torczon. 2011. Engineering a compiler. Elsevier.
- Cusumano-Towner et al. (2020) Marco Cusumano-Towner, Alexander K Lew, and Vikash K Mansinghka. 2020. Automating involutive MCMC using probabilistic and differentiable programming. arXiv preprint arXiv:2007.09871 (2020).
- Cusumano-Towner (2020) Marco Francis Cusumano-Towner. 2020. Gen: a high-level programming platform for probabilistic inference. Ph. D. Dissertation. Massachusetts Institute of Technology.
- Cusumano-Towner et al. (2019) Marco F Cusumano-Towner, Feras A Saad, Alexander K Lew, and Vikash K Mansinghka. 2019. Gen: a general-purpose probabilistic programming system with programmable inference. In Proceedings of the 40th acm sigplan conference on programming language design and implementation. 221–236.
- Dahlqvist and Kozen (2019) Fredrik Dahlqvist and Dexter Kozen. 2019. Semantics of higher-order probabilistic programs with conditioning. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–29.
- Faggian et al. (2024) Claudia Faggian, Daniele Pautasso, and Gabriele Vanoni. 2024. Higher Order Bayesian Networks, Exactly. Proceedings of the ACM on Programming Languages 8, POPL (2024), 2514–2546.
- Ge et al. (2018) Hong Ge, Kai Xu, and Zoubin Ghahramani. 2018. Turing: a language for flexible probabilistic inference. In International conference on artificial intelligence and statistics. PMLR, 1682–1690.
- Goodman et al. (2012) Noah Goodman, Vikash Mansinghka, Daniel M Roy, Keith Bonawitz, and Joshua B Tenenbaum. 2012. Church: a language for generative models. arXiv preprint arXiv:1206.3255 (2012).
- Goodman and Stuhlmüller (2014) Noah D Goodman and Andreas Stuhlmüller. 2014. The Design and Implementation of Probabilistic Programming Languages. http://dippl.org. Accessed: 2025-3-20.
- Gordon et al. (2014) Andrew D Gordon, Thomas A Henzinger, Aditya V Nori, and Sriram K Rajamani. 2014. Probabilistic programming. In Future of software engineering proceedings. 167–181.
- Gorinova et al. (2019) Maria I Gorinova, Andrew D Gordon, and Charles Sutton. 2019. Probabilistic programming with densities in SlicStan: efficient, flexible, and deterministic. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1–30.
- Gorinova et al. (2021) Maria I Gorinova, Andrew D Gordon, Charles Sutton, and Matthijs Vákár. 2021. Conditional independence by typing. ACM Transactions on Programming Languages and Systems (TOPLAS) 44, 1 (2021), 1–54.
- Hennessy and Patterson (2011) John L Hennessy and David A Patterson. 2011. Computer architecture: a quantitative approach. Elsevier.
- Heunen et al. (2017) Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1–12.
- Holtzen et al. (2020) Steven Holtzen, Guy Van den Broeck, and Todd Millstein. 2020. Scaling exact inference for discrete probabilistic programs. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 1–31.
- Hur et al. (2014) Chung-Kil Hur, Aditya V Nori, Sriram K Rajamani, and Selva Samuel. 2014. Slicing probabilistic programs. ACM SIGPLAN Notices 49, 6 (2014), 133–144.
- Hur et al. (2015) Chung-Kil Hur, Aditya V Nori, Sriram K Rajamani, and Selva Samuel. 2015. A provably correct sampler for probabilistic programs. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
- Koller and Friedman (2009) Daphne Koller and Nir Friedman. 2009. Probabilistic graphical models: principles and techniques. MIT press.
- Kozen (1979) Dexter Kozen. 1979. Semantics of probabilistic programs. In 20th Annual Symposium on Foundations of Computer Science (sfcs 1979). IEEE, 101–114.
- Lee et al. (2019) Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. 2019. Towards verified stochastic variational inference for probabilistic programs. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–33.
- Lew et al. (2019) Alexander K Lew, Marco F Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K Mansinghka. 2019. Trace types and denotational semantics for sound programmable inference in probabilistic languages. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–32.
- Lew et al. (2023) Alexander K Lew, Matin Ghavamizadeh, Martin C Rinard, and Vikash K Mansinghka. 2023. Probabilistic Programming with Stochastic Probabilities. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 1708–1732.
- Lundén et al. (2021) Daniel Lundén, Johannes Borgström, and David Broman. 2021. Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages.. In ESOP. 404–431.
- Lunn et al. (2000) David J Lunn, Andrew Thomas, Nicky Best, and David Spiegelhalter. 2000. WinBUGS-a Bayesian modelling framework: concepts, structure, and extensibility. Statistics and computing 10 (2000), 325–337.
- Mak et al. (2021) Carol Mak, C-H Luke Ong, Hugo Paquet, and Dominik Wagner. 2021. Densities of almost surely terminating probabilistic programs are differentiable almost everywhere. In Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27–April 1, 2021, Proceedings 30. Springer International Publishing, 432–461.
- Mansinghka et al. (2018) Vikash K Mansinghka, Ulrich Schaechtle, Shivam Handa, Alexey Radul, Yutian Chen, and Martin Rinard. 2018. Probabilistic programming with programmable inference. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 603–616.
- McCallum et al. (2009) Andrew McCallum, Karl Schultz, and Sameer Singh. 2009. Factorie: Probabilistic programming via imperatively defined factor graphs. Advances in Neural Information Processing Systems 22 (2009).
- Milch et al. (2007) Brian Milch, Bhaskara Marthi, Stuart Russell, David Sontag, Daniel L Ong, and Andrey Kolobov. 2007. BLOG: Probabilistic models with unknown objects. (2007).
- Milch et al. (2005) Brian Milch, Bhaskara Marthi, David Sontag, Stuart Russell, Daniel L Ong, and Andrey Kolobov. 2005. Approximate inference for infinite contingent Bayesian networks. In International Workshop on Artificial Intelligence and Statistics. PMLR, 238–245.
- Minka (2012) Tom Minka. 2012. Infer. NET 2.5. http://research. microsoft. com/infernet (2012).
- Murray and Schön (2018) Lawrence M Murray and Thomas B Schön. 2018. Automated learning with a probabilistic programming language: Birch. Annual Reviews in Control 46 (2018), 29–43.
- Paisley et al. (2012) John Paisley, David Blei, and Michael Jordan. 2012. Variational Bayesian inference with stochastic search. arXiv preprint arXiv:1206.6430 (2012).
- Paquet (2021) Hugo Paquet. 2021. Bayesian strategies: probabilistic programs as generalised graphical models. In Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27–April 1, 2021, Proceedings 30. Springer International Publishing, 519–547.
- Ranganath et al. (2014) Rajesh Ranganath, Sean Gerrish, and David Blei. 2014. Black box variational inference. In Artificial intelligence and statistics. PMLR, 814–822.
- Ritchie et al. (2016) Daniel Ritchie, Andreas Stuhlmüller, and Noah Goodman. 2016. C3: Lightweight incrementalized MCMC for probabilistic programs using continuations and callsite caching. In Artificial Intelligence and Statistics. PMLR, 28–37.
- Roeder et al. (2017) Geoffrey Roeder, Yuhuai Wu, and David K Duvenaud. 2017. Sticking the landing: Simple, lower-variance gradient estimators for variational inference. Advances in Neural Information Processing Systems 30 (2017).
- Saad et al. (2021) Feras A Saad, Martin C Rinard, and Vikash K Mansinghka. 2021. SPPL: probabilistic programming with fast exact symbolic inference. In Proceedings of the 42nd acm sigplan international conference on programming language design and implementation. 804–819.
- Salvatier et al. (2016) John Salvatier, Thomas V Wiecki, and Christopher Fonnesbeck. 2016. Probabilistic programming in Python using PyMC3. PeerJ Computer Science 2 (2016), e55.
- Sampson et al. (2014) Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S McKinley, Dan Grossman, and Luis Ceze. 2014. Expressing and verifying probabilistic assertions. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 112–122.
- Schulman et al. (2015) John Schulman, Nicolas Heess, Theophane Weber, and Pieter Abbeel. 2015. Gradient estimation using stochastic computation graphs. Advances in neural information processing systems 28 (2015).
- Staton et al. (2016) Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. 2016. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. 525–534.
- Tolpin et al. (2015) David Tolpin, Jan-Willem van de Meent, and Frank Wood. 2015. Probabilistic programming in Anglican. In Machine Learning and Knowledge Discovery in Databases: European Conference, ECML PKDD 2015, Porto, Portugal, September 7-11, 2015, Proceedings, Part III 15. Springer, 308–311. https://probprog.github.io/anglican/
- Vákár et al. (2019) Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1–29.
- van de Meent et al. (2018) Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An introduction to probabilistic programming. arXiv preprint arXiv:1809.10756 (2018).
- Wingate et al. (2011) David Wingate, Andreas Stuhlmüller, and Noah Goodman. 2011. Lightweight implementations of probabilistic programming languages via transformational compilation. In Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics. JMLR Workshop and Conference Proceedings, 770–778.
- Wu et al. (2016) Yi Wu, Lei Li, Stuart Russell, and Rastislav Bodik. 2016. Swift: Compiled inference for probabilistic programming languages. arXiv preprint arXiv:1606.09242 (2016).
- Yang et al. (2014) Lingfeng Yang, Patrick Hanrahan, and Noah Goodman. 2014. Generating efficient MCMC kernels from probabilistic programs. In Artificial Intelligence and Statistics. PMLR, 1068–1076.
- Zhang et al. (2018) Cheng Zhang, Judith Bütepage, Hedvig Kjellström, and Stephan Mandt. 2018. Advances in variational inference. IEEE transactions on pattern analysis and machine intelligence 41, 8 (2018), 2008–2026.
## Appendix A Control-Flow Graph Construction
** Definition 0**
*A CFG is a tuple $(N_{\textnormal{start}},N_{\textnormal{end}},\mathcal{N},\mathcal{E})$ comprised of start and end node, a set of branch, join, and assign nodes, $\mathcal{N}$ , and a set of edges, $\mathcal{E}\subseteq\mathcal{N}^{*}\times\mathcal{N}^{*}$ , where $\mathcal{N}^{*}=\mathcal{N}\cup\{N_{\textnormal{start}},N_{\textnormal{end}}\}$ .*
- The CFG of a skip-statement, $$ , consists of only start and end node:
<details>
<summary>x11.png Details</summary>
### Visual Description
Icon/Small Image (118x21)
</details>
$G=\big{(}N_{\textnormal{start}},N_{\textnormal{end}},\emptyset,\{(N_{\textnormal{start}},N_{\textnormal{end}})\}\big{)}$
- The CFG of an assignment, $x=E$ , or sample statement $$ , is a sequence of start, assign, and end node:
<details>
<summary>x12.png Details</summary>
### Visual Description
Icon/Small Image (186x21)
</details>
<details>
<summary>x13.png Details</summary>
### Visual Description
Icon/Small Image (335x25)
</details>
$$
G=\big{(}N_{\textnormal{start}},N_{\textnormal{end}},\{A\},\{(N_{\textnormal{start}},A),(A,N_{\textnormal{end}})\}\big{)},
$$
where $A=\textnormal{Assign}(x=\dots)$ is the corresponding assign node.
- The CFG for a sequence of statements, $S=S_{1};S_{2}$ , is recursively defined by ”stitching together” the CFGs $G_{1}=(N_{\textnormal{start}}^{1},N_{\textnormal{end}}^{1},\mathcal{N}^{1},\mathcal{E}^{1})$ and $G_{2}=(N_{\textnormal{start}}^{2},N_{\textnormal{end}}^{2},\mathcal{N}^{2},\mathcal{E}^{2})$ of $S_{1}$ and $S_{2}$ :
<details>
<summary>x14.png Details</summary>
### Visual Description
Icon/Small Image (235x35)
</details>
| | $\displaystyle G=\big{(}$ | $\displaystyle N_{\textnormal{start}}^{1},\,N_{\textnormal{end}}^{2},\,\mathcal{N}^{1}\cup\mathcal{N}^{2},\,\mathcal{E}^{1}\setminus\{(N^{1}_{e},N_{\textnormal{end}}^{1})\}\cup\mathcal{E}^{2}\setminus\{(N_{\textnormal{start}}^{2},N^{2}_{s})\}\cup\{(N^{1}_{e},N^{2}_{s})\}\big{)},$ | |
| --- | --- | --- | --- |
where $N^{1}_{e}$ is the predecessor node of $N_{\textnormal{end}}^{1}$ in $G_{1}$ , $(N^{1}_{e},N_{\textnormal{end}}^{1})\in\mathcal{E}^{1}$ , and $N^{2}_{s}$ is the successor node of $N_{\textnormal{start}}^{2}$ in $G_{2}$ , $(N_{\textnormal{start}}^{2},N^{2}_{s})\in\mathcal{E}_{2}$ .
- The CFG of an if statement, $$ , is also defined in terms of the CFGs of $S_{1}$ and $S_{2}$ together with a branch node $B=\textnormal{Branch}(E)$ and a join node $J$ :
<details>
<summary>x15.png Details</summary>
### Visual Description
\n
## Diagram: Conditional Process Flowchart
### Overview
The image displays a simple, monochrome flowchart diagram illustrating a conditional process flow. The diagram uses standard flowchart symbols connected by directional arrows to depict a sequence of steps involving a decision point and two alternative paths that later converge.
### Components/Axes
The diagram consists of the following elements, arranged horizontally from left to right:
1. **START Node**: A rectangle on the far left containing the text "START".
2. **Decision Node (E)**: A diamond shape to the right of START, containing the letter "E". This represents a decision or evaluation point.
3. **Path Labels**:
* An arrow labeled "consequent" leads from the top vertex of the diamond "E" to the next node.
* An arrow labeled "alternative" leads from the bottom vertex of the diamond "E" to a different node.
4. **Process Nodes**:
* **G1**: A circle located above the central axis, connected by the "consequent" path.
* **G2**: A circle located below the central axis, connected by the "alternative" path.
5. **Merge Node**: A solid black diamond shape positioned to the right of G1 and G2. Both the path from G1 and the path from G2 connect to this node.
6. **END Node**: A rectangle on the far right containing the text "END", connected from the merge node.
### Detailed Analysis
* **Flow Direction**: The process flows unidirectionally from left (START) to right (END).
* **Decision Logic**: At node "E", the process splits into two mutually exclusive branches based on a condition:
* The **"consequent"** path (likely taken if the condition at E is true) leads to process G1.
* The **"alternative"** path (likely taken if the condition at E is false) leads to process G2.
* **Convergence**: Regardless of which path (G1 or G2) is taken, both branches merge at the solid black diamond before proceeding to the final END state. This indicates that the two alternative processes lead to the same subsequent step or termination point.
### Key Observations
1. **Symmetry**: The diagram is visually symmetrical along the horizontal axis, with G1 and G2 placed as mirror images above and below the central flow line.
2. **Symbol Conventions**: It uses standard flowchart symbols: rectangles for start/end, a diamond for a decision, and circles for processes or states. The solid black diamond is less standard but clearly functions as a merge or connector point.
3. **Clarity of Labels**: All text is clear, legible, and in English. The labels "consequent" and "alternative" explicitly define the logic of the decision branches.
### Interpretation
This diagram models a fundamental logical structure common in processes, algorithms, and workflows: **conditional branching with later convergence**.
* **What it demonstrates**: It shows that after an initial evaluation (E), the system or process can proceed in one of two distinct ways (G1 or G2). Crucially, these paths are not permanent forks; they are temporary alternatives that ultimately reunite. This structure is typical for handling "if-then-else" scenarios where different actions are taken based on a condition, but the overall process must continue to a common conclusion.
* **Relationship between elements**: The START and END nodes frame the entire process. The decision node "E" is the critical control point. The circles G1 and G2 represent the core alternative actions or states. The merge node ensures that the process flow is recombined, maintaining a single path to completion.
* **Notable implication**: The use of "consequent" and "alternative" rather than "true/false" or "yes/no" suggests the decision at E might be based on a more complex condition or evaluation, not just a binary check. The diagram's simplicity makes it a versatile template for representing any process with a single decision point and two rejoining paths.
</details>
| | $\displaystyle G=\big{(}$ | $\displaystyle N_{\textnormal{start}},\,N_{\textnormal{end}},\,\mathcal{N}^{1}\cup\mathcal{N}^{2}\cup\{B,J\},$ | |
| --- | --- | --- | --- |
The nodes $N^{1}_{s}$ , $N^{1}_{e}$ , $N^{2}_{s}$ , $N^{2}_{e}$ are defined as in the last case. This construction assumes that $\mathcal{E}^{1}\neq\emptyset$ and $\mathcal{E}^{2}\neq\emptyset$ . Otherwise, the branch would be a skip statement and we would connect $B$ with $J$ directly. The two predecessors of $J$ are denoted with $\textnormal{predcon}(J)$ and $\textnormal{predalt}(J)$ depending on the path.
- The CFG of $$ is given in terms of the sub-cfg $G_{S}$ of statement $S$ .
<details>
<summary>x16.png Details</summary>
### Visual Description
## Diagram: State Transition Flowchart
### Overview
The image displays a simple state transition diagram or flowchart, illustrating a process flow with a conditional loop. The diagram consists of five distinct nodes connected by directional arrows, indicating the sequence and logic of the process. The primary language is English.
### Components/Axes
The diagram is composed of the following labeled components, arranged from left to right:
1. **START Node**: A rectangular box containing the text "START". Positioned at the far left.
2. **Decision Node (E)**: A diamond-shaped box containing the letter "E". Positioned to the right of the START node.
3. **Loop/State Node (Gₛ)**: A circular node containing the text "Gₛ" (where "s" is a subscript). Positioned above and to the right of the Decision Node (E).
4. **Termination Node**: A solid, filled black diamond shape. Positioned to the right of the Decision Node (E).
5. **END Node**: A rectangular box containing the text "END". Positioned at the far right.
**Connections (Arrows):**
* A single arrow points from the **START** node to the **Decision Node (E)**.
* From the **Decision Node (E)**, two arrows emerge:
* One arrow points upward and to the right, leading to the **Gₛ** node.
* Another arrow points directly to the right, leading to the **filled black diamond**.
* An arrow points from the **Gₛ** node back to the **Decision Node (E)**, creating a loop.
* An arrow points from the **filled black diamond** to the **END** node.
### Detailed Analysis
The diagram defines a process with a single decision point that can lead to either a repetitive loop or a direct termination.
* **Flow Path 1 (Looping Path):** START → E → Gₛ → E → ... This path indicates that after reaching state "E", the process can transition to state "Gₛ", which then returns control to "E". This creates a potential infinite loop or a repetitive cycle between states E and Gₛ.
* **Flow Path 2 (Termination Path):** START → E → [Filled Diamond] → END. This path indicates that from state "E", the process can also transition to a terminal condition (represented by the filled diamond), which then leads directly to the END state.
### Key Observations
1. **Asymmetric Decision:** The decision node "E" has two possible outcomes, but they are not symmetric. One leads to a loop (Gₛ), and the other leads to termination.
2. **Visual Distinction of Termination:** The termination condition is uniquely represented by a solid black diamond, visually distinguishing it from the other nodes (outline shapes) and emphasizing its role as a final or absorbing state before the END.
3. **Subscript Notation:** The label "Gₛ" uses a subscript "s", which is a specific technical notation. This could denote a specific type of state, a generator, a goal state, or a state dependent on a parameter 's'.
4. **No Explicit Conditions:** The diagram does not label the arrows with the conditions that trigger each transition (e.g., "if condition X, go to Gₛ; else, go to termination"). The logic is implied by the structure.
### Interpretation
This diagram models a system or algorithm with a core operational state (E) that can engage in a sub-process or feedback loop (Gₛ) before potentially returning to re-evaluate. The presence of the filled diamond suggests a distinct, possibly irreversible, condition that must be met to exit the loop and conclude the process.
**Possible Technical Contexts:**
* **Algorithm Design:** It could represent a loop in a program where "E" is an evaluation step, "Gₛ" is a step that modifies a state or generates a candidate solution, and the filled diamond represents a convergence criterion or success condition being met.
* **State Machine:** In a finite state machine, "E" might be an active state, "Gₛ" a transient or helper state, and the filled diamond a final or accepting state.
* **Process Control:** It could model a quality control loop where "E" is an inspection, "Gₛ" is a corrective action, and the filled diamond is the point where the product passes inspection and moves to packaging (END).
The absence of explicit conditional labels means the precise logic (what causes the transition to Gₛ vs. the filled diamond) is not defined by the diagram alone; it would be specified in accompanying text or system specifications. The diagram's primary function is to visually communicate the existence of a loop and an alternate exit path from the central decision point.
</details>
| | $\displaystyle G=\big{(}$ | $\displaystyle N_{\textnormal{start}},\,N_{\textnormal{end}},\,\mathcal{N}^{S}\cup\{B,J\},$ | |
| --- | --- | --- | --- |
where $G_{S}=(N_{\textnormal{start}}^{S},N_{\textnormal{end}}^{S},\mathcal{N}^{S},\mathcal{E}^{S})$ .
Again, if $$ , then we would have the edge $(B,B)$ instead of $(B,N^{S}_{s})$ and $(N^{S}_{e},B)$ .
- The unrolled CFG of $$ is defined as follows:
<details>
<summary>x17.png Details</summary>
### Visual Description
\n
## Process Flow Diagram: Decision-State Pathway
### Overview
The image displays a technical process flow diagram (PFD) or state transition diagram. It illustrates a sequential pathway from a starting point to an endpoint, characterized by alternating decision points and state nodes, with one conditional or alternative path indicated. The diagram uses standard flowchart symbols and is rendered in a monochrome, technical style.
### Components/Axes
The diagram is composed of the following elements, arranged primarily in a left-to-right flow with some diagonal connections:
1. **Terminal Symbols (Rectangles):**
* **START**: Located at the far left. This is the entry point of the process.
* **END**: Located at the far right. This is the termination point of the process.
2. **Decision Symbols (Diamonds):**
* Three diamonds, each labeled with the letter **"E"**. These represent decision points, evaluations, or events within the process flow.
* One **solid black diamond**. This typically represents a merge point, a synchronization node, or a final decision where multiple paths converge.
3. **Process/State Symbols (Circles):**
* Two circles, each labeled **"Gs"**. These represent processes, operations, or, more likely given the context, specific states (e.g., "Goal State").
4. **Connector Lines:**
* **Solid lines with arrows**: Indicate the primary, mandatory flow of the process.
* **Dashed line with an arrow**: Indicates an alternative, conditional, or optional path.
5. **Annotation:**
* An **ellipsis ("...")** is placed near the dashed line, suggesting an omitted sequence, an iterative loop, or an unspecified number of repetitions for that alternative path.
### Detailed Analysis
**Flow and Connectivity:**
1. The process initiates at **START**.
2. A solid arrow leads to the first **Decision (E)**.
3. From the first **E**, a solid arrow leads to the first **State (Gs)**.
4. From the first **Gs**, a solid arrow leads to the second **Decision (E)**.
5. From the second **E**, a solid arrow leads to the second **State (Gs)**.
6. From the second **Gs**, a solid arrow leads to the third **Decision (E)**.
7. From the third **E**, the path splits:
* **Primary Path (Solid Line):** A solid arrow leads directly to the **Black Diamond (Merge Point)**.
* **Alternative Path (Dashed Line):** A dashed arrow, accompanied by an ellipsis ("..."), also leads to the **Black Diamond**. This suggests that after the third decision, there may be an optional or conditional sub-process (represented by "...") before merging back into the main flow.
8. From the **Black Diamond**, a final solid arrow leads to **END**.
**Spatial Grounding:**
* The **START** box is positioned at the vertical center-left.
* The **END** box is positioned at the bottom-right.
* The main sequence of **E -> Gs -> E -> Gs -> E** forms a slightly ascending diagonal line from left to right.
* The **Black Diamond** is positioned below and to the right of the third **E**, creating a convergence point.
* The **ellipsis ("...")** is positioned above the dashed line, near the third **E**.
### Key Observations
1. **Alternating Pattern:** The core process follows a strict alternating pattern of Decision (E) -> State (Gs) -> Decision (E) -> State (Gs) -> Decision (E).
2. **Path Divergence and Convergence:** A key structural feature is the divergence after the third decision point into two paths (one solid, one dashed) that subsequently converge at the black diamond. This is the most complex part of the diagram.
3. **Symbol Consistency:** All decision points are labeled identically ("E"), and both state nodes are labeled identically ("Gs"). This implies they represent the same type of action or condition each time they appear.
4. **Monochrome Design:** The diagram uses only black lines and text on a white background, emphasizing function over aesthetics, typical of technical documentation.
### Interpretation
This diagram models a **structured, iterative decision-making process**. The "E" likely stands for **"Evaluation," "Event," or "Examination,"** while "Gs" likely stands for **"Goal State" or "Generated State."**
The process suggests a cycle where an evaluation leads to a new state, which then triggers another evaluation, and so on. The critical insight is at the third evaluation point, where the process offers a choice:
* Proceed directly to the merge point (the solid line path).
* Undertake an alternative or extended sub-process (the dashed line path with "..."), the details of which are abstracted away, before merging back.
The **black diamond** acts as a **synchronization barrier** or **final decision gate**. All paths, whether the direct one or the extended alternative, must reach this point before the process can conclude at **END**.
**Underlying Logic:** The diagram could represent anything from a software algorithm with a conditional loop, a business process with an exception-handling path, a scientific method with an iterative testing phase, or a strategic planning model with a contingency branch. The abstraction (using "E" and "Gs") makes it a generic template for any process requiring sequential evaluations leading to states, with a built-in option for a more complex path before finalization. The ellipsis is crucial—it signifies that the alternative path's complexity is acknowledged but deliberately not detailed in this high-level view.
</details>
| | $\displaystyle G=\big{(}$ | $\displaystyle N_{\textnormal{start}},\,N_{\textnormal{end}},$ | |
| --- | --- | --- | --- |
where $G_{S_{i}}=(N_{\textnormal{start}}^{S_{i}},N_{\textnormal{end}}^{S_{i}},\mathcal{N}^{S_{i}},\mathcal{E}^{S_{i}})$ is the $i$ -th copy of sub-graph $G_{S}$ . $N^{S_{i}}_{s}$ and $N^{S_{i}}_{e}$ are defined as in the cases before.
If $$ , then we would have the edges $(B_{i},B_{i+1})$ instead of the edges $(B_{i},N^{S_{i}}_{s})$ and $(N^{S_{i}}_{e},B_{i+1})$ .
## Appendix B Proofs of Sections 2-4
### B.1. Proof of Proposition 2
Statement. For all programs $S$ without while loops and corresponding control-flow graph $G$ , it holds that for all traces $\mathtt{tr}$ and all initial states $\sigma_{0}$
$$
{\bar{p}_{S}(\mathtt{tr},\sigma_{0})=\bar{p}_{G}(\mathtt{tr},\sigma_{0}).}
$$
* Proof*
With structural induction we prove the more general equivalence:
$$
(\sigma,S)\Downarrow^{\mathtt{tr}}\sigma^{\prime}\iff(\sigma,\text{START})\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}\dots\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime},\text{END}).
$$ We write $\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}$ to indicate that the predecessor-successor relationship follow the CFG of program $S$ . For programs consisting of a single skip, assignment, or sample statement, the equality can be seen by directly comparing the operational semantic rules to the graph semantics. For sequence $S=(S_{1};S_{2})$ , by induction assumption we have
| | $\displaystyle(\sigma,S_{1})\Downarrow^{\mathtt{tr}}\sigma^{\prime}$ | $\displaystyle\iff(\sigma,N_{\text{start}}^{1})\underset{S_{1}}{\overset{\mathtt{tr}}{\longrightarrow}}\dots\underset{S_{1}}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime}_{1},N^{1})\underset{S_{1}}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime},N_{\text{end}}^{1})$ | |
| --- | --- | --- | --- |
By definition of the CFG of $S$ , we see that
$$
(\sigma,S)\Downarrow^{\mathtt{tr}}\sigma^{\prime\prime}\iff(\sigma,N_{\text{start}}^{1})\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}\dots\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime}_{1},N^{1})\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime},N^{2})\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}\dots\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime\prime},N_{\text{end}}^{2})
$$ In a similar way, we proof the result for if statements $$ by considering the two cases $\sigma(E)=\mathtt{true}$ and $\sigma(E)=\mathtt{false}$ .
$$
(\sigma,S)\Downarrow^{\mathtt{tr}}\sigma^{\prime}\iff(\sigma,N_{\text{start}})\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma,\text{Branch}(E))\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}\dots\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime},N_{\text{join}})\underset{S}{\overset{\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime},N_{\text{end}})
$$
Depending on the case, we replace the dots with the path of $S_{i}$ without the start and end nodes. Note that in our notation in both cases $(\sigma,S_{i})\Downarrow^{\mathtt{tr}}\sigma^{\prime}$ . ∎
### B.2. Proof of Proposition 9
To prove soundness of Algorithm 1, we list properties of the provenance set that will become useful in subsequent proofs.
** Lemma 0**
*Let $N$ be a CFG node and $x$ a variable. prov has following properties:
- For all nodes $N^{\prime}$ it holds that
$$
\displaystyle\textnormal{RD}(N,x)=\textnormal{RD}(N^{\prime},x)\implies\textnormal{prov}(N,x)=\textnormal{prov}(N^{\prime},x). \tag{11}
$$
- If $N^{\prime}\in\textnormal{RD}(N,x)$ is an assignment node, $N^{\prime}=\textnormal{Assign}(x=E)$ , then
$$
\displaystyle\textnormal{prov}(N^{\prime},E)=\textstyle\bigcup_{y\in\textnormal{vars}(E)}\textnormal{prov}(N^{\prime},y)\subseteq\textnormal{prov}(N,x). \tag{12}
$$
- if $N^{\prime}\in\textnormal{RD}(N,x)$ is a sample node, $$ , then
$$
\displaystyle\textnormal{prov}(N^{\prime},E_{0})\subseteq\textnormal{prov}(N,x)\quad\text{and}\quad\textnormal{addresses}(N^{\prime})\subseteq\textnormal{prov}(N,x). \tag{13}
$$
- For all $N^{\prime}\in\textnormal{RD}(N,x)$ it holds that for all branch parents $N_{\text{bp}}=\textnormal{Branch}(E_{N_{\text{bp}}})\in\textnormal{BP}(N^{\prime})$ we have $\textnormal{prov}(N_{\text{bp}},E_{N_{\text{bp}}})\subseteq\textnormal{prov}(N,x)$ and
$$
\displaystyle\begin{split}\textstyle\bigcup_{N_{\text{bp}}\in\textnormal{BP}(N^{\prime})}\textnormal{prov}(N_{\text{bp}},E_{N_{\text{bp}}})=\textstyle\bigcup_{N_{\text{bp}}\in\textnormal{BP}(N^{\prime})}\textstyle\bigcup_{y\in\textnormal{vars}(E_{N_{\text{bp}}})}\textnormal{prov}(N_{\text{bp}},y)\subseteq\textnormal{prov}(N,x).\end{split} \tag{14}
$$*
* Proof*
If $(N^{\prime},y)$ is pushed into the queue, then $\textnormal{prov}(N^{\prime},y)\subseteq\textnormal{prov}(N,x)$ as the algorithm for computing $\textnormal{prov}(N^{\prime},y)$ starts with only $(N^{\prime},y)$ in the queue. With this fact the properties follow directly from the definition of the algorithm. ∎
Statement. Let $G$ be the CFG of a program $S$ without while loop statements. For each node $N$ and variable $x$ , there exists an evaluation function
$$
V^{N}_{x}\in[\mathcal{T}|_{\textnormal{prov}(N,x)}\to\mathcal{V}],
$$
such that for all traces $\mathtt{tr}$ , initial program state $\sigma_{0}$ as in Definition 1, and execution sequence
$$
(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},N_{i})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{l},\text{END})
$$
we have
$$
\sigma_{i}(x)=V^{N_{i}}_{x}(\mathtt{tr}).
$$
In the proof we also use the evaluation function of expressions $V^{N}_{E}\in[\mathcal{T}|_{\textnormal{prov}(N,E)}\to\mathcal{V}]$ , where $V^{N}_{c}(\mathtt{tr})=c$ and $V^{N}_{g(E_{1},\dots,E_{n})}(\mathtt{tr})=g(V^{N}_{E_{1}}(\mathtt{tr}),\dots,V^{N}_{E_{n}}(\mathtt{tr})).$
* Proof*
Step 1. Defining $V^{N}_{x}$ and proving $V^{N}_{x}\in[\mathcal{T}|_{\textnormal{prov}(N,x)}\to\mathcal{V}]$ . We begin by defining $V^{N}_{x}$ inductively by noting that every node $N\neq\text{START}$ has exactly one predecessor except for join nodes which have two predecessors. Further, the CFG $G$ is a finite directed acyclic graph with a single root node which makes mathematical induction possible. Base case. For $((x_{i}\mapsto\mathtt{null},\textbf{p}\mapsto 1),\text{START})$ , let $V^{\text{START}}_{\textbf{p}}(\mathtt{tr})=1$ and $V^{\text{START}}_{x}(\mathtt{tr})=\mathtt{null}$ for all variables $x$ . We have $V^{\text{START}}_{x}\in[\mathcal{T}|_{\emptyset}\to\mathcal{V}]$ . Induction step. Case 1. Let $N$ be a node with single predecessor $N^{\prime}$ ( $N$ is not a join node). We define $V^{N}_{x}$ based on the node type of $N^{\prime}$ , for which we make the induction assumption that the evaluation function $V^{N^{\prime}}_{x}\in[\mathcal{T}|_{\textnormal{prov}(N^{\prime},x)}\to\mathcal{V}]$ exists for all variables.
- Case 1.1. $N^{\prime}$ is an assignment node, $N^{\prime}=\textnormal{Assign}(z=E)$ . Define
$$
V^{N}_{y}(\mathtt{tr})=\begin{cases}V^{N^{\prime}}_{E}(\mathtt{tr})&\text{if}\,y=z\\
V^{N^{\prime}}_{y}(\mathtt{tr})&\text{otherwise}.\end{cases}
$$
By assumption $V^{N^{\prime}}_{y}\in[\mathcal{T}|_{\textnormal{prov}(N^{\prime},y)}\to\mathcal{V}]$ for all $y$ and thus, $V^{N^{\prime}}_{E}\in[\mathcal{T}|_{\textnormal{prov}(N^{\prime},E)}\to\mathcal{V}]$ .
For $x\neq z$ , $\textnormal{RD}(N,x)=\textnormal{RD}(N^{\prime},x)$ and by Eq. 11 we have $\textnormal{prov}(N,x)=\textnormal{prov}(N^{\prime},x)$ , implying that $V^{N}_{x}\in[\mathcal{T}|_{\textnormal{prov}(N,x)}\to\mathcal{V}]$ .
For $x=z$ , $\textnormal{RD}(N,x)=\{N^{\prime}\}$ since $N^{\prime}$ is the single predecessor of $N$ and assigns $x$ . By Eq. 12 $\textnormal{prov}(N^{\prime},E)\subseteq\textnormal{prov}(N,x)$ , and by Eq. 4
$$
V^{N}_{x}=V^{N^{\prime}}_{E}\in[\mathcal{T}|_{\textnormal{prov}(N^{\prime},E)}\to\mathcal{V}]\subseteq[\mathcal{T}|_{\textnormal{prov}(N,x)}\to\mathcal{V}].
$$
- Case 1.2. $N^{\prime}$ is a sample node, $$ . Define
$$
V^{N}_{y}(\mathtt{tr})=\begin{cases}\mathtt{tr}(V^{N^{\prime}}_{E_{0}}(\mathtt{tr}))&\text{if}\,y=z\\
V^{N^{\prime}}_{y}(\mathtt{tr})&\text{otherwise.}\end{cases}
$$
As before, for $x\neq z$ , $V^{N}_{x}\in[\mathcal{T}|_{\textnormal{prov}(N,x)}\to\mathcal{V}]$ .
For $x=z$ , by definition $V^{N^{\prime}}_{E_{0}}(\mathtt{tr})\in\textnormal{addresses}(N^{\prime})$ . Since $N^{\prime}\in\textnormal{RD}(N,x)=\{N^{\prime}\}$ it follows from Eq. 13 that $\textnormal{addresses}(N^{\prime})\subseteq\textnormal{prov}(N,x)$ and $\textnormal{prov}(N^{\prime},E_{0})\subseteq\textnormal{prov}(N,x)$ . By Eq. 4
$$
V^{N}_{x}\in[\mathcal{T}|_{\textnormal{addresses}(N^{\prime})\cup\textnormal{prov}(N^{\prime},E_{0})}\to\mathcal{V}]\subseteq[\mathcal{T}|_{\textnormal{prov}(N,x)}\to\mathcal{V}].
$$
- Case 1.3. $N^{\prime}$ is a branch or join node. Define $V^{N}_{y}=V^{N^{\prime}}_{y}$ for all variables $y$ . Case 2. Let $J$ be a join node with two predecessor nodes, $N^{\prime}_{1}=\text{predcons}(J)$ , $N^{\prime}_{2}=\text{predalt}(J)$ . Let $B=\text{Branch}(E)$ be the corresponding branching node, $(B,J)\in\textnormal{BranchJoin}(G)$ . For variable $x$ , there are two cases:
1. There exists a reaching definition $N^{\prime}\in\textnormal{RD}(J,x)$ on a path $(B,\dots,N^{\prime},\dots,J)$ . Define $V^{1}_{x}$ and $V^{2}_{x}$ depending on the node type of $N^{\prime}_{1}$ and $N^{\prime}_{2}$ as in step 1. The functions $V^{i}_{x}$ compute the value of $x$ after executing $N^{\prime}_{i}$ . As before one can see that $V^{i}_{x}\in[\mathcal{T}|_{\textnormal{prov}(J,x)}\to\mathcal{V}]$ . Let
$$
V^{J}_{x}(\mathtt{tr})\coloneqq\textnormal{ife}(V^{B}_{E}(\mathtt{tr}),V^{1}_{x}(\mathtt{tr}),V^{2}_{x}(\mathtt{tr}))=\begin{cases}V^{1}_{x}(\mathtt{tr})&\text{if }V^{B}_{E}(\mathtt{tr})=\mathtt{true},\\
V^{2}_{x}(\mathtt{tr})&\text{otherwise.}\end{cases}
$$
Since $B\in\textnormal{BP}(N^{\prime})$ , by Eq. 14 $\textnormal{prov}(B,E)\subseteq\textnormal{prov}(J,x)$ and thus $V^{J}_{x}\in[\mathcal{T}|_{\textnormal{prov}(J,x)}\to\mathcal{V}]$ .
1. All reaching definitions of $x$ (if there are any) are predecessors of $B$ . Then, $\textnormal{RD}(J,x)=\textnormal{RD}(B,x)$ and by Eq. 11 $\textnormal{prov}(J,x)=\textnormal{prov}(B,x)$ . Define $V^{J}_{x}\coloneqq V^{B}_{x}.$ Step 2: Proving that $\sigma_{i}(x)=V^{N_{i}}_{x}(\mathtt{tr})$ . Having defined the evaluation functions, we now have to prove that they indeed compute the correct values. For trace $\mathtt{tr}$ let the corresponding execution sequence be
$$
(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},N_{i})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{l},\text{END}).
$$
We will prove that $\sigma_{i}(x)=V^{N_{i}}_{x}(\mathtt{tr})$ by induction. Base case. The base case immediately follows from the definition $\sigma_{0}(x)=V^{\text{START}}_{x}(\mathtt{tr})$ . Induction step. For transition $(\sigma_{i},N_{i})\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i+1},N_{i+1})$ the assumption is that $\sigma_{j}(x)=V^{N_{j}}_{x}(\mathtt{tr})$ holds for all variables $x$ and $j\leq i$ . If $N_{i+1}$ is not a join node, then $\sigma_{i+1}(x)=V^{N_{i+1}}_{x}(\mathtt{tr})$ follows directly from the CFG semantics and definition of $V^{N_{i+1}}_{x}$ in case 1 of step 1. Lastly, we consider the case when $N_{i+1}$ is a join node with branching node $N_{j}=\text{Branch}(E)$ , $(N_{j},N_{i+1})\in\text{BranchJoin}(G)$ , for some $j\leq i$ . Let $N^{\prime}_{1}=\text{predcons}(N_{i+1})$ , $N^{\prime}_{2}=\text{predalt}(N_{i+1})$ . By the semantics of if statements, $V^{B}_{E}(\mathtt{tr})=\mathtt{true}$ iff $N_{i}=N^{\prime}_{1}$ and $V^{B}_{E}(\mathtt{tr})=\mathtt{false}$ iff $N_{i}=N^{\prime}_{2}$ . If there is a node $N^{\prime}$ between $N_{j}$ and $N_{i+1}$ in the execution sequence that assigns $x$ , $N^{\prime}\in\textnormal{RD}(N_{i+1},x)$ , then by definitions of $V^{1}_{x}$ , $V^{2}_{x}$ , and $V^{N_{i+1}}_{x}$ we have
$$
\sigma_{i+1}(x)=\textnormal{ife}(V^{B}_{E}(\mathtt{tr}),V^{1}_{x}(\mathtt{tr}),V^{2}_{x}(\mathtt{tr}))=V^{N_{i+1}}_{x}(\mathtt{tr}).
$$
If there is no such $N^{\prime}$ , then
$$
\sigma_{i+1}(x)=\sigma_{j}(x)=V^{N_{j}}_{x}(\mathtt{tr})=V^{N_{i+1}}_{x}(\mathtt{tr}).
$$ ∎
### B.3. Proof of Proposition 1
Statement. For all program $S$ with CFG $G$ and unrolled CFG $H$ , it holds that for all traces $\mathtt{tr}$ and initial states $\sigma_{0}$
$$
{\bar{p}_{S}(\mathtt{tr},\sigma_{0})=\bar{p}_{G}(\mathtt{tr},\sigma_{0})=\bar{p}_{H}(\mathtt{tr},\sigma_{0}).}
$$
* Proof*
We continue the proof of Proposition 2 for a while statement. Note the well-known equivalence for while statements in terms of the operational semantics:
Thus, if the program terminates for $\mathtt{tr}$ , it is equivalent to $S;\dots;S$ ( $S$ repeated $n$ times), where $\sigma_{0}=\sigma$ , $(\sigma_{i},S)\Downarrow^{\mathtt{tr}}\sigma_{i+1}$ , $\sigma_{n}=\sigma^{\prime}$ , such that $\sigma_{i}(E)=\mathtt{true}$ for $i<n$ , $\sigma_{n}(E)=\mathtt{false}$ . In this case, it can be shown that the (unrolled) CFG of $S;\dots;S$ is also equivalent to the (unrolled) CFG of the while statement. If the program does not terminate, then ${\bar{p}_{S}(\mathtt{tr},\sigma_{0})=\bar{p}_{G}(\mathtt{tr},\sigma_{0})=\bar{p}_{H}(\mathtt{tr},\sigma_{0})}=\textnormal{undefined}$ . ∎
### B.4. Proof of Lemma 3
Statement. Let $G$ be the CFG and $H$ the unrolled CFG of program $S$ . For each node $M\in H$ following equation holds.
$$
\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{RD}(M,x)\}\subseteq\textnormal{RD}(\iota_{\textnormal{cfg}}(M),x) \tag{15}
$$
* Proof*
We will prove following Lemma by structural induction: Lemma. For every path $\vv{M}=(M^{\prime},\dots,M)$ in the unrolled CFG $H$ , there is a path in the CFG $G$ , $\vv{N}=(N^{\prime},\dots,N)$ , such that
$$
\iota_{\textnormal{cfg}}(M^{\prime})=N^{\prime},\quad\iota_{\textnormal{cfg}}(M)=N,
$$
$$
\textnormal{AssignNodes}(\vv{N},x)=\left\{\iota_{\textnormal{cfg}}(M_{i})\colon M_{i}\in\textnormal{AssignNodes}(\vv{M},x)\right\}=\textnormal{AssignNodes}_{\textnormal{cfg}}(\vv{M},x),
$$
for all variables $x$ , where $\textnormal{AssignNodes}(\vv{N},x)$ is the set of all CFG nodes that assign $x$ in path $\vv{N}$ and $\textnormal{AssignNodes}_{\textnormal{cfg}}(\vv{M},x)$ is the set of all assign nodes in path $\vv{M}$ mapped to $G$ with $\iota_{\textnormal{cfg}}$ . With this lemma we can prove the statement: Let $M^{\prime}\in\textnormal{RD}(M,x)$ . Thus, there exists a path $\vv{M}=(M^{\prime},\dots,M)$ , such that $M^{\prime}$ is the only assign node for $x$ before $M$ . By the lemma, there is a path in the CFG $\vv{N}=(N^{\prime},\dots,N)$ , such that $\iota_{\textnormal{cfg}}(M^{\prime})=N^{\prime}$ and $\iota_{\textnormal{cfg}}(M)=N$ . Further, since $\textnormal{AssignNodes}(\vv{N},x)=\textnormal{AssignNodes}_{\textnormal{cfg}}(\vv{M},x)\subseteq\{\iota_{\textnormal{cfg}}(M^{\prime}),\iota_{\textnormal{cfg}}(M)\}=\{N^{\prime},N\}$ , the node $N^{\prime}$ is also the only node in the path $\vv{N}$ before $N$ that assigns $x$ . Thus, $\iota_{\textnormal{cfg}}(M^{\prime})=N^{\prime}\in\textnormal{RD}(N,x)=\textnormal{RD}(\iota_{\textnormal{cfg}}(M),x).$ Proof of Lemma. By structural induction. For CFGs consisting only of a single assign node, the unrolled CFGs are identical and the statement follows. For a sequence of two statements $(S_{1};S_{2})$ , let $G$ be the CFG with sub-graphs $G_{1}$ and $G_{2}$ for statements $S_{1}$ and $S_{2}$ respectively. Let $H$ the unrolled CFG with sub-graphs $H_{1}$ and $H_{2}$ . We consider the only interesting case where $M^{\prime}\in H_{1}$ and $M\in H_{2}$ :
$$
\vv{M}=(\underbrace{M,\dots,M_{i}}_{\in H_{1}},\underbrace{M_{i+1},\dots,M}_{\in H_{2}}).
$$
For sub-paths $\vv{M_{1}}\coloneqq(M,\dots,M_{i},\textnormal{END})$ and $\vv{M_{2}}\coloneqq(\textnormal{START},M_{i+1},\dots,M)$ we apply the induction assumption to get two paths $\vv{N_{1}}=(N^{\prime},\dots,N_{1},\text{END})$ , $\vv{N_{2}}=(\text{START},N_{2},\dots,N)$ , with $\iota_{\textnormal{cfg}}(M^{\prime})=N^{\prime}$ and $\iota_{\textnormal{cfg}}(M)=N$ . The corresponding CFG path in $G$ is $\vv{N}\coloneqq(N^{\prime},\dots,N_{1},N_{2},\dots,N)$ as
| | $\displaystyle\textnormal{AssignNodes}_{\textnormal{cfg}}(\vv{M},x)$ | $\displaystyle=\textnormal{AssignNodes}_{\textnormal{cfg}}(\vv{M_{1}},x)\cup\textnormal{AssignNodes}_{\textnormal{cfg}}(\vv{M_{2}},x)$ | |
| --- | --- | --- | --- | For an if statement, let $G$ be the CFG with branch node $\tilde{B}$ , join node $\tilde{J}$ , and sub-graphs $G_{1}$ , $G_{2}$ . Let $H$ be the unrolled CFG with corresponding $B$ , $J$ , $H_{1}$ , and $H_{2}$ . We only show the statement for the case
$$
\vv{M}=(B,\underbrace{M^{\prime},\dots,M}_{\in H_{i}},J).
$$
Again, we apply the induction assumption to $\vv{M_{i}}\coloneqq(\textnormal{START},M^{\prime},\dots,M,\textnormal{END})$ and get a path in $G_{i}$ : $\vv{N_{i}}=(\textnormal{START},N^{\prime},\dots,N,\textnormal{END})$ . Since $\iota_{\textnormal{cfg}}(B)=\tilde{B}$ , $\iota_{\textnormal{cfg}}(J)=\tilde{J}$ , which are not assign nodes, and $\textnormal{AssignNodes}(\vv{N_{i}})=\textnormal{AssignNodes}_{\textnormal{cfg}}(\vv{M_{i}})$ , the statement follows for the path $(\tilde{B},N^{\prime},\dots,N,\tilde{J})$ . Lastly, for a while loop, let $G$ be the CFG with branch node $\tilde{B}$ , join node $\tilde{J}$ , and sub-graph $G_{S}$ . Let $H$ be the unrolled CFG with $B_{i}$ branch nodes, $J$ join node, and $H_{i}$ sub-graphs. For the sake of brevity we consider three cases: - For $M^{\prime}\in H_{i}$ and $M\in H_{j}$
$$
\vv{M}=(\underbrace{M^{\prime},\dots,M_{i}}_{\in H_{i}},B_{i+1},\dots,B_{j},\underbrace{M_{j},\dots,M}_{\in H_{j}})
$$
we apply the induction assumption to the sub-paths and construct the path
$$
\vv{N}=(\underbrace{N^{\prime},\dots,N_{i}}_{\in G_{S}},\tilde{B},\dots,\tilde{B},\underbrace{N_{j},\dots,N}_{\in G_{S}}))
$$
where $\tilde{B}$ and $B_{i}$ are do not contribute to $\textnormal{AssignNodes}(\vv{N})$ or $\textnormal{AssignNodes}(\vv{M})$ .
- For $M^{\prime}\in H_{i}$ and $J$
$$
\vv{M}=(\underbrace{M^{\prime},\dots,M_{i}}_{\in H_{i}},B_{i+1},\dots,B_{l},J)
$$
we construct the path
$$
\vv{N}=(\underbrace{N^{\prime},\dots,N_{i}}_{\in G_{S}},\tilde{B},\dots,\tilde{B},\tilde{J})
$$
- For the path $\vv{M}=(B_{l},J)$ the path in the CFG is $\vv{N}=(\tilde{B},\tilde{J})$ .
∎
Statement. Let $G$ be the CFG and $H$ the unrolled CFG of program $S$ . For each node $M\in H$ the following equation holds.
$$
\textnormal{BP}_{\textnormal{cfg}}(M)\coloneqq\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{BP}(M)\}=\textnormal{BP}(\iota_{\textnormal{cfg}}(M)) \tag{16}
$$
* Proof*
We prove this statement by structural induction. For CFGs only consisting of a single assign node, the unrolled CFGs are identical, there are no branch parents, and the statement follows. The sequencing of two statements $(S_{1};S_{2})$ does not change the branch parents of any node. For an if statement, let $G$ be the CFG with branch node $\tilde{B}$ , join node $\tilde{J}$ , and sub-graphs $G_{1}$ , $G_{2}$ . Let $H$ be the unrolled CFG with corresponding $B$ , $J$ , $H_{1}$ , and $H_{2}$ . Every node $M$ in $H_{i}$ has branch parents $\left(\textnormal{BP}(M)\cap H_{i}\right)\cup\{B\}$ . By induction assumption $\textnormal{BP}_{\textnormal{cfg}}(M)\cap G_{i}=\textnormal{BP}(\iota_{\textnormal{cfg}}(M))\cap G_{i}$ and thus
| | $\displaystyle\textnormal{BP}_{\textnormal{cfg}}(M)$ | $\displaystyle=\left\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{BP}(M)\cap H_{i}\right\}\cup\{\iota_{\textnormal{cfg}}(B)\}$ | |
| --- | --- | --- | --- |
Nodes $B$ , $\tilde{B}$ , $J$ , and $\tilde{J}$ do not have branch parents. Lastly, for a while loop, let $G$ be the CFG with branch node $\tilde{B}$ , join node $\tilde{J}$ , and sub-graph $G_{S}$ . Let $H$ be the unrolled CFG with $B_{i}$ branch nodes, $J$ join node, and $H_{i}$ sub-graphs. Every node $M$ in $H_{i}$ has branch parents $\left(\textnormal{BP}(M)\cap H_{i}\right)\cup\{B_{1},\dots,B_{i}\}$ . The CFG node $\iota_{\textnormal{cfg}}(M)\in G_{S}$ has branch parents $\left(\textnormal{BP}(\iota_{\textnormal{cfg}}(M))\cap G_{S}\right)\cup\{\tilde{B}\}$ . Since $\iota_{\textnormal{cfg}}(B_{j})=\tilde{B}$ and by induction assumption $\textnormal{BP}_{\textnormal{cfg}}(M)\cap G_{S}=\textnormal{BP}(\iota_{\textnormal{cfg}}(M))\cap G_{S}$ , we get
| | $\displaystyle\textnormal{BP}_{\textnormal{cfg}}(M)$ | $\displaystyle=\left\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{BP}(M)\cap H_{i}\right\}\cup\{\iota_{\textnormal{cfg}}(B_{1}),\dots,\iota_{\textnormal{cfg}}(B_{i})\}$ | |
| --- | --- | --- | --- |
∎
Statement. Let $G$ be the CFG and $H$ the unrolled CFG of program $S$ . For each node $M\in H$ the following equation holds.
$$
\textnormal{prov}(M,x)\subseteq\textnormal{prov}(\iota_{\textnormal{cfg}}(M),x) \tag{17}
$$
* Proof*
Follows directly from the two equations $\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{RD}(M,x)\}\subseteq\textnormal{RD}(\iota_{\textnormal{cfg}}(M),x)$ and $\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{BP}(M)\}=\textnormal{BP}(\iota_{\textnormal{cfg}}(M))$ , since $\textnormal{prov}(M,x)$ is defined in terms of RD and BP. ∎
### B.5. Proof of Proposition 4
Statement. Let $H$ be the unrolled CFG of a program $S$ . For each node $M$ and variable $x$ , there exists an evaluation function
$$
V^{M}_{x}\in[\mathcal{T}|_{\textnormal{prov}(M,x)}\to\mathcal{V}],
$$
such that for all traces $\mathtt{tr}$ , initial program state $\sigma_{0}$ as in Definition 1, and execution sequence
$$
(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},M_{i})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{l},\text{END})
$$
we have
$$
\sigma_{i}(x)=V^{M_{i}}_{x}(\mathtt{tr}).
$$
* Proof*
First, we have to justify the use of mathematical induction to prove properties on a potentially infinite graph. For $M_{1},M_{2}\in H$ define the relation $M_{1}\prec M_{2}\Leftrightarrow M_{1}\text{ is parent of }M_{2}$ (i.e. there is an edge from $M_{1}$ to $M_{2}$ in $H$ ). By construction of $H$ , there are no infinite descending chains, $M_{i}\in H$ for $i\in\mathbb{N}$ such that $M_{i+1}\prec M_{i}$ . This makes $\prec$ a well-founded relation, i.e. every non-empty subset has a minimal element. As a result, we may apply induction with respect to this relation (as has been done in the proof of Proposition 9) for graphs with infinite nodes. This proof principle is called well-founded or Noetherian induction. To complete the proof, we only need to consider one additional case: Case 3. Let $J$ be a join node of a while loop with the parents $B_{i}=\textnormal{Branch}(E)$ , $i\in\mathbb{N}$ . The function $V^{B_{i}}_{x}\in[\mathcal{T}|_{\textnormal{prov}(B_{i},x)}\to\mathcal{V}]$ exists by induction assumption and computes the value of $x$ before executing the while loop body for the $i$ -th time. If there is a reaching definition $M^{\prime}\in\textnormal{RD}(J,x)$ on a path $(B_{i},\dots,M^{\prime},\dots,J)$ , define
$$
V^{J}_{x}(\mathtt{tr})\coloneqq\begin{cases}V^{B_{i}}_{x}(\mathtt{tr})&\text{if }\exists i\in\mathbb{N}\colon\forall j<i\colon V^{B_{j}}_{E}(\mathtt{tr})=\mathtt{true}\land V^{B_{i}}_{E}(\mathtt{tr})=\mathtt{false},\\
\mathtt{null}&\text{otherwise.}\end{cases}
$$
Further, as $M^{\prime}$ belongs to the sub-CFG of the while loop body, we have that for every $B_{i}$ there is a $M_{i}^{\prime}\in\textnormal{RD}(J,x)$ on the path from $B_{i}$ to $J$ . Since $B_{i}\in\textnormal{BP}(M_{i}^{\prime})$ , by Equation 14 $\textnormal{prov}(B_{i},E)\subseteq\textnormal{prov}(J,x)$ for all $i$ and thus $V^{J}_{x}\in[\mathcal{T}|_{\textnormal{prov}(J,x)}\to\mathcal{V}]$ . If there is no reaching definition in the while loop body sub-CFG, then $\textnormal{prov}(J,x)=\textnormal{prov}(B_{1},x)$ and define $V^{J}_{x}=V^{B_{1}}_{x}$ . ∎
### B.6. Proof of Theorem 5
Statement. Let $G$ be the CFG for a program $S$ . Let $N_{1},\dots,N_{K}$ be all sample nodes in $G$ . For each sample node $$ , let
$$
A_{k}=\textnormal{addresses}(N_{k})\cup\textstyle\bigcup_{i=0}^{n_{k}}\textnormal{prov}(N_{k},E_{i}^{k})\cup\textstyle\bigcup_{N^{\prime}\in\textnormal{BP}(N_{k})}\textnormal{prov}(N^{\prime},{\textnormal{condexp}(N^{\prime})}).
$$
Then, there exist functions $p_{k}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}]$ such that for all $\mathtt{tr}\in\mathcal{T}$ , if $p_{S}(\mathtt{tr})\neq\textnormal{undefined}$ , then
$$
p_{S}(\mathtt{tr})=p_{G}(\mathtt{tr})=p_{H}(\mathtt{tr})=\prod_{k=1}^{K}p_{k}(\mathtt{tr}).
$$
* Proof*
Let $H$ be the unrolled CFG of program $S$ . Denote the (countably many) sample nodes in $H$ with $$ . Like in the proof of Theorem 10, define for each $M_{j}$ , $b_{j}(\mathtt{tr})\coloneqq\bigwedge_{M^{\prime}\in\textnormal{BP}(M_{j})}t^{j}_{M^{\prime}}(V^{M^{\prime}}_{{\textnormal{condexp}(M^{\prime})}}(\mathtt{tr}))$ where
$$
b_{j}\in[\mathcal{T}|_{\textstyle\bigcup_{M^{\prime}\in\textnormal{BP}(M_{j})}\textnormal{prov}(M^{\prime},{\textnormal{condexp}(M^{\prime})})}\to\{\mathtt{true},\mathtt{false}\}].
$$
Again, $b_{j}(\mathtt{tr})=\mathtt{true}$ if $M_{j}$ is in the execution sequence for $\mathtt{tr}$ else $\mathtt{false}$ . Define
$$
\tilde{p}_{j}(\mathtt{tr})\coloneqq\delta_{b_{j}(\mathtt{tr})}\textnormal{pdf}_{f^{j}}\left(\mathtt{tr}(V^{M_{j}}_{E_{0}^{j}}(\mathtt{tr}));V^{M_{j}}_{E_{1}^{j}}(\mathtt{tr}),\dots,V^{M_{j}}_{E_{n_{j}}^{j}}(\mathtt{tr})\right)+(1-\delta_{b_{j}(\mathtt{tr})}).
$$
We have $\tilde{p}_{j}\in[\mathcal{T}|_{\tilde{A}_{j}}\to\mathbb{R}_{\geq 0}]$ , for
$$
\tilde{A}_{j}=\textnormal{addresses}(M_{j})\cup\textstyle\bigcup_{i=0}^{n_{j}}\textnormal{prov}(M_{j},E_{i}^{j})\cup\textstyle\bigcup_{M^{\prime}\in\textnormal{BP}(M_{j})}\textnormal{prov}(M^{\prime},{\textnormal{condexp}(M^{\prime})}).
$$
Finally, we group the nodes $M_{j}$ by their corresponding CFG node.
$$
p_{k}=\prod_{j\colon\iota_{\textnormal{cfg}}(M_{j})=N_{k}}\tilde{p}_{j}
$$
If $\iota_{\textnormal{cfg}}(M_{j})=N_{k}$ , then $\tilde{A}_{j}\subseteq A_{k}$ , since for $i=0,\dots,n$ we have $E_{i}^{k}=E_{i}^{j}$ and by Eq. 8
$$
\textnormal{prov}(M_{j},E_{i}^{j})\subseteq\textnormal{prov}(\iota_{\textnormal{cfg}}(M_{j}),E_{i}^{j})=\textnormal{prov}(N_{k},E_{i}^{k})
$$
and by Eq. 7 it holds that
$$
\{\iota_{\textnormal{cfg}}(M^{\prime})\colon M^{\prime}\in\textnormal{BP}(M_{j})\}=\textnormal{BP}(\iota_{\textnormal{cfg}}(M_{j}))=\textnormal{BP}(N_{k})
$$
such that
| | $\displaystyle\textstyle\bigcup_{M^{\prime}\in\textnormal{BP}(M_{j})}\textnormal{prov}(M^{\prime},{\textnormal{condexp}(M^{\prime})})$ | $\displaystyle\subseteq\textstyle\bigcup_{M^{\prime}\in\textnormal{BP}(M_{j})}\textnormal{prov}(\iota_{\textnormal{cfg}}(M^{\prime}),{\textnormal{condexp}(\iota_{\textnormal{cfg}}(M^{\prime}))})$ | |
| --- | --- | --- | --- |
Thus, for all $j$ , $\iota_{\textnormal{cfg}}(M_{j})=N_{k}$ , we have $\tilde{p}_{j}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}]$ which implies $p_{k}\in[\mathcal{T}|_{A_{k}}\to\mathbb{R}_{\geq 0}].$ Again, we know that for the end-state $\sigma_{l}(\textbf{p})=V^{\text{END}}_{\textbf{p}}(\mathtt{tr})=p_{H}(\mathtt{tr})$ and since $b_{j}(\mathtt{tr})=\mathtt{true}$ if and only if $M_{j}$ is in the execution sequence for $\mathtt{tr}$ , we have $p_{H}(\mathtt{tr})=\prod_{k=1}^{K}p_{k}(\mathtt{tr})$ . ∎
## Appendix C Towards a Measure-theoretic Interpretation of the Operational Semantics
In this section, we will briefly discuss how one may construct a measure space on traces such that the function $\mathtt{tr}\mapsto p_{S}(\mathtt{tr})$ is indeed a Radon-Nikodym derivative of a measure on this space. This construction is related to denotational semantics based on trace types (Lew et al., 2019, 2023). We first define a measure space for each value type:
| | $\displaystyle\tau$ | $\displaystyle:\coloneqq\{\mathtt{null}\},\mathbb{Z},\mathbb{R},\mathbb{R}^{2},\dots$ | |
| --- | --- | --- | --- |
These measure spaces model the support of common distributions, but could also be extended by building sum and product spaces. They are comprised of the typical Dirac measure, power sets, counting measure, Borel sets, and Lebesgue measures.
Each trace $\mathtt{tr}$ can be assigned an unique type function $\tau_{\mathtt{tr}}\colon\mathbf{Strings}\to\mathbf{Types}$ such that for all $\alpha\in\mathbf{Strings}$ we have $\mathtt{tr}(\alpha)\in\tau_{\mathtt{tr}}(\alpha)$ . The types are assumed to be disjoint (e.g. $\mathbb{Z}\cap\mathbb{R}=\emptyset$ ). Let
$$
\mathcal{S}_{<\infty}=\{s\colon\mathbf{Strings}\to\mathbf{Types}\colon|\{\alpha\in\mathbf{Strings}\colon s(\alpha)\neq\{\mathtt{null}\}\}|<\infty\}
$$
be the set of all type functions that correspond to traces with a finite number of non- $\mathtt{null}$ values. We enumerate the addresses, $\mathbf{Strings}=\{\alpha_{i}\colon i\in\mathbb{N}\}$ , and define a measureable space for each type function, $s\colon\mathbf{Strings}\to\mathbf{Types}$ , $\mathscr{M}_{s}=(M_{s},\Sigma_{s})=\bigotimes_{i\in\mathbb{N}\colon s(\alpha_{i})\neq\{\mathtt{null}\}}\mathcal{M}_{s(\alpha_{i})}$ . If $s\in\mathcal{S}_{<\infty}$ , then $\mathscr{M}_{s}$ is a finite dimensional product space with product measure $\nu_{s}$ . For the set of traces $\mathcal{T}$ , we define the $\sigma$ -algebra $\Sigma_{\mathcal{T}}$ with $A\in\Sigma_{\mathcal{T}}\Leftrightarrow\forall s\colon\mathbf{Strings}\to\mathbf{Types}\colon\pi_{s}(\{\mathtt{tr}\in A\colon\tau_{\mathtt{tr}}=s\})\in\Sigma_{s},$ where $\pi_{s}\colon\mathcal{T}\to M_{s}$ is the canonical projection. The reference measure on $(\mathcal{T},\Sigma_{\mathcal{T}})$ is
$$
\nu(A)=\sum_{s\in\mathcal{S}_{<\infty}}\nu_{s}(\pi_{s}(\{\mathtt{tr}\in A\colon\tau_{\mathtt{tr}}=s\}))
$$
which effectively is a measure of traces with a finite number of non- $\mathtt{null}$ values.
If a primitive distribution $f$ with $\text{support}(f)\subseteq\tau_{f}$ and arguments $v_{1}\dots,v_{n}$ corresponds to the measure $\mu_{f,v_{1},\dots,v_{n}}$ with Radon-Nikodym derivative ${\mathtt{d}\mu_{f,v_{1},\dots,v_{n}}}/{\mathtt{d}\nu_{\tau_{f}}}$ , we define
$$
\textnormal{pdf}_{f}(v;v_{1},\dots,v_{n})=\begin{cases}(\mathtt{d}\mu_{f,v_{1},\dots,v_{n}}/\mathtt{d}\nu_{\tau_{f}})(v)&{\text{if }v\in\tau_{f}}\\
0&\text{otherwise}.\end{cases}
$$
The measure-theoretic interpretation of a program is the measure $\mu_{S}(A)=\int_{\mathcal{T}_{\textnormal{valid}}\cap A}p_{S}\,\mathtt{d}\nu$ , where
$$
\mathcal{T}_{\textnormal{valid}}\coloneqq\{\mathtt{tr}\colon p_{S}(\mathtt{tr})\neq\textnormal{undefined}\land\forall\alpha\colon\mathtt{tr}(\alpha)\neq\mathtt{null}\Rightarrow p_{S}(\mathtt{tr}[\alpha\mapsto\mathtt{null}])=\textnormal{undefined}\}
$$
is the set of all traces with well-defined density such that changing a value at any address to $\mathtt{null}$ leads to an undefined density. That is, for $\mathtt{tr}\in\mathcal{T}_{\textnormal{valid}}$ all addresses that are not used during the execution of the program are set to $\mathtt{null}$ and all address that are used are set to non- $\mathtt{null}$ values. Such a trace necessarily has a finite number of non- $\mathtt{null}$ values as the density for non-termination is undefined which is the only possibility for executing an infinite number of sample statements. This condition is important, because the countably infinite sum in definition of $\nu$ has better convergence properties on $\mathcal{T}_{\textnormal{valid}}$ . Finally, $p_{S}$ the Radon-Nikodym derivative of $\mu_{S}$ with respect to $\nu$ on $\mathcal{T}_{\textnormal{valid}}$ .
We emphasize that this interpretation demands a careful analysis of the measurability of $\mathcal{T}_{\textnormal{valid}}$ and $p_{S}$ which is beyond the scope of this work. This requires additional assumptions about the program, at the very least that the primitives $g$ are measurable. Such measurability analysis may be done along the lines of Borgström et al. (2016) and Lee et al. (2019).
Note that this construction can handle programs where random variables are of mixed-type like the variable $\mathtt{y}$ in the example below:
⬇
x = sample ("x", Bernoulli (p))
if x == 1 then
y = sample ("y", Bernoulli (0.5))
else
y = sample ("y", Normal (0.,1.))
We list the density according to the semantics for different example trace of different type:
| | $\displaystyle p(\{x\mapsto 1\colon\mathbb{Z},y\mapsto 1\colon\mathbb{Z}\})$ | $\displaystyle=\textnormal{pdf}_{\textnormal{Bernoulli}}(1;0.5)\cdot\textnormal{pdf}_{\textnormal{Bernoulli}}(1;0.5)=0.5\cdot 0.5$ | |
| --- | --- | --- | --- |
### C.1. Remark on Conditioning
We have defined density semantics such that $p_{S}$ denotes the joint probability distribution over all variables in the model in the sense described above. In our construction, we do not differentiate between latent and observed variables. To incorporate observed data, we can define the trace $\mathtt{obs\_tr}$ , where addresses are mapped to the observed data points. All addresses that do not correspond to observed data map to $\mathtt{null}$ . Loosely, the function $\mathtt{tr}\mapsto p_{S}(\mathtt{tr}\oplus\mathtt{obs\_tr})$ then corresponds to the unnormalised posterior density, where we merge the trace $\mathtt{tr}$ , encapsulating latent variables, with the observed trace $\mathtt{obs\_tr}$ like below
$$
(A\oplus B)(\alpha)=\begin{cases}B(\alpha)&\text{if}\,B(\alpha)\neq\mathtt{null},\\
A(\alpha)&\text{otherwise.}\end{cases}
$$
This is only a loose correspondence, because it is not clear whether this function can be normalized by integrating over all observed variables. It is beyond the scope of this work to precisely define conditioning semantics. For work discussing similar issues, see Lee et al. (2019).
## Appendix D Proofs of Section 5
### D.1. Sliced CFG Construction
First, we formally define the CFG slicing with respect to the factorisation of Theorem 5. Here, we use provnode instead of prov to make the dependencies between CFG nodes explicit (see Section 3.2).
** Definition 0**
*Let $G=(N_{\textnormal{start}},N_{\textnormal{end}},\mathcal{N},\mathcal{E})$ be a CFG with $K$ sample nodes, which we enumerate with $$ for $j=1,\dots,K$ . For each $k\in\{1,\dots,K\}$ , we define the set of indices of sample nodes that the factor $p_{k}$ depends on:
$$
\mathcal{J}_{k}\coloneqq\{j\in\{1,\dots,K\}\colon N_{k}\in\textstyle\bigcup_{i=0}^{n_{j}}\textnormal{provnode}(N_{j},E^{j}_{i})\cup\textstyle\bigcup_{N^{\prime}\in\textnormal{BP}(N_{j})}\textnormal{provnode}(N^{\prime},\textnormal{condexp}(N^{\prime}))\}.
$$
Next, we define the set of nodes that lie on path from $N_{k}$ to some of its dependent node $N_{j}$ :
$$
\mathcal{N}^{\prime}_{k}\coloneqq\{N\in\mathcal{N}\colon\exists j\in\mathcal{J}_{k}\colon\exists\text{ path }\nu=(N_{k},\dots,N_{j})\colon N\in\nu\text{ and }N_{k}\text{ only appears at the start of }\nu\}.
$$
We transform all sample nodes that are in $\mathcal{N}_{k}^{\prime}$ , but do not depend on $N_{k}$ to a read statement, which in contrast to sample statements do not contribute to the density: $\mathcal{N}_{k}\coloneqq\{\psi(N)\colon N\in\mathcal{N}_{k}^{\prime}\}$ , where
The semantic of read statements is given below. Note that we have to keep all $E_{i}$ in the statement to check their values against $\mathtt{null}$ like in Equation 1. We omit this technicality in the main text.
We restrict the set of edges to the subset of nodes $\mathcal{N}_{k}$ :
$$
\mathcal{E}_{k}^{\prime}\coloneqq\{(\psi(e_{1}),\psi(e_{2}))\colon(e_{1},e_{2})\in\mathcal{E}\land e_{1}\in\mathcal{N}_{k}^{\prime}\land e_{2}\in\mathcal{N}_{k}^{\prime}\}.
$$
We connect the new start node $N^{k}_{\textnormal{start}}$ to $N_{k}$ and the new end node $N^{k}_{\textnormal{end}}$ to all $N_{j}$ , $j\in\mathcal{J}_{k}$ , that do not have a successor in $\mathcal{E}_{k}^{\prime}$ :
$$
\mathcal{E}_{k}=\mathcal{E}_{k}^{\prime}\cup\{(N^{k}_{\textnormal{start}},N_{k})\}\cup\{(N_{j},N^{k}_{\textnormal{end}})\colon j\in\mathcal{J}_{k}\land\nexists N\in\mathcal{N}_{k}\colon(N_{j},N)\in\mathcal{E}_{k}^{\prime}\}.
$$
Finally, define the CFG sliced with respect to $N_{k}$ as
$$
G_{k}\coloneqq(N^{k}_{\textnormal{start}},N^{k}_{\textnormal{end}},\mathcal{N}_{k},\mathcal{E}_{k}).
$$*
Note that in this construction, we allow that the end node $N^{k}_{\textnormal{end}}$ has multiple predecessors. This does not change the CFG semantics. Next, we rewrite Lemma 3 and Lemma 1 in terms of provnode and prove two technical lemmas needed to establish the correctness result in the next section.
** Lemma 0**
*Let $M$ be a CFG node and $x$ a variable. provnode has following properties:
- If $M^{\prime}\in\textnormal{RD}(M,x)$ is an assignment node, $M^{\prime}=\textnormal{Assign}(x=E)$ , then
$$
\displaystyle\textnormal{provnode}(M^{\prime},E)=\textstyle\bigcup_{y\in\textnormal{vars}(E)}\textnormal{provnode}(M^{\prime},y)\subseteq\textnormal{provnode}(M,x). \tag{19}
$$
- if $M^{\prime}\in\textnormal{RD}(M,x)$ is a sample node, $$ , then
$$
\displaystyle\textnormal{provnode}(M^{\prime},E_{0})\subseteq\textnormal{provnode}(M,x)\quad\text{and}\quad M^{\prime}\in\textnormal{provnode}(M,x). \tag{20}
$$
- For all $M^{\prime}\in\textnormal{RD}(M,x)$ it holds that for all branch parents $N_{\text{bp}}=\textnormal{Branch}(E_{M_{\text{bp}}})\in\textnormal{BP}(M^{\prime})$
$$
\displaystyle\textnormal{provnode}(M_{\text{bp}},E_{N_{\text{bp}}})\subseteq\textnormal{provnode}(M,x). \tag{21}
$$
- We have following relationship between provnode on CFG $G$ and on unrolled CFG $H$ :
$$
\textnormal{provnode}(M,x)\subseteq\textnormal{provnode}(\iota_{\textnormal{cfg}}(M),x). \tag{22}
$$*
** Lemma 0**
*Let $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ be traces that only differ at address $\alpha$ , i.e. $\mathtt{tr}_{1}(\alpha)\neq\mathtt{tr}_{2}(\alpha)$ and $\forall\beta\neq\alpha\colon\mathtt{tr}_{1}(\beta)=\mathtt{tr}_{2}(\beta).$ Further, let $M_{\alpha}$ bet the only sample node in the execution sequences of $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ whose address expression evaluates to $\alpha$ . If CFG node $M$ appears in both execution sequences and variable $x$ ,
| | $\displaystyle(\sigma_{0},\text{START})\overset{\mathtt{tr}_{1}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{1}}{\longrightarrow}(\sigma_{1},M)\overset{\mathtt{tr}_{1}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{1}}{\longrightarrow}(\sigma_{l_{1}},\text{END}),$ | |
| --- | --- | --- |
then the inequality $\sigma_{1}(x)=V^{M}_{x}(\mathtt{tr}_{1})\neq V^{M}_{x}(\mathtt{tr}_{2})=\sigma_{2}(x)$ implies $M_{\alpha}\in\textnormal{provnode}(M,x)$ . Or equivalently, $M_{\alpha}\notin\textnormal{provnode}(M,x)$ implies $\sigma_{1}(x)=V^{M}_{x}(\mathtt{tr}_{1})=V^{M}_{x}(\mathtt{tr}_{2})=\sigma_{2}(x)$ .*
* Proof*
By induction on the position in the execution sequence. The claim is trivially true for the start node. Let $M$ be a node in both execution sequences with $V^{M}_{x}(\mathtt{tr}_{1})\neq V^{M}_{x}(\mathtt{tr}_{2})$ . The induction assumption states that for all nodes $M^{\prime}$ that appear sooner than $M$ in any of the execution sequences, the claim holds. Let $M^{\prime}_{1}\in\textnormal{RD}(M,x)\neq\emptyset$ be the assign node that last writes $x$ in the execution sequence of $\mathtt{tr}_{1}$ before evaluating $M$ . Similarly, let $M^{\prime}_{2}\in\textnormal{RD}(M,x)\neq\emptyset$ be the corresponding assign node in the execution sequences of $\mathtt{tr}_{2}$ .
- Case 1. $M^{\prime}_{1}\neq M^{\prime}_{2}$ : By definition of reaching definitions, both execution sequences must contain a different path from start node to $M$ . This can only happen if there exists one branch parent $B\in\textnormal{BP}(M^{\prime}_{1})\cap\textnormal{BP}(M^{\prime}_{2})$ in both execution sequences that evaluates differently, $V^{B}_{E}(\mathtt{tr}_{1})\neq V^{B}_{E}(\mathtt{tr}_{2})$ for $E=\textnormal{condexp}(B)$ . By induction assumption, $M_{\alpha}\in\textnormal{provnode}(B,E)$ and Equation 21 implies $M_{\alpha}\in\textnormal{provnode}(M,x)$ .
- Case 2. $M^{\prime}\coloneqq M^{\prime}_{1}=M^{\prime}_{2}=\textnormal{Assign}(x=E)$ : It holds that $V^{M^{\prime}}_{E}(\mathtt{tr}_{1})=V^{M}_{x}(\mathtt{tr}_{1})\neq V^{M}_{x}(\mathtt{tr}_{2})=V^{M^{\prime}}_{E}(\mathtt{tr}_{2})$ . By induction assumption, we have $M_{\alpha}\in\textnormal{provnode}(M^{\prime},E)$ and Equation 19 implies $M_{\alpha}\in\textnormal{provnode}(M,x)$ .
- Case 3. $$ : It holds that $\mathtt{tr}_{1}(V^{M^{\prime}}_{E_{0}}(\mathtt{tr}_{1}))=V^{M}_{x}(\mathtt{tr}_{1})\neq V^{M}_{x}(\mathtt{tr}_{2})=\mathtt{tr}_{2}(V^{M^{\prime}}_{E_{0}}(\mathtt{tr}_{2}))$ . If $V^{M^{\prime}}_{E_{0}}(\mathtt{tr}_{1})=\alpha$ or $V^{M^{\prime}}_{E_{0}}(\mathtt{tr}_{2})=\alpha$ , then $M^{\prime}=M_{\alpha}$ , since $M_{\alpha}$ is the only sample node whose address expression evaluates to $\alpha$ and we have $M_{\alpha}\in\textnormal{provnode}(M,x)$ by Equation 20. Otherwise, since the traces only differ at $\alpha$ , the inequality can only hold if $V^{M^{\prime}}_{E_{0}}(\mathtt{tr}_{1})\neq V^{M^{\prime}}_{E_{0}}(\mathtt{tr}_{2})$ . But then as in Case 2, by induction assumption $M_{\alpha}\in\textnormal{provnode}(M^{\prime},E_{0})$ and by Equation 20 we have $M_{\alpha}\in\textnormal{provnode}(M,x)$ .
Lastly, if there are no such $M^{\prime}_{1}$ and $M^{\prime}_{2}$ in both sequences, then $V^{M}_{x}(\mathtt{tr}_{1})=\mathtt{null}=V^{M}_{x}(\mathtt{tr}_{2})$ , a contradiction. If there is only $M^{\prime}_{1}$ or only $M^{\prime}_{2}$ , then the claim follows as in Case 1. ∎
** Lemma 0**
*Let $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ be traces that only differ at address $\alpha$ , i.e. $\mathtt{tr}_{1}(\alpha)\neq\mathtt{tr}_{2}(\alpha)$ and $\forall\beta\neq\alpha\colon\mathtt{tr}_{1}(\beta)=\mathtt{tr}_{2}(\beta).$ Further, let $M_{\alpha}$ be the only sample node in the execution sequences whose address expression evaluates to $\alpha$ . If CFG node $M$ is in one but not both of the execution sequences of $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ , then there exists a branch parent $B\in\textnormal{BP}(M)$ such that $M_{\alpha}\in\textnormal{provnode}(B,\textnormal{condexp}(B))$ .*
* Proof*
As in the proof of Theorem 5, $b(\mathtt{tr})=\bigwedge_{B\in\textnormal{BP}(M)}t_{B}(V^{B}_{\textnormal{condexp}(B)}(\mathtt{tr}))$ is $\mathtt{true}$ if $M$ is in the execution sequence of $\mathtt{tr}$ else $\mathtt{false}$ . Since $M$ is not in both execution sequences we have $b(\mathtt{tr}_{1})\neq b(\mathtt{tr}_{2})$ . Thus, one of the branch parents has to evaluate differently, i.e. there is a branch parent $B\in\textnormal{BP}(M)$ in both execution sequences such that $V^{B}_{\textnormal{condexp}(B)}(\mathtt{tr}_{1})\neq V^{B}_{\textnormal{condexp}(B)}(\mathtt{tr}_{2})$ . Since, $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ differ only at $\alpha$ and $M_{\alpha}$ is the only sample node in the execution sequences whose address expression evaluates to $\alpha$ , by Lemma 3, $M_{\alpha}\in\textnormal{provnode}(B,\textnormal{condexp}(B))$ . ∎
### D.2. Proof of Theorem 1 - Correctness of Slicing
Now, we are ready to prove the main correctness result of the sliced CFG construction.
Statement. Let $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ be traces that only differ at address $\alpha$ , i.e. $\mathtt{tr}_{1}(\alpha)\neq\mathtt{tr}_{2}(\alpha)$ and $\forall\beta\neq\alpha\colon\mathtt{tr}_{1}(\beta)=\mathtt{tr}_{2}(\beta).$ Let the execution sequences in the unrolled CFG $H$ be equal up to sample node $$ and state $\sigma$ , such that $\alpha=\sigma(E_{0})$ :
$$
\displaystyle(\sigma_{0},\text{START})\overset{\mathtt{tr}_{1}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{1}}{\longrightarrow}(\sigma,M_{\alpha})\overset{\mathtt{tr}_{1}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{1}}{\longrightarrow}(\sigma_{l_{1}},\text{END}), \displaystyle(\sigma_{0},\text{START})\overset{\mathtt{tr}_{2}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{2}}{\longrightarrow}(\sigma,M_{\alpha})\overset{\mathtt{tr}_{2}}{\longrightarrow}\cdots\overset{\mathtt{tr}_{2}}{\longrightarrow}(\sigma_{l_{2}},\text{END}). \tag{23}
$$
If $M_{\alpha}$ is the only sample node in the execution sequences whose address expression evaluates to $\alpha$ , then for the sliced CFG $G_{k}$ of sample node $N_{k}=\iota_{\textnormal{cfg}}(M_{\alpha})$ , it holds that
$$
\log p_{G}(\mathtt{tr}_{1})-\log p_{G}(\mathtt{tr}_{2})=\log\bar{p}_{G_{k}}(\mathtt{tr}_{1},\sigma)-\log\bar{p}_{G_{k}}(\mathtt{tr}_{2},\sigma).
$$
* Proof*
Let $M_{1}^{\prime}$ and $M_{2}^{\prime}$ be the last sample nodes in the sequences, such that $\iota_{\textnormal{cfg}}(M_{1}^{\prime})\in G_{k}$ and $\iota_{\textnormal{cfg}}(M_{2}^{\prime})\in G_{k}$ . By definition of $G_{k}$ , the execution sequences for $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ in the unrolled version $H_{k}$ of $G_{k}$ become
$$
(\sigma,\text{START})\underset{H_{k}}{\overset{\mathtt{tr}_{1}}{\longrightarrow}}(\sigma,M_{\alpha})\underset{H_{k}}{\overset{\mathtt{tr}_{1}}{\longrightarrow}}\cdots\underset{H_{k}}{\overset{\mathtt{tr}_{1}}{\longrightarrow}}(\sigma^{\prime}_{1},M^{\prime}_{1})\underset{H_{k}}{\overset{\mathtt{tr}_{1}}{\longrightarrow}}\cdots\underset{H_{k}}{\overset{\mathtt{tr}_{1}}{\longrightarrow}}(\sigma_{1}^{\prime\prime},\text{END}),
$$
$$
(\sigma,\text{START})\underset{H_{k}}{\overset{\mathtt{tr}_{2}}{\longrightarrow}}(\sigma,M_{\alpha})\underset{H_{k}}{\overset{\mathtt{tr}_{2}}{\longrightarrow}}\cdots\underset{H_{k}}{\overset{\mathtt{tr}_{2}}{\longrightarrow}}(\sigma^{\prime}_{2},M^{\prime}_{2})\underset{H_{k}}{\overset{\mathtt{tr}_{2}}{\longrightarrow}}\cdots\underset{H_{k}}{\overset{\mathtt{tr}_{2}}{\longrightarrow}}(\sigma_{2}^{\prime\prime},\text{END}),
$$
for some states $\sigma^{\prime}_{1}$ , $\sigma^{\prime}_{2},\sigma^{\prime\prime}_{1}$ , $\sigma^{\prime\prime}_{2}$ . Note that technically we also have $(\sigma^{\prime}_{i},M^{\prime}_{i})\underset{H_{k}}{\overset{\mathtt{tr}_{i}}{\longrightarrow}}(\sigma_{i}^{\prime},\text{END})$ . To prove the statement, we have to show that the contribution to the density of sample nodes $M$ that come after $M_{1}^{\prime}$ and $M_{2}^{\prime}$ in the original execution sequences (23) or (24) and sample nodes $M$ that come between $M_{\alpha}$ and $M_{1}^{\prime}$ or $M_{2}^{\prime}$ but were transformed to read statements in $G_{k}$ , see (18), is equal. By Theorem 5, the contribution to the density of sample node $M$ with $N_{j}=\iota_{\textnormal{cfg}}(M)$ , i.e. $$ , has provenance set
| | $\displaystyle\tilde{A}_{j}$ | $\displaystyle\coloneqq\textnormal{addresses}(M)\cup\textstyle\bigcup_{i=0}^{n_{j}}\textnormal{prov}(M,E_{i}^{j})\cup\textstyle\bigcup_{M_{\textnormal{bp}}\in\textnormal{BP}(M)}\textnormal{prov}(M_{\textnormal{bp}},\textnormal{condexp}(M_{\textnormal{bp}}))$ | |
| --- | --- | --- | --- |
or equivalently expressed in terms of sample nodes
| | $\displaystyle\tilde{\mathcal{A}}_{j}$ | $\displaystyle\coloneqq\{M\}\cup\textstyle\bigcup_{i=0}^{n_{j}}\textnormal{provnode}(M,E_{i}^{j})\cup\textstyle\bigcup_{M_{\textnormal{bp}}\in\textnormal{BP}(M)}\textnormal{provnode}(M_{\textnormal{bp}},\textnormal{condexp}(M_{\textnormal{bp}}))$ | |
| --- | --- | --- | --- |
such that by Lemma 2
| | $\displaystyle\{\iota_{\textnormal{cfg}}(M^{\prime})\colon$ | $\displaystyle M^{\prime}\in\tilde{\mathcal{A}}_{j}\}\subseteq$ | |
| --- | --- | --- | --- | If $M$ comes after $M^{\prime}_{1}$ or $M^{\prime}_{2}$ in (23) or (24), then $\iota_{\textnormal{cfg}}(M)=N_{j}\notin G_{k}$ , and by definition of $G_{k}$ , we have $\iota_{\textnormal{cfg}}(M_{\alpha})=N_{k}\notin\mathcal{A}_{j}$ and thus also $M_{\alpha}\notin\tilde{\mathcal{A}}_{j}$ . If $M$ comes between $M_{\alpha}$ and $M^{\prime}_{1}$ or $M^{\prime}_{2}$ , but was transformed to a read statement in $G_{k}$ , then by definition of $G_{k}$ , also $N_{k}\notin\mathcal{A}_{j}$ and $M_{\alpha}\notin\tilde{\mathcal{A}}_{j}$ . In both cases, by Lemma 4, $M$ has to be in both original execution sequences, since otherwise we would have the contradiction $M_{\alpha}\in\textstyle\bigcup_{B\in\textnormal{BP}(M)}\textnormal{provnode}(B,\textnormal{condexp}(B))$ . Let $(\sigma_{1},M)$ denote the appearance in (23) and $(\sigma_{2},M)$ the appearance in (24). Since $M_{\alpha}\notin\textstyle\bigcup_{i=0}^{n_{j}}\textnormal{provnode}(M,E_{i}^{j})$ , by Lemma 3, we have $\sigma_{1}(y)=\sigma_{2}(y)$ for all variables $y\in\textstyle\bigcup_{i=0}^{n_{j}}\textnormal{vars}(E_{i}^{j})$ . Since it also holds that $\alpha\neq\sigma_{1}(E_{0})=\sigma_{2}(E_{0})$ , we have $\mathtt{tr}_{1}(\sigma_{1}(E_{0}))=\mathtt{tr}_{2}(\sigma_{2}(E_{0}))$ , which means that $M$ contributes the same value to the density in both execution sequences, compare Equation 2. ∎
### D.3. Proof of Corollary 2 - Correctness of Slicing (cont.)
Statement. Assume that for each trace $\mathtt{tr}$ there is at most one sample node $M_{\alpha}$ in its execution sequences such that the address expression of $M_{\alpha}$ evaluates to $\alpha$ . For initial program state $\sigma_{0}$ as in Definition 1, define
$$
p_{\alpha}(\mathtt{tr})\coloneqq\begin{cases}\bar{p}_{G_{k}}(\mathtt{tr},\sigma)&\text{ if }\exists\,\sigma\in\Sigma,M_{\alpha}\colon(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma,M_{\alpha})\land\iota_{\textnormal{cfg}}(M_{\alpha})=N_{k}\\
1&\text{ otherwise.}\end{cases}
$$
Then, $\Delta_{\alpha}(\mathtt{tr})\coloneqq\log p_{G}(\mathtt{tr})-\log p_{\alpha}(\mathtt{tr})$ is independent of address $\alpha$ , $\Delta_{\alpha}\in[\mathcal{T}|_{\mathbf{Strings}\setminus\{\alpha\}}\to\mathbb{R}_{\geq 0}].$
* Proof*
By definition $\Delta_{\alpha}\in[\mathcal{T}|_{\mathbf{Strings}\setminus\{\alpha\}}\to\mathbb{R}_{\geq 0}]$ , if for two traces $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ it holds that
$$
\forall\beta\in\mathbf{Strings}\setminus\{\alpha\}\colon\mathtt{tr}_{1}(\beta)=\mathtt{tr}_{2}(\beta)\implies\Delta_{\alpha}(\mathtt{tr}_{1})=\Delta_{\alpha}(\mathtt{tr}_{2}).
$$
Let $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ be traces such that $\mathtt{tr}_{1}(\alpha)\neq\mathtt{tr}_{2}(\alpha)$ and $\forall\beta\neq\alpha\colon\mathtt{tr}_{1}(\beta)=\mathtt{tr}_{2}(\beta).$ The execution sequences of $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ are equal up to $(\sigma,M_{\alpha})$ , where $M_{\alpha}$ is the first sample node whose address expression evaluates to $\alpha$ . If there is no such sample node, then the execution sequences are completely identical. In this case, $\log p_{G}(\mathtt{tr}_{1})=\log p_{G}(\mathtt{tr}_{2})$ and $\log p_{\alpha}(\mathtt{tr}_{1})=\log p_{\alpha}(\mathtt{tr}_{2})=0$ . If there is such a sample node $M_{\alpha}$ , by assumption it is the only one whose address expression evaluations to $\alpha$ and by Theorem 1, $\log p_{G}(\mathtt{tr}_{1})-\log p_{G}(\mathtt{tr}_{2})=\log\bar{p}_{G_{k}}(\mathtt{tr}_{1},\sigma)-\log\bar{p}_{G_{k}}(\mathtt{tr}_{2},\sigma)$ . After rearranging, we have
| | $\displaystyle\Delta_{\alpha}(\mathtt{tr}_{1})-\Delta_{\alpha}(\mathtt{tr}_{2})$ | $\displaystyle=(\log p_{G}(\mathtt{tr}_{1})-\log p_{\alpha}(\mathtt{tr}_{1}))-(\log p_{G}(\mathtt{tr}_{2})-\log p_{\alpha}(\mathtt{tr}_{2}))$ | |
| --- | --- | --- | --- |
∎
### D.4. Proof of Corollary 3 - Correctness of LMH Optimisation
To prove correctness of the LMH optimisation, we require the notion of keys and minimal traces.
** Definition 0**
*The set of keys of a trace $\mathtt{tr}$ is the set of addresses that map to an non- $\mathtt{null}$ value
$$
\textnormal{keys}(\mathtt{tr})\coloneqq\{\alpha\in\mathbf{Strings}\colon\mathtt{tr}(\alpha)\neq\mathtt{null}\}.
$$ A trace $\mathtt{tr}$ is minimal with respect to $G$ if
$$
p_{G}(\mathtt{tr})\neq\textnormal{undefined}\quad\text{and}\quad\forall a\in\mathbf{Strings}\colon p_{G}(\mathtt{tr}[\alpha\mapsto\mathtt{null}])=\textnormal{undefined}.
$$*
Note that the density is undefined if a trace is read at an address that maps to $\mathtt{null}$ , see (2). Since a trace is minimal if setting a single additional address to $\mathtt{null}$ results in undefined density, the minimality condition captures ”key errors”. For a minimal trace $\textnormal{keys}(\mathtt{tr})$ is the minimal set of addresses that need to be set to non- $\mathtt{null}$ values such that the density is well-defined, i.e. the trace contains no redundant information. We can immediately establish following lemma. Here, and in the following, we often omit the dependency on $G$ and write $p(\mathtt{tr})=p_{G}(\mathtt{tr})$ to declutter notation.
** Lemma 0**
*Let $\mathtt{tr}_{1}$ be a minimal trace and $\mathtt{tr}_{2}$ a trace such that $\forall\alpha\in\textnormal{keys}(\mathtt{tr}_{1})\colon\mathtt{tr}_{1}(\alpha)=\mathtt{tr}_{2}(\alpha)$ . Then, the execution sequences of $\mathtt{tr}_{1}$ and $\mathtt{tr}_{2}$ as in Proposition 4 are the same and $p(\mathtt{tr}_{1})=p(\mathtt{tr}_{2}).$*
* Proof*
By induction on the execution sequence. Assume the execution sequences are equal up to sample node $N$ with address expression $E_{0}$ and state $\sigma$ . Since $p(\mathtt{tr}_{1})\neq\textnormal{undefined}$ , we must have $\mathtt{tr}_{1}(\sigma(E_{0}))\neq\mathtt{null}$ in (2). Thus, we have $\sigma(E_{0})\in\textnormal{keys}(\mathtt{tr}_{1})$ and $\mathtt{tr}_{2}(\sigma(E_{0}))=\mathtt{tr}_{1}(\sigma(E_{0}))\neq\mathtt{null}$ and the execution sequence continue to be equal. All other transition rules follow immediately. ∎
Next, we formally define the semantics of the LMH kernel (Wingate et al., 2011) in our setting.
** Definition 0**
*Let $Q(\beta)$ be a proposal distribution for each address $\beta$ and $\texttt{vs}(\beta)\sim Q(\beta)$ a sample from $Q(\beta)$ . For a minimal trace $\mathtt{tr}$ , the semantics of the LMH kernel (Wingate et al., 2011) that resamples at address $\alpha$ is given below, where we introduce new reserved variables $\boldsymbol{tr}$ and $\boldsymbol{q}$ .
Let there exists a state $\sigma\in\Sigma$ such that $(\sigma_{0},S)\Downarrow^{\mathtt{tr},\texttt{vs}}_{\texttt{LMH}(\alpha)}\sigma$ for program $S$ and initial program state $\sigma_{0}=(x_{1}\mapsto\mathtt{null},\dots,x_{n}\mapsto\mathtt{null},\textbf{p}\mapsto 1,\boldsymbol{tr}\mapsto\texttt{nulltr},\boldsymbol{q}\mapsto 1)$ , where nulltr is a trace that maps all addresses to $\mathtt{null}$ . Then, the new trace $\mathtt{tr}^{\prime}\coloneqq\sigma(\boldsymbol{tr})$ is called valid LMH proposal and $\mathtt{tr}^{\prime}$ is a minimal trace that agrees with $\mathtt{tr}$ on $\textnormal{keys}(\mathtt{tr})\cap\textnormal{keys}(\mathtt{tr}^{\prime})\setminus\{\alpha\}$ . Furthermore, there exists a state $\sigma^{\prime}$ such that $(\sigma_{0},S)\Downarrow^{\mathtt{tr}^{\prime},\mathtt{tr}}_{\texttt{LMH}(\alpha)}\sigma^{\prime}$ and $\mathtt{tr}=\sigma^{\prime}(\boldsymbol{tr})$ . With $p(\mathtt{tr}^{\prime})=\sigma(\textbf{p})$ , $Q_{\alpha}(\mathtt{tr}^{\prime}|\mathtt{tr})=\sigma(\boldsymbol{q})$ , $p(\mathtt{tr})=\sigma^{\prime}(\textbf{p})$ , and $Q_{\alpha}(\mathtt{tr}|\mathtt{tr}^{\prime})=\sigma^{\prime}(\boldsymbol{q})$ the acceptance probability is given by
$$
A=\min\left(1,\frac{p(\mathtt{tr}^{\prime})\times Q_{\alpha}(\mathtt{tr}|\mathtt{tr}^{\prime})}{p(\mathtt{tr})\times Q_{\alpha}(\mathtt{tr}^{\prime}|\mathtt{tr})}\right).
$$ Lastly, let the equivalent semantics on the CFG be denoted by $\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr},\texttt{vs}}{\longrightarrow}}$ .*
** Definition 0**
*We can translate the LMH semantics to the semantics of context ForwardCtx, denoted by $\Downarrow^{\mathtt{tr},\texttt{vs}}_{\texttt{Fwd}(\alpha)}$ , and of context BackwardCtx, denoted by $\Downarrow^{\mathtt{tr}}_{\texttt{Bck}(\alpha)}$ . Using log-densities, at the visit node, we have:
At read nodes, we just read the trace $\mathtt{tr}$ :
The semantics of score nodes look similar to the semantics of sample statements in Definition 7 with the difference that $V_{0}\neq\alpha$ :
The semantics of the BackwardCtx are simply
$$
\Downarrow^{\mathtt{tr}}_{\texttt{Bck}(\alpha)}\,=\,\Downarrow^{\mathtt{tr}^{\prime},\mathtt{tr}}_{\texttt{Fwd}(\alpha)}.
$$*
Now, we are ready to prove Corollary 3 which we make more precise here.
Statement. For address $\alpha$ and minimal trace $\mathtt{tr}$ , let vs be values from the proposal distributions as in Definition 7 and let $\mathtt{tr}^{\prime}$ be a valid LMH proposal. Assume that the address expression of at most one sample node in the execution sequence evaluates to $\alpha$ for all traces. Then, the execution sequences of $\mathtt{tr}$ and $\mathtt{tr}^{\prime}$ are equal up to $(\sigma,M_{\alpha})$ , where $M_{\alpha}$ is the first and only sample node whose address expression evaluates to $\alpha$ . For the sliced CFG $G_{k}$ , where $\iota_{\textnormal{cfg}}(M_{\alpha})=N_{k}$ , we have
$$
\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})=\log\bar{p}_{G_{k}}(\mathtt{tr}^{\prime},\sigma)-\log\bar{p}_{G_{k}}(\mathtt{tr},\sigma).
$$
The quantities $\log\bar{p}_{G_{k}}(\mathtt{tr}^{\prime},\sigma)$ , and $\log Q_{\alpha}(\mathtt{tr}^{\prime}|\mathtt{tr})$ are computed by ForwardCtx and the quantities $\log\bar{p}_{G_{k}}(\mathtt{tr},\sigma)$ and $\log Q_{\alpha}(\mathtt{tr}|\mathtt{tr}^{\prime})$ are computed by BackwardCtx. The new trace $\mathtt{tr}^{\prime}$ can be constructed from $\mathtt{tr}$ and the output of both contexts.
* Proof*
Since $\mathtt{tr}^{\prime}$ is a valid LMH proposal for $\mathtt{tr}$ , we have that both traces are minimal and $\forall\beta\in\textnormal{keys}(\mathtt{tr})\cap\textnormal{keys}(\mathtt{tr}^{\prime})\setminus\{\alpha\}\colon\mathtt{tr}(\beta)=\mathtt{tr}^{\prime}(\beta)$ . Let $\mathtt{tr}_{1}=\mathtt{tr}$ and $\mathtt{tr}_{2}=\mathtt{tr}^{\prime}$ and define two new traces
$$
\overline{\mathtt{tr}_{i}}(\beta)=\begin{cases}\mathtt{tr}_{i}(\alpha)&\text{ if }\beta=\alpha\\
\mathtt{tr}_{1}(\beta)=\mathtt{tr}_{2}(\beta)&\text{ if }\beta\in(\textnormal{keys}(\mathtt{tr}_{1})\cap\textnormal{keys}(\mathtt{tr}_{2}))\setminus\{\alpha\}\\
\mathtt{tr}_{1}(\beta)&\text{ if }\beta\in\textnormal{keys}(\mathtt{tr}_{1})\setminus\textnormal{keys}(\mathtt{tr}_{2})\\
\mathtt{tr}_{2}(\beta)&\text{ if }\beta\in\textnormal{keys}(\mathtt{tr}_{2})\setminus\textnormal{keys}(\mathtt{tr}_{1})\\
\mathtt{null}&\text{ otherwise.}\end{cases}
$$
It holds that $\forall\beta\in\textnormal{keys}(\mathtt{tr}_{i})\colon\overline{\mathtt{tr}_{i}}(\beta)=\mathtt{tr}_{i}(\beta)$ (Note that $\alpha\in\textnormal{keys}(\mathtt{tr}_{i})$ ). By Lemma 6, $\overline{\mathtt{tr}_{1}}$ has the same execution sequence as $\mathtt{tr}$ and $\overline{\mathtt{tr}_{2}}$ the same as $\mathtt{tr}^{\prime}$ . Since $\overline{\mathtt{tr}_{1}}$ differs from $\overline{\mathtt{tr}_{2}}$ only at $\alpha$ the by Theorem 1 we have
| | $\displaystyle\log p(\mathtt{tr}^{\prime})-\log p(\mathtt{tr})$ | $\displaystyle=\log p(\overline{\mathtt{tr}_{2}})-\log p(\overline{\mathtt{tr}_{1}})=$ | |
| --- | --- | --- | --- | As the LMH semantics do not change the computation of $\sigma(\textbf{p})$ , we immediately conclude that the ForwardCtx computes $\bar{p}_{G_{k}}(\mathtt{tr}^{\prime},\sigma)$ and the BackwardCtx computes $\bar{p}_{G_{k}}(\mathtt{tr},\sigma)$ . As in the proof of Theorem 1, but with LMH semantics, let $M^{\prime}_{1}$ be the last sample node in the execution sequence of $\mathtt{tr}$ such that $\iota_{\textnormal{cfg}}(M^{\prime}_{1})\in G_{k}$ and likewise $M^{\prime}_{2}$ for $\mathtt{tr}^{\prime}$ .
$$
(\sigma_{0},\text{START})\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr},\texttt{vs}}{\longrightarrow}}\cdots\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr},\texttt{vs}}{\longrightarrow}}(\sigma,M_{\alpha})\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr},\texttt{vs}}{\longrightarrow}}\cdots\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr},\texttt{vs}}{\longrightarrow}}(\sigma^{\prime}_{1},M^{\prime}_{1})\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr},\texttt{vs}}{\longrightarrow}}\cdots\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr},\texttt{vs}}{\longrightarrow}}(\sigma_{1},\text{END}),
$$
$$
(\sigma_{0},\text{START})\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr}^{\prime},\mathtt{tr}}{\longrightarrow}}\cdots\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr}^{\prime},\mathtt{tr}}{\longrightarrow}}(\sigma,M_{\alpha})\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr}^{\prime},\mathtt{tr}}{\longrightarrow}}\cdots\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr}^{\prime},\mathtt{tr}}{\longrightarrow}}(\sigma^{\prime}_{2},M^{\prime}_{2})\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr}^{\prime},\mathtt{tr}}{\longrightarrow}}\cdots\underset{\texttt{LMH}(\alpha)}{\overset{\mathtt{tr}^{\prime},\mathtt{tr}}{\longrightarrow}}(\sigma_{2},\text{END}).
$$
For sample nodes that come before $M_{\alpha}$ or after $M^{\prime}_{1}$ or $M^{\prime}_{2}$ the address expressions evaluate to some $\beta\in\textnormal{keys}(\mathtt{tr})\cap\textnormal{keys}(\mathtt{tr}^{\prime})\setminus\{\alpha\}$ . Thus, they do not update $\boldsymbol{q}$ and $\log Q_{\alpha}(\mathtt{tr}^{\prime}|\mathtt{tr})=\log\sigma_{1}(\boldsymbol{q})$ as well as $\log Q_{\alpha}(\mathtt{tr}|\mathtt{tr}^{\prime})=\log\sigma_{2}(\boldsymbol{q})$ are fully computed in the sliced CFG by ForwardCtx and BackwardCtx, respectively (compare Definition 7). For the same reason, the difference between $\mathtt{tr}$ and $\mathtt{tr}^{\prime}$ is also fully accounted for in the sliced CFG. The new trace $\mathtt{tr}^{\prime}$ can be constructed by removing the address-value pairs encountered in the BackwardCtx from $\mathtt{tr}$ and adding the address-value pairs encountered in the ForwardCtx. ∎
### D.5. Proof of Corollary 4 - Correctness of BBVI optimisation
Before we can prove correctness of the BBVI optimisation, we need to formally define the variational distribution over traces $Q_{\phi}$ .
** Definition 0**
*For every address $\alpha$ , let there be a probability measure on some measurable space $\mathcal{M_{\alpha}}=(Z_{\alpha},\Sigma_{\alpha})$ parameterised by $\phi_{\alpha}$ that admits a density $q_{\alpha}(z_{\alpha}|\phi_{\alpha})$ differentiable with respect to $\phi_{\alpha}$ (the density is with respect to the Lebesgue measure on $\mathbb{R}^{d_{\alpha}}$ or counting measure on $\mathbb{Z}^{d_{\alpha}}$ ). For every finite address set $A$ , define the joint density $q_{A}((z_{\alpha})_{\alpha\in A}|(\phi_{\alpha})_{\alpha\in A})=\prod_{\alpha\in A}q_{\alpha}(z_{\alpha}|\phi_{\alpha})$ on the product space $\mathcal{M}_{A}=(Z_{A},\Sigma_{A})=\bigotimes_{\alpha\in A}\mathcal{M_{\alpha}}.$ On the set of traces $\mathcal{T}$ , define the $\sigma$ -algebra $\Sigma_{\mathcal{T}}$ , such that $T\in\Sigma_{\mathcal{T}}$ if and only if for all finite address sets $A$ , we have $\{(\mathtt{tr}(\alpha))_{\alpha\in A}\colon\mathtt{tr}\in T\}\in\Sigma_{A}$ . Lastly, assume that for program density $p$ the set $\mathcal{T}_{\textnormal{minimal}}=\{\mathtt{tr}\in\mathcal{T}\colon\mathtt{tr}\text{ is minimal wrt. }p\}$ is measurable in $\Sigma_{\mathcal{T}}$ . Then, the variational distribution is defined by the density
$$
Q_{\phi}(\mathtt{tr})=1_{\mathcal{T}_{\textnormal{minimal}}}(\mathtt{tr})\sum_{\begin{subarray}{c}A\subseteq\mathbf{Strings},\\
|A|<\infty\end{subarray}}1_{\mathcal{T}_{A}}(\mathtt{tr})\prod_{\alpha\in A}q_{\alpha}(\mathtt{tr}(\alpha)|\phi_{\alpha}),
$$
where $\mathcal{T}_{A}\coloneqq\{\mathtt{tr}\in\mathcal{T}\colon\forall\alpha\in\mathbf{Strings}\colon\mathtt{tr}(\alpha)\neq\mathtt{null}\Leftrightarrow\alpha\in A\}$ . For all measurable functions $f$ we can express the expectation with respect to $Q_{\phi}$ as
| | $\displaystyle\mathbb{E}_{\mathtt{tr}\sim Q_{\phi}}{\left[f(\mathtt{tr})\right]}$ | $\displaystyle=\int f(\mathtt{tr})Q_{\phi}(\mathtt{tr})d\mathtt{tr}$ | |
| --- | --- | --- | --- |
Above $\iota_{\mathcal{T}}(z_{A})$ for $z_{A}=(z_{\alpha})_{\alpha\in A}\in Z_{A}$ is the trace that maps address $\alpha$ to $z_{\alpha}$ if $\alpha\in A$ and all other addresses to $\mathtt{null}$ . Note that we may exchange integration and sum, since for a minimal trace only one term in the sum is non-zero.*
Before repeating the correctness statement in terms of Definition 9, we formally defined the semantics of BBVICtx.
** Definition 0**
*The semantics of the BBVICtx are very similar to the standard semantics with the only difference that we store $\log q_{\alpha}(\mathtt{tr}(\alpha)|\phi_{\alpha})$ at visit statements and the use of log-densities. The semantics of read statements remains unchanged: Lastly, the semantics of score statements are only rewritten in terms of log-densities:*
Statement. Let $Q_{\phi}$ be a variational distribution over traces as in Definition 9. Assume that the address expression of at most one sample node in the execution sequence evaluates to $\alpha$ for all traces. Assume that the program density $p$ and the set $\mathcal{T}_{\textnormal{minimal}}$ are measurable with respect to $(\mathcal{T},\Sigma_{\mathcal{T}})$ . With $p_{\alpha}$ as in Corollary 2, it holds that
| | $\displaystyle\nabla_{\phi_{\alpha}}\mathbb{E}_{\mathtt{tr}\sim Q_{\phi}}{\left[\log p(\mathtt{tr})-\log Q_{\phi}(\mathtt{tr})\right]}=$ | |
| --- | --- | --- |
The quantity $\log p_{\alpha}(\mathtt{tr})-\log q_{\alpha}(\mathtt{tr}(\alpha)|\phi_{\alpha})$ is computed by BBVICtx.
* Proof*
First, we repeat the known identity for the BBVI estimator
| | $\displaystyle\nabla_{\phi_{\alpha}}\mathbb{E}_{\mathtt{tr}\sim Q_{\phi}}{\left[\log p(\mathtt{tr})-\log Q_{\phi}(\mathtt{tr})\right]}=\mathbb{E}_{\mathtt{tr}\sim Q_{\phi}}{\left[\nabla_{\phi_{\alpha}}\big{[}\log Q_{\phi}(\mathtt{tr})\big{]}\big{(}\log p(\mathtt{tr})-\log Q_{\phi}(\mathtt{tr})\big{)}\right]}.$ | |
| --- | --- | --- |
Then, for a minimal trace $\mathtt{tr}$ , we have
| | $\displaystyle\nabla_{\phi_{\alpha}}\big{[}\log Q_{\phi}(\mathtt{tr})\big{]}$ | $\displaystyle=\delta_{\alpha\in\textnormal{keys}(\mathtt{tr})}\sum_{\beta\in\textnormal{keys}(\mathtt{tr})}\nabla_{\phi_{\alpha}}\log q_{\beta}(\mathtt{tr}(\beta)|\phi_{\beta})$ | |
| --- | --- | --- | --- | Further, let $\Delta_{p}(\mathtt{tr})=\log p(\mathtt{tr})-\log p_{\alpha}(\mathtt{tr})$ and $\Delta_{q}(\mathtt{tr})=\log Q_{\phi}(\mathtt{tr})-\log q_{\alpha}(\mathtt{tr}(\alpha)|\phi_{\alpha})$ . For an address set $A$ with $\alpha\in A$ , by Corollary 2 and by definition of $Q_{\phi}$ , both $\Delta_{p}\circ\iota_{\mathcal{T}}$ and $\Delta_{q}\circ\iota_{\mathcal{T}}$ are constant with respect to $z_{\alpha}$ in $Z_{A}$ . Thus,
| | $\displaystyle\int 1_{\mathcal{T}_{\textnormal{minimal}}}(\iota_{\mathcal{T}}(z_{A}))\,\nabla_{\phi_{\alpha}}\log q_{\alpha}(z_{\alpha}|\phi_{\alpha})\,\Delta_{p}(\iota_{\mathcal{T}}(z_{A}))\prod_{\beta\in A}q_{\beta}(z_{\beta})|\phi_{\beta})\,\,dz_{A}=$ | |
| --- | --- | --- |
because $\int\nabla_{\phi_{\alpha}}\big{[}\log q_{\alpha}(z_{\alpha}|\phi_{\alpha})\big{]}q_{\alpha}(z_{\alpha}|\phi_{\alpha})\,dz_{\alpha}=0$ . Similarly,
| | $\displaystyle\int 1_{\mathcal{T}_{\textnormal{minimal}}}(\iota_{\mathcal{T}}(z_{A}))\,\nabla_{\phi_{\alpha}}\log q_{\alpha}(z_{\alpha}|\phi_{\alpha})\,\Delta_{q}(\iota_{\mathcal{T}}(z_{A}))\prod_{\beta\in A}q_{\beta}(z_{\beta})|\phi_{\beta})\,\,dz_{A}=0.$ | |
| --- | --- | --- |
Lastly, we rewrite
| | $\displaystyle f(\mathtt{tr})$ | $\displaystyle\coloneqq\nabla_{\phi_{\alpha}}\big{[}\log Q_{\phi}(\mathtt{tr})\big{]}\big{(}\log p(\mathtt{tr})-\log Q_{\phi}(\mathtt{tr})\big{)}$ | |
| --- | --- | --- | --- |
Since we have shown that the second term in the sum integrates to $0$ for every address set $A$ , with $\alpha\in A$ , by linearity of the integral, we have
| | $\displaystyle\mathbb{E}_{\mathtt{tr}\sim Q_{\phi}}{\left[f(\mathtt{tr})\right]}$ | $\displaystyle=\sum_{\begin{subarray}{c}A\subseteq\mathbf{Strings},\\ |A|<\infty,\alpha\in A\end{subarray}}\int 1_{\mathcal{T}_{\textnormal{minimal}}}(\iota_{\mathcal{T}}(z_{A}))\,f(\iota_{\mathcal{T}}(z_{A}))\prod_{\beta\in A}q_{\beta}(z_{\beta})|\phi_{\beta})\,\,dz_{A}$ | |
| --- | --- | --- | --- | Finally, from the definition of the BBVICtx it follows immediately that this context computes the quantities $\log p_{\alpha}(\mathtt{tr})$ and $\log q_{\alpha}(\mathtt{tr}(\alpha)|\phi_{\alpha})$ . ∎
### D.6. Proof of Proposition 5 - Correctness of SMC optimisation
First, we formalise the sliced CFG construction for SMC.
** Definition 0**
*Let $G=(N_{\textnormal{start}},N_{\textnormal{end}},\mathcal{N},\mathcal{E})$ be a CFG with $K$ sample nodes, which we enumerate with $$ for $j=1,\dots,K$ . We define the set of nodes that lie on path from $N_{k}$ to some of other sample node $N_{j}$ :
| | $\displaystyle\mathcal{N}_{k}\coloneqq\{N\in\mathcal{N}\colon\exists j\in\{1,\dots,K\}\colon$ | $\displaystyle\exists\text{ path }\nu=(N_{k},\dots,N_{j})\colon$ | |
| --- | --- | --- | --- |
In this construction, we do not require read statements. We restrict the set of edges to the subset of nodes $\mathcal{N}_{k}$ :
$$
\mathcal{E}_{k}^{\prime}\coloneqq\{(e_{1},e_{2})\colon(e_{1},e_{2})\in\mathcal{E}\land e_{1}\in\mathcal{N}_{k}\land e_{2}\in\mathcal{N}_{k}\}.
$$
We connect the new start node $N^{k}_{\textnormal{start}}$ to $N_{k}$ and the new end node $N^{k}_{\textnormal{end}}$ to all $N_{j}$ , $j\in\{1,\dots,K\}$ :
$$
\mathcal{E}_{k}=\mathcal{E}_{k}^{\prime}\cup\{(N^{k}_{\textnormal{start}},N_{k})\}\cup\{(N_{j},N^{k}_{\textnormal{end}})\colon j\in\{1,\dots,K\}\land N_{j}\in\mathcal{N}_{k}\}.
$$
Finally, define the CFG sliced with respect to $N_{k}$ as
$$
G_{k}^{\texttt{SMC}}\coloneqq(N^{k}_{\textnormal{start}},N^{k}_{\textnormal{end}},\mathcal{N}_{k},\mathcal{E}_{k}).
$$*
The ”continuation property” of this sliced CFG follows directly from its construction.
Statement. Let $G$ be a CFG such that for initial program state $\sigma_{0}$ and trace $\mathtt{tr}$ , we have execution sequence $(\sigma_{0},\text{START})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{i},M_{i})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma_{l},\text{END})$ in its unrolled version $H$ . Let $(\sigma^{\prime}_{1},M^{\prime}_{1})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{2},M^{\prime}_{2})$ be a sub-sequence such that $\iota_{\textnormal{cfg}}(M^{\prime}_{1})=N_{k}$ and $\iota_{\textnormal{cfg}}(M^{\prime}_{2})=N_{j}$ are the only sample nodes. Then, the execution sequence in the unrolled version of the sliced CFG $G_{k}^{\texttt{SMC}}$ matches the sub-sequence: $(\sigma^{\prime}_{1},\text{START})\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{1},M^{\prime}_{1})\overset{\mathtt{tr}}{\longrightarrow}\cdots\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{2},M^{\prime}_{2})\overset{\mathtt{tr}}{\longrightarrow}(\sigma^{\prime}_{2},\text{END}).$
* Proof*
Follows directly from Definition 11. ∎