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.

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