Variable Elimination as Rewriting in a Linear Lambda Calculus

TL;DR

The paper addresses exact inference for discrete probabilistic programs by reframing Variable Elimination as a rewriting on programs within a linear probabilistic $\lambda$-calculus. It introduces $\mathcal{L}$, a language with stochastic matrices and a rich let-term structure, and defines a rewriting system that localises eliminated variables while preserving semantics, yielding factorisations equivalent to standard $\mathsf{VE}$. It proves soundness and completeness of the term-rewriting VE ($\mathsf{VE}^{\mathcal{L}}$) with respect to the classical VE on factors ($\mathsf{VE}^{\mathsf F}$), and shows that any elimination order can be implemented by the rewrite, thereby unifying model specification and exact inference at the program level. The work integrates a denotational, cost-aware perspective, linking factorisation to resource usage and suggesting a foundation for cost-sensitive probabilistic programming and scalable exact inference on general-purpose stochastic languages.

Abstract

Variable Elimination (VE) is a classical exact inference algorithm for probabilistic graphical models such as Bayesian Networks, computing the marginal distribution of a subset of the random variables in the model. Our goal is to understand Variable Elimination as an algorithm acting on programs, here expressed in an idealized probabilistic functional language -- a linear simply-typed $λ$-calculus suffices for our purpose. Precisely, we express VE as a term rewriting process, which transforms a global definition of a variable into a local definition, by swapping and nesting let-in expressions. We exploit in an essential way linear types.

Figures (2)

• Figure 1: Example of running the $\mathsf{VE}$ algorithm on a let-term $\ell$.
• Figure 2: Typing rules: the binary rules suppose that the set of the free arrow variables of the subterms are disjoint; the let-rule binding an arrow variable $f$ requires also that this variable $f$ is free in the expression $e'$.