Semantic Foundations for Laziness in Discrete Probabilistic Programming
summary
Claims that knowledge compilation and binary decision diagrams follow directly from a denotational semantics that splits sampling into two effects: name-generation vs reading. It builds a hybrid model by composing a name-allocation monad with a Reader monad, evaluates allocation call-by-value and reads call-by-name, and proves that for Reader monads call-by-name and call-by-value coincide. Implements BDD-style intermediate representations for translating distributions (used on Bottoscopia-style record types) and gives a correctness theorem against standard call-by-value semantics.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:56Botoscopia project context
- 3:39Probabilistic species representations
- 5:45Knowledge compilation evaluation
- 8:12Monadic semantics for names
- 10:18Summary and implications
- 10:40Q&A
related talks
49mSemantic Foundations for Probabilistic Programming
06mStatic Delayed Sampling for Probabilistic Programming Languages
17mLazy Knowledge Compilation for Discrete PPLs
05mNew foundations for probabilistic separation logic
19mPanel: Compilation Frameworks
14mAdequacy for Algebraic Effects Revisited
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
15mStable Relations and Abstract Interpretation of Higher-Order Programs