Density-Based Semantics for Reactive Probabilistic Programming

TL;DR

This paper introduces two schedule-agnostic semantics for reactive probabilistic programming languages, enabling more flexible reasoning and optimization of probabilistic models without requiring explicit execution order.

Contribution

It proposes novel semantics that interpret probabilistic expressions as density streams, allowing for schedule independence and improved reasoning about program equivalence.

Findings

Proposed semantics are proven correct for program transformations.

The relational semantics facilitate reasoning about program equivalence.

The approach supports optimized inference algorithms for state-space models.

Abstract

Synchronous languages are now a standard industry tool for critical embedded systems. Designers write high-level specifications by composing streams of values using block diagrams. These languages have been extended with Bayesian reasoning to program state-space models which compute a stream of distributions given a stream of observations. However, the semantics of probabilistic models is only defined for scheduled equations -- a significant limitation compared to dataflow synchronous languages and block diagrams which do not require any ordering. In this paper we propose two schedule agnostic semantics for a probabilistic synchronous language. The key idea is to interpret probabilistic expressions as a stream of un-normalized density functions which maps random variable values to a result and positive score. The co-iterative semantics interprets programs as state machines and equations are computed using a fixpoint operator. The relational semantics directly manipulates streams and is thus a better fit to reason about program equivalence. We use the relational semantics to prove the correctness of a program transformation required to run an optimized inference algorithm for state-space models with constant parameters.