Search papers, labs, and topics across Lattice.
This paper introduces a semantics-preserving transformation called Slice for recursive, higher-order probabilistic programs that utilize continuous distributions, enabling exact discretization. By employing a non-local, type-directed analysis, the authors identify partitions of continuous values into finitely many observationally relevant regions, allowing for the rewriting of sampling and comparison behaviors. The empirical results demonstrate that Slice not only facilitates exact inference for complex continuous programs but also competes effectively with existing state-of-the-art exact inference systems when benchmarked against them.
Slice transforms continuous probabilistic programs into discrete forms, enabling exact inference where previous methods fail.
We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where continuous values are compared against finitely many constants, so exact inference reduces to a discrete problem. Our central technical contribution is a non-local, type-directed analysis that infers where continuous values can be partitioned into finitely many observationally relevant regions, then rewrites sampling and comparison behavior over those regions. We call this transformation Slice. Because this construction is global and type-directed, correctness requires reasoning beyond the local syntax: we formalize the transformation and prove soundness for boolean queries using a coupling-style logical relations argument over operational semantics. As an application, transformed programs can be executed by discrete engines such as Dice, Roulette, and Storm. Our empirical evaluation shows two complementary strengths of Slice when paired with discrete backends: it enables exact inference for challenging continuous programs that lie beyond the reach of previous exact systems, and, on benchmarks where direct comparison is possible, it is competitive with state-of-the-art exact inference systems for continuous programs.
