Variable Elimination as Rewriting in a Linear Lambda Calculus

Probabilistic programming languages (PPLs) provide a rich and expressive framework for stochastic modeling and Bayesian reasoning. The crucial but computationally hard task is that of inference, i.e. computing explicitly  the probability distribution which is implicitly specified by the probabilistic program. Most PPLs focus on continuous random variables—in this setting the inference engine typically implements approximate inference algorithms based on sampling methods (such as importance sampling, Markov Chain Monte Carlo, Gibbs sampling). However, several domains of application (e.g. network verification, ranking and voting, text or graph analysis) are naturally discrete, yielding to an increasing interest in the challenge of exact inference [17, 19, 21, 34, 35, 39, 44, 46]. A good example is Dice [21], a first-order functional language whose inference algorithm exploits the structure of the program in order to factorise inference, making it possible to scale exact inference to large distributions. A common ground to most exact approaches is to be inspired by techniques for exact inference on discrete graphical models, which typically exploit probabilistic independence as the key for compact representation and efficient inference.

Indeed, specialized formalisms do come with highly efficient algorithms for exact inference; a prominent example is that of Bayesian networks, which enable algorithms such as Message Passing [37] and Variable Elimination [45]—to name two classical ones—and a variety of approaches for exploiting local structure, such as reducing inference to Weighted Model Counting [3, 4]. General-purpose programming language do provide a rich expressiveness, which allows in particular for the encoding of Bayesian networks, however, the corresponding algorithms are often lost when leaving the realm of graphical models for PPLs, leaving an uncomfortable gap between the two worlds. Our goal is shedding light in this gray area, understanding exact inference as an algorithm acting on programs.

In pioneering work, Koller et al. [27] define a general purpose functional language which not only is able to encode Bayesian networks (as well as other specialized formalisms), but also comes with an algorithm which mimics Variable Elimination (\(\textsf{VE}\) for short) by means of term transformation. \(\textsf{VE}\) is arguably the simplest algorithm for exact inference, which is factorised into smaller intermediate computations, by eliminating the irrelevant variables according to a specific order. The limit in [27] is that unfortunately, the algorithm there can only implement a specific elimination ordering (the one determined by the lazy evaluation implicit in the algorithm), which might not be the most efficient: a different ordering might result in smaller intermediate factors. The general problem to be able to deal with any possible ordering, hence producing any possible factorisation, is there left as an open challenge for further investigation. The approach that is taken by the authors in a series of subsequent papers will go in a different direction from term rewriting; eventually in [39] programs are compiled into an intermediate structure, and it is on this graph structure that a sophisticated variant of \(\textsf{VE}\) is performed. The question of understanding \(\textsf{VE}\) as a transformation on programs remains still open; we believe it is important for a foundational understanding of PPLs.

In this paper, we provide an answer, defining an inference algorithm which fully formalizes the classical \(\textsf{VE}\) algorithm as rewriting of programs, expressed in an idealized probabilistic functional language—a linear simply-typed \(\lambda \)-calculus suffices for our purpose. Formally, we prove soundness and completeness of our algorithm with respect to the standard one. Notice that the choice of the elimination order is not part of a \(\textsf{VE}\) algorithm—several heuristics are available in the literature to compute an efficient elimination order (see e.g. [8]). As wanted, we prove that any given elimination ordering can be implemented by our algorithm. When we run it on a stochastic program representing a Bayesian network, its computational behaviour is the same as that of standard \(\textsf{VE}\) for Bayesian networks, and the cost is of the same complexity order. While the idea behind \(\textsf{VE}\) is simple, crafting an algorithm on terms which is able to implement any elimination order is non-trivial— our success here relies on the use of linear types \(P\multimap T\) enabled by linear logic [18], accounting for the interdependences generated by a specific elimination order. Let us explain the main ideas.

Factorising Inference, via the graph structure. Bayesian networks describe a set of random variables and their conditional (in)dependencies. Let us restrict ourselves to boolean random variables, i.e. variables x representing a boolean value \(\texttt{t}\) or \(\texttt{f}\) with some probability.¹ Such a variable can be described as a vector of two non-negative real numbers \((\rho _\texttt{t}, \rho _\texttt{f})\) quantifying the probability \(\rho _\texttt{t}\) (resp. \(\rho _\texttt{f}\)) of sampling \(\texttt{t}\) (resp. \(\texttt{f}\)) from x.

