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.

翻译：同步语言如今已成为关键嵌入式系统的标准工业工具。设计者通过块图组合数值流来编写高层规格说明。这些语言已扩展了贝叶斯推理功能，可用于对状态空间模型进行编程——该模型根据观测流计算分布流。然而，概率模型的语义仅适用于已排序的方程——相比无需任何排序的数据流同步语言和块图，这一限制颇为显著。本文针对一种概率同步语言提出了两种与排序无关的语义。关键思想是将概率表达式解释为未归一化的密度函数流，该函数将随机变量值映射为结果与正得分。余迭代语义将程序解释为状态机，并通过不动点算子计算方程。关系语义直接操作流，因此更适合用于推理程序等价性。我们利用关系语义证明了一种程序变换的正确性——该变换旨在对具有恒定参数的状态空间模型运行优化推理算法。