The Variable Elimination Algorithm as a Let-Term Rewriting
summary
Expresses variable elimination for Bayesian networks as let-term linear lambda-calculus rewriting and proves any VE factorization is reachable by four simple rewrite rules (let-commute, functional commuting, let-merging, dead-variable elimination). Gives a constructive reduction strategy that transforms the naive global-product term into the memoized factorized form, and uses linear typing to show intermediate factors are typed as nested structures — values, finite distributions, stochastic matrices, and matrices-of-matrices — i.e. stochastic matrices of stochastic matrices.
AI-written summary · about
chapters (6)
- 0:00Variable elimination intro
- 5:49Motivation and research
- 10:24Lambda terms for factorization
- 13:44Rewriting rules
- 16:17Linear typing benefits
- 19:03Conclusion and future
related talks
19mCompiling Probabilistic Programs for Variable Elimination with Information Flow
30mThe Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi...
13mTowards Compiling Higher-Order Programs to Bayesian Networks
23mLet Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)
21mVerifying term graph optimizations using Isabelle/HOL
16mHigher Order Bayesian Networks, Exactly
59mUnification Modulo Equational Theories in Languages with Binding Operators
22mFrom Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs