Variable Elimination as Rewriting in a Linear Lambda Calculus

TL;DR

This paper models Variable Elimination, a key probabilistic inference algorithm, as a rewriting process within a linear lambda calculus, providing a novel program-based perspective on the algorithm.

Contribution

It introduces a new interpretation of Variable Elimination as a rewriting process in a linear lambda calculus, leveraging linear types for clarity.

Findings

Variable Elimination can be represented as term rewriting.

Linear types are essential for the rewriting process.

The approach offers a new perspective on probabilistic inference algorithms.

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 $\lambda$-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.