Fig. 1a depicts an example of Bayesian network. It is a directed acyclic graph \(\mathcal {G}\) where the nodes are associated with random variables and where the arrows describe conditional dependencies between these variables. For instance, in Fig. 1a the variable \(x_5\) depends on the values sampled from \(x_3\) and \(x_4\), and, in turn, it affects the probability of which boolean we can sample from \(x_6\). The network does not give a direct access to a vector \((\rho _\texttt{t}, \rho _\texttt{f})\) describing \(x_5\) by its own, but only to a stochastic matrix \(\mathtt M_5\) quantifying the conditional dependence of \(x_5\) with respect to \(x_3\) and \(x_4\). Formally, \(\mathtt M_5\) is a matrix with four rows, representing the four possible outcomes of a joint sample of \(x_3\) and \(x_4\) (i.e. \((\texttt{t}, \texttt{t})\), \((\texttt{t}, \texttt{f})\), \((\texttt{f}, \texttt{t})\), \((\texttt{f}, \texttt{f})\)), and two columns, representing the two possible outcomes for \(x_5\). The matrix is stochastic in the sense that each line represents a probabilistic distribution of booleans: for instance, \((\mathtt M_5)_{(\texttt{t}, \texttt{f}), \texttt{t}}=0.4\) and \((\mathtt M_5)_{(\texttt{t}, \texttt{f}), \texttt{f}}=0.6\) mean that \(\texttt{t}\) can be sampled from \(x_5\) with a 40% chance, while \(\texttt{f}\) with 60%, whenever \(x_3\) has been observed to be \(\texttt{t}\) and \(x_4\) to be \(\texttt{f}\).

Having such a graph \(\mathcal {G}\) and the stochastic matrices \(\mathtt M_1\), \(\mathtt M_2\), \(\mathtt M_3\), etc. associated with its nodes, a typical query is to compute the joint probability of a subset of the variables of \(\mathcal {G}\). For example, the vector \(\Pr (x_3,x_6)=(\rho _{(\texttt{t}, \texttt{t})},\rho _{(\texttt{t}, \texttt{f})},\rho _{(\texttt{f}, \texttt{t})},\rho _{(\texttt{f}, \texttt{f})})\) giving the marginal over \(x_3\) and \(x_6\), i.e. the probability of the possible outcomes of \(x_3\) and \(x_6\). A way to obtain this is first computing the joint distributions of all variables in the graph in a single shot and then summing out the variable we are not interested in. This will give, for every possible boolean value \(b_3,b_6\) in \(\{\texttt{t},\texttt{f}\}\) taken by, respectively, \(x_3\) and \(x_6\), the following expression: For each of the \(2^2\) possible values of the indexes \((b_3, b_6)\) we have a sum of \(2^4\) terms. That is, to compute the joint probability of \((x_3, x_6)\), we have to compute \(2^6\) entries. This method is unfeasible in general as it requires a number of operations exponential in the size of \(\mathcal {G}\). Luckily, one can take advantage of the conditional (in)dependencies underlined by \(\mathcal {G}\) to get a better factorisation than in (1), breaking the computation in that of factors of smaller size. For example: Let us denote by \(\phi ^i\) the intermediate factor in (2) identified by the sum over \(b_i\): for example \(\phi ^2\) is the sum \(\sum _{b_2}\phi ^1_{b_2}(\mathtt M_3)_{b_2, b_3}(\mathtt M_6)_{(b_2, b_5), b_6}\). Notice that if we suppose to have memorised the results of computing \(\phi ^1\), to obtain \(\phi ^2\) requires to compute \(2^4\) entries, i.e. the cost is exponential in the number of the different indexes \(b_j\)’s appearing in the expression defining \(\phi ^2\). By applying the same reasoning to all factors in (2), one notices that in the whole computation we never need to compute more than \(2^4\) entries: we have gained a factor of \(2^2\) with respect to (1).

The Variable Elimination algorithm performs factorisations like (2) in order to compute more efficiently the desired marginal distribution. The factorisation is characterised by an ordered sequence of unobserved (or marginalised) variables to eliminate, i.e. to sum out. The factorisation in (2) is induced by the sequence \((x_1,x_2,x_4,x_5)\): \(\phi ^1\) eliminates variable \(x_1\), \(\phi ^2\) then eliminates variable \(x_2\), and so on. Different orders yield different factorisations with different performances, e.g. the inverse order \((x_5,x_4,x_2,x_1)\) is less efficient, as the largest factor here requires to compute \(2^5\) entries.

