Higher Order Bayesian Networks, Exactly
summary
A higher-order lambda-calculus is defined that is sound and complete for Bayesian networks: every Bayesian network encodes as a term and every well-typed ground-term compiles to a first-order Bayesian network normal form, including recursive and hierarchical models. Types are intersection types tracking generated random-variable names, semantics uses factors so probability computation mirrors variable-elimination, and a call-by-push-value calculus controls sharing versus copying of samples; extraction from type derivations yields graph structure and a static cost measure for inference.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 3:39Limitations of first-order BNs
- 5:23Higher-order probabilistic models
- 7:08Type system and semantics
- 10:01Technical foundations
- 12:31Main contributions
- 13:14Q&A
related talks
13mTowards Compiling Higher-Order Programs to Bayesian Networks
04mSeparated and Shared Effects in Higher-Order Languages
15mStable Relations and Abstract Interpretation of Higher-Order Programs
24mTowards a Higher-Order Mathematical Operational Semantics
27mHigher-Order Behavioural Conformances via Fibrations
49mSemantic Foundations for Probabilistic Programming
19mThe Variable Elimination Algorithm as a Let-Term Rewriting
17mλKanren: Higher-order Logic Programming with Shallow Embedding