一句话：提出类型导向的全局变换 Slice，将连续概率程序精确离散化，保持语义并赋能离散推断引擎。
本文研究面向递归高阶概率程序的精确离散化，将其视为一种保持语义的程序变换。目标程序中的连续值只与有限多个常数比较，因此精确推断可归约为离散问题。核心贡献是一种非局部的、类型导向的分析：它推断连续值可被划分为有限多个与观测相关的区域，并据此重写采样与比较行为，该变换称为 Slice。由于构造是全局且类型导向的，正确性不能仅靠局部语法推理；作者形式化了该变换，并在操作语义上通过耦合式逻辑关系论证，证明了其针对布尔查询的可靠性。应用层面，变换后的程序可由 Dice、Roulette、Storm 等离散引擎执行。实证评估显示 Slice 与离散后端结合具有两方面优势：一是能为先前精确系统难以处理的连续程序实现精确推断，二是在可直接比较的基准上与最先进的连续程序精确推断系统具有竞争力。
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.
@article{paperbot12077,
title = {Type-Directed Discretization of Probabilistic Programs},
author = {Katherine Wu and Jules Jacobs and Kevin Batz and Alexandra Silva},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839534}
}