Factorising Inference, via the program structure. In the literature, factorisations are usually described as collections of factors (basically vectors) and the \(\textsf{VE}\) algorithm is presented as an iterative algorithm acting on such collections. In this paper we propose a framework that gives more structure to this picture, expressing \(\textsf{VE}\) as a program transformation, building a factorisation by induction on the structure of a program, compositionally. More precisely:

The reader can easily convince herself that the query about the joint marginal distribution \((x_3, x_6)\) to the Bayesian network in Fig. 1a can be expressed by the let-term \(\ell \) in Fig. 1b, where we have enriched the syntax of \(\lambda \)-terms with the constants representing the stochastic matrices. We consider \(\texttt{let}\, x\, =\, e\, \texttt{in}\, e'\) as a syntactic sugar for \((\lambda x. e')e\), so the term \(\ell \) can be seen as a \(\lambda \)-term, which is moreover typable in a linear type system like the one in Fig. 2. The fact that some variables \(x_i\) have more free occurrences in sub-terms of \(\ell \) is not in contrast with the linearity feature of the term, as let-expressions are supposed to be evaluated following a call-by-value strategy, and ground values (as e.g. booleans) can be duplicated in linear systems (see Ex. 1 and Remark 2 for more details).

Terms of this type are associated in quantitative denotational semantics such as [7, 29] with algebraic expressions which give the joint distribution of the output variables. Here, in the same spirit as [11], we adopt a variant of the quantitative denotation (Sect. 3), which can be seen as a compact reformulation of the original model, and is more suitable to deal with factorised inference. It turns out that when we compositionally compute the semantics of \(\ell \) following the structure of the program, we have a more efficient computation than in (1). This is because the inductive interpretation yields intermediate factors of smaller size, similarly to what algorithms for exact inference do. Indeed, the inductive interpretation of \(\ell \) behaves like \(\textsf{VE}\) with the elimination order \((x_5,x_4,x_2,x_1)\), see Ex. (5).

Notice that different programs may encode the same model and query, but with a significantly different inference cost, due to their different structure. A natural question is then to wonder if we can directly act on the structure of the program, in such a way that the semantics is invariant, but inference is more efficient. In fact, we show that the language \(\mathcal {L}\) is sufficiently expressive to represent all possible factorisations of (1), e.g. (2). The main idea for such a representation arises from the observation that summing-out variables in the semantics corresponds in the syntax to make a let-in definition local to a sub-expression. For example, the factor \(\phi ^1 = \sum _{b_1}(\mathtt M_1)_{b_1}(\mathtt M_2)_{b_1, b_2}\) of (2) can be easily obtained by making the variable \(x_1\) local to the definition of \(x_2\), creating a \(\lambda \)-term \(e^1\) of the shape \(\texttt{let}\, x_1\, =\, \mathtt M_1\, \texttt{in}\, \mathtt M_2 x_1\) and replacing the first two definitions of \(\ell \) with \(\texttt{let}\, x_2\, =\, e^1\, \texttt{in}\, \dots \). In fact, the denotation of \(e^1\) is exactly \(\phi ^1\). What about \(\phi ^2\)? Here the situation is subtler as in order to make local the definition of \(x_2\) one should gather together the definitions of \(x_3\) and \(x_6\), but the definition of \(x_6\) depends on a variable \(x_5\) which in turn depends on \(x_3\), so a simple factor of ground types (i.e. tensors of booleans) will generate a dependence cycle. Luckily, we can use a (linear) functional type, defining a \(\lambda \)-term \(e^2\) as \(\texttt{let}\, x_2\, =\, e^1\, \texttt{in}\, (\mathtt M_3 x_2, \lambda x_5.\mathtt M_6 (x_2, x_5))\) and then transforming \(\ell \) into Fig. 1c. Again, we can notice that the denotation of \(e^2\) is exactly \(\phi ^2\). Fig. 7 details² the whole rewriting mimicking the elimination of the variables \((x_1, x_2, x_4, x_5)\) applied to \(\ell \). This paper shows how to generalise this reasoning to any let-term.

