Bayesian inference in probabilistic programs requires searching the space of possible program executions to find those that make observations likely. Many Monte Carlo algorithms explore this space iteratively, repeatedly sampling modifications from a proposal distribution and reevaluating the program’s likelihood under the proposed changes. As full recomputation is expensive, many probabilistic programming systems implement some form of incremental density computation that reuses intermediate results from previous evaluations whenever possible.

In systems that support programmable inference, user-provided proposal distributions can generate complex changes to the execution traces of probabilistic programs. In this work, we present a new, modular approach to addressing two key challenges in this setting. First, we propose a general way of representing changes to a model’s execution, by computing trace types for a user’s program, and then applying type-directed rules, inspired by the incremental λ-calculus, to define a space of changes to the program’s traces. Second, we develop a two-step program transformation that first compiles the user’s probabilistic program into a deterministic density program, and then incrementalizes this deterministic density.

This approach decouples probabilistic programming concerns from incrementalization, enabling easier formal reasoning about correctness, and preliminary results show it supports efficient Monte Carlo inference.