Statically Bounded-Memory Delayed Sampling for Probabilistic Streams
summary
Defines two dataflow conditions, m-consumed and unseparated path, and proves they are necessary and sufficient for delayed sampling to use bounded memory on streams (ProbZelus-style semantics). Builds a static analysis that abstracts program state and the delayed-sampling graph, proves the analysis is sound, and ships an implementation. Empirical run finds exact results on six benchmarks, flags two cases whose unbounded executions occur with probability zero, and reports one conservative false positive.
AI-written summary · about