Contents of the paper. We present an algorithm which is able to fully perform \(\textsf{VE}\) on programs: for any elimination order, program \( \ell \) is rewritten by the algorithm into program \( \ell '\), representing—possibly in a more efficient way—the same model. As stressed, our investigation is of foundational nature; we focus on a theoretical framework in which we are able to prove the soundness and completeness (Th. 1, Cor. 1) of the \(\textsf{VE}\) algorithm on terms. To do so, we leverage on the quantitative denotation of the terms. The structure of the paper is as follows.

– Sect. 2 defines the linear \(\lambda \)-calculus \(\mathcal {L}\), and its semantics. In particular, Fig. 2 gives the linear typing system, which is a fragment of multiplicative linear logic [18] (Remark 2). Fig. 4 sketches the denotational semantics of \(\mathcal {L}\) as weighted relations [29]. At first, the reader who wishes to focus on \(\textsf{VE}\) can skip the formal details about the semantics, and just read the intuitions in Sect. 2.2.

– Sect. 3 formalises the notion of factorisation as a set of factors (Def. 1) and shows how to associate a factorisation to the let-terms in \(\mathcal {L}\) (Def. 4). Def. 5 recalls the standard \(\textsf{VE}\) algorithm—acting on sets of factors—denoted by \(\textsf{VE}^{\mathsf F}\).

– Sect. 4 is the core of our paper, capturing \(\textsf{VE}\) as a let-term transformation (Def. 8), denoted here by \(\textsf{VE}^\mathcal {L}\), using the rewriting rules of Fig. 6. We prove the correspondence between the two versions of \(\textsf{VE}\) in Th. 1 and Cor. 1, stating our main result, the soundness and completeness of \(\textsf{VE}^\mathcal {L}\) with respect to \(\textsf{VE}^{\mathsf F}\).

As an extra bonus, an enrichment of the semantics—based on probabilistic coherence spaces [7]—yields a neat property of the terms of \(\mathcal {L}\), namely that the total mass of the denotation is easily computable from the terms type (Prop. 1).

Missing proofs and more technical details are in the extended version [12].

Related work. Variants of factorisation algorithms were invented independently in multiple communities (see [28] for a survey). The algorithm of Variable Elimination (\(\textsf{VE}\)) was first formalised in [45]. The approach to \(\textsf{VE}\) which is usually taken by PPLs is to compile a program into an intermediate structure, on which \(\textsf{VE}\) is performed. Our specific contribution is to provide the first algorithm which fully performs \(\textsf{VE}\) directly on programs. As explained, by this we mean the following. First, we observe that the inductive interpretation of a term behaves as \(\textsf{VE}\), for an ordering of the variables to eliminate which is implicit in the structure of the program—possibly a non-efficient one. Second, our algorithm transforms the program in such a way that its structure reflects \(\textsf{VE}\) according to any arbitrary ordering, while the semantics (the denoted model) is invariant.

As we discussed before, our work builds on the programme put forward in [27]. Pfeffer [39](page 417) summarizes this way the limits of the algorithm in [27]: "The the solution is only partial. Given a BN encoded in their language, the algorithm can be viewed as performing Variable Elimination using a particular elimination order: namely, from the last variable in the program upward. It is well-known that the cost of VE is highly dependent on the elimination order, so the algorithm is exponentially more expensive for some families of models than an algorithm that can use any order." The algorithm we present here achieves a full solution: any elimination order can be implemented.

– Rewriting the program to improve inference efficiency, as in [19]. A key goal of PPLs is to separate the model description (the program) from the inference task. As pointed out by [19], such a goal is hard to achieve in practice. To improve inference efficiency, users are often forced to re-write the program by hand.

– Exploiting the local structure of the program to achieve efficient inference, as in [21]. This road is taken by the authors of the language Dice—here the algorithm does not act on the program itself.

Our work incorporates elements from both lines: we perform inference compositionally, following the inductive structure of the program; to improve efficiency, our rewriting algorithm modifies the program structure (modelling the \(\textsf{VE}\) algorithm),while keeping the semantics invariant.

As a matter of fact, our first-order language is very similar to the language Dice [21], and has similar expressiveness. In order to keep presentation and proofs simple, we prefer to omit a conditioning construct such as observe, but it could easily be accommodated (see Sect. 5). There are however significant differences. We focus on \(\textsf{VE}\), while Dice implements a different inference algorithm, compiling programs to weighted Boolean formulas, then performing Weighted Model Counting [3]. Moreover, as said, Dice exploits the local structure of the given program, without program transformations to improve the inference cost, which is instead at the core of our approach.

Rewriting is central to [19]. The focus there is on probabilistic programs with mixed discrete and continuous parameters: by eliminating the discrete parameters, general (gradient-based) algorithms can then be used. To automate this process, the authors introduce an information flow type system that can detect conditional independencies; rewriting uses \(\textsf{VE}\) techniques, even though the authors are not directly interested in the equivalence with the standard \(\textsf{VE}\) algorithm (this is left as a conjecture). In the same line, we mention also a very recent work [31] which tackle a similar task as [19]; while using similar ideas, a new design in both the language and the information flow type system allows the authors to deal with bounded recursion. The term transformations have a different goal than ours, compiling a probabilistic program into a pure one. However, some key elements there resonate with our approach: program transformations are based on continuation passing style (we use arrow variables in a similar fashion); the language in [31] is not defined by an operational semantics, instead the authors —like us— adopt a compositional, denotational treatment.

Denotational semantics versus cost-awareness. Our approach integrates and is grounded on a quantitative denotational semantics. Pioneering work by [24, 25] has paved the way for a logical and semantical comprehension of Bayesian networks and inference from a categorical perspective, yielding an extensive body of work based on the setting of string diagrams, e.g. [5, 22, 23]. A denotational take on Bayesian networks is also at the core of [36], and underlies the categorical framework of [43]. These lines of research however do not take into consideration the computational cost, which is the very reason motivating the introduction and development of Bayesian networks, and inference algorithms such as \(\textsf{VE}\). In the literature, foundational understanding tends to focus on either a compositional semantics or on efficiency, but the two worlds are separated, and typically explored as independent entities. This dichotomy stands in stark contrast to Bayesian networks, where the representation, the semantics (i.e. the underlying joint distribution), and the inference algorithms are deeply intertwined. A new perspective has been recently propounded by [11], advocating the need for a quantitative semantical approach more attentive to the resource consumption and to the actual cost of computing the semantics, which here exactly corresponds to performing inference. Our contribution fits in this line, which inspires also the cost-aware semantics in [16]. The latter introduces a higher-order language -in the idealized form of a \(\lambda \)-calculus-which is sound and complete w.r.t. Bayesian networks, together with a type system which computes the cost of (inductively performed) inference. Notice that [16] does not deal with terms transformations to rewrite a program into a more efficient one. Such transformations, reflecting the essence of the \(\textsf{VE}\) algorithm, is exactly the core of our paper — our algorithm easily adapts to the first-order fragment of [16].

We consider a linear simply typed \(\lambda \)-calculus extended with stochastic matrices over tuples of booleans. Our results can be extended to more general systems, but here we focus on the core fragment able to represent Bayesian networks and the factorisations produced by the \(\textsf{VE}\) algorithm. In particular, we adopt a specific class of types, where arrow types are restricted to linear maps from (basically) tuples of booleans (i.e.  the values of positive types in the grammar below) to pairs of a tuple of booleans and, possibly, another arrow.

As mentioned in the Introduction, variable elimination is an iterative procedure transforming sets of factors (one can think of these as originally provided by a Bayesian network). We recall this procedure, adapting it to our setting—in particular, we start from a set \(\textsf{Fs}(\ell )\) of factors generated by a let-term \(\ell \) representing a Bayesian network. Subsect. 3.1 defines factors and the main operations on them (product and summing-out). Subsect. 3.2 shows how to associate a let-term \(\ell \) with a set of factors \(\textsf{Fs}(\ell )\) such that from their product one can recover \(\llbracket \ell \rrbracket \) (Prop. 3). Finally, Subsect. 3.3 presents the variable elimination algorithm as a transformation \(\textsf{VE}^{\mathsf F}\) over \(\textsf{Fs}(\ell )\) (Def. 5) and Prop. 4 gives the soundness of the algorithm. This latter result is standard from the literature (see e.g. [8]), and the contribution of this section is the definition of \(\textsf{Fs}(\ell )\) which is essential to link this variable elimination \(\textsf{VE}^{\mathsf F}\) on factors to our main contribution given in the next section: the variable elimination \(\textsf{VE}^\mathcal {L}\) as a term-rewriting process.

This section contains our main contribution, expressing the variable elimination algorithm syntactically, as a rewriting of let-terms, transforming the “eliminated” variables from global variables (i.e. defined by a definition of a let-term and accessible to the following definitions), into local variables (i.e. private to some subexpression in a specific definition). Subsect. 4.1 defines such a rewriting \(\rightarrow \) of let-terms (Fig. 6) and states some of its basic properties. Subsect. 4.2 introduces the \(\textsf{VE}^\mathcal {L}\) transformation as a deterministic strategy to apply \(\rightarrow \) in order to make local the variable to be eliminated (Def. 8), without changing the denotational semantics of the term (Prop. 6). Theorem 1 and Corollary 1 prove that \(\textsf{VE}^\mathcal {L}\) and \(\textsf{VE}^{\mathsf F}\) are equivalent, showing that \(\textsf{Fs}(\cdot )\) commutes over the two transformations. Finally, Subsect. 4.2 briefly discusses some complexity properties, namely that the \(\textsf{VE}^\mathcal {L}\) increases the size of a let-term quite reasonably, keeping a linear bound.

We have identified a fragment \(\mathcal {L}\) of the linear simply-typed \(\lambda \)-calculus which can express syntactically any factorisation induced by a run of the variable elimination algorithm over a Bayesian network. In particular, we define a rewriting (Fig. 6) and a reduction strategy \(\textsf{VE}^\mathcal {L}\) (Def. 8) that, given a sequence \((x_1,\dots , x_n)\) of variables to eliminate, transforms in \(O(n\textsf{s}(\ell ))\) steps a let-term \(\ell \) into a let-term \(\textsf{VE}^\mathcal {L}(\ell , (x_1,\dots , x_n))\) associated with the factorisation generated by the \((x_1,\dots , x_n)\) elimination (Corollary 1). We have proven that the size of \(\textsf{VE}^\mathcal {L}(\ell , (x_1,\dots , x_n))\) is linear in the size of \(\ell \) and in the number of variables involved in the elimination process (Prop. 8).

Our language is a fragment of a more expressive one [15], in which several classes of stochastic models can be encoded. Our work is therefore a step towards defining standard exact inference algorithms on a general-purpose stochastic language, as first propounded in [27] with the goal is to have general-purpose algorithms of reasonable cost, usable on any model expressed in the language.

While it is known (see [26], Sect. 9.3.1.3) that \(\textsf{VE}\) produces intermediate factors that are not conditional probabilities—i.e. not stochastic matrices— our approach is able to associate a term and a type to such factors. In fact, the types of the calculus \(\mathcal {L}\) give a logical description of the interdependences between the factors generated by the \(\textsf{VE}\) algorithm: the grammar is more expressive than just the types of stochastic matrices between tuples of booleans (Remark 1).

Discussion and perspectives. Since our approach is theoretical, the main goal has been to give a formal framework for proving the soundness and the completeness of \(\textsf{VE}^\mathcal {L}\). For that sake, the rewriting rules of Fig. 6 are reduced to a minimum, in order to keep reasonable the number of cases in the proofs. The drawback is that the rewritten terms have a lot of bureaucratic code, as the reader may realize by looking at Fig. 7. Although this fact is not crucial from the point of view of the asymptotic complexity, when aiming at a prototypical implementation, one may enrich the rewriting system with more rules to avoid useless code.

The grammar of let-terms recalls the notion of administrative normal form (abbreviated ANF), which is often used as an intermediate representation in the compilation of functional programs. In particular, let-terms and ANF share in common the restriction of applications to variables, so suggesting a precise evaluation order. Several optimisations are defined as transformations over ANF, even considering some let-floating rules analogous to the ones considered in Fig. 6, see e.g. [38]. Comparing these optimisations is not trivial as the cost model is different. E.g. [38] aims to reduce heap allocations, while here we are factoring algebraic expressions to minimise floating-point operations. We plan to investigate more in detail the possible interplay/interference between these techniques.

The quest for optimal factorisations is central not only to Bayesian programming. In particular, these techniques can be applied to large fragments of \(\lambda \)-calculus, suggesting heuristics for making tractable the computation of the quantitative semantics of other classes of \(\lambda \)-terms than the one identified by \(\mathcal {L}\). This is of great interest in particular because these semantics are relevant in describing quantitative observational equivalences, as hinted for example by the full-abstraction results achieved in probabilistic programming, e.g.  [6, 13, 14].

Finally, while we have stressed that our work is theoretical, we do not mean to say that foundational understanding in general, and this work in particular, is irrelevant to the practice. Let us mention one such perspective. Factored inference is central to inference in graphical models, but scaling it up to the more complex problems expressible as probabilistic programs proves difficult—research in this direction is beginning, mainly guided by implementation techniques [21, 32, 40]. We believe that a foundational understanding of factorisation on the structure of the program—starting from the most elementary algorithms, as we do here— is also important to allow progress in this direction.

On dealing with evidence. We have focused on the computation of marginals, without explicitly treating posteriors. Our approach could easily be adapted to deal with evidence (hence, posteriors), by extending syntax and rewriting rules to include an observe construct as in [21] or in [16].