Semantics of Probabilistic Program Traces
This extended abstract presents a minimal core calculus modeling modern, trace-based PPLs–PPLs like Gen, ProbTorch, Pyro, and Turing in which probabilistic program traces are not just an implementation detail, but rather a user-facing data type, meant to be inspected and explicitly reasoned about. We show how to precisely define the distribution a program encodes over traces, and illustrate how to define and validate program transformations using the calculus (our example transformations are for computing trace densities and implementing weighted samplers). Our aim is to: (1) give theorists a self-contained model of a typical trace-based PPL, to facilitate discussions between implementors/users of such languages and PPL theorists; (2) give PPL developers a blueprint for formal reasoning about program semantics & new program transformations, and (3) provide a common reference point for discussion and comparison of many real-world PPLs.
|Semantics of Probabilistic Program Traces (lafi23-final97.pdf)