Schedule Agnostic Semantics for Reactive Probabilistic Programming

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 recently extended with Bayesian reasoning to program state-space models which compute a stream of distributions given a stream of observations. Yet, the semantics of probabilistic models is only defined for scheduled equations—a significant limitation compared to dataflow synchronous languages and block diagrams.

In this article we propose a new operational semantics and a new denotational semantics for a probabilistic synchronous language that are both schedule agnostic. The key idea is to externalize the source of randomness and interpret a probabilistic expression as a stream of functions mapping random elements to a value and positive score. The operational semantics interprets expressions as state machines where mutually recursive equations are evaluated using a fixpoint operator. The denotational semantics directly manipulates streams and is thus a better fit to reason about program equivalence. We use the denotational semantics to prove the correctness of a program transformation required to run an optimized inference algorithm for state-space models with constant parameters.