We give a domain-theoretic semantics to a statistical programming language, using the plain old category of dcpos, in contrast to some more sophisticated recent proposals. Remarkably, our monad of minimal valuations is commutative, which allows for program transformations that permute the order of independent random draws, as one would expect. A similar property is not known for Jones and Plotkin' s monad of continuous valuations. Instead of working with true real numbers, we work with exact real arithmetic, providing a bridge towards possible implementations. (Implementations by themselves are not addressed here.) Rather remarkably, we show that restricting ourselves to minimal valuations does not restrict us much: all measures on the real line can be modeled by minimal valuations on the domain $\mathbf{I}\mathbb{R}_\bot$ of exact real arithmetic. We give three operational semantics for our language, and we show that they are all adequate with respect to the denotational semantics. We also explore quite a few examples in order to demonstrate that our semantics computes exactly as one would expect, and in order to debunk the myth that a semantics based on continuous maps would not be expressive enough to encode measures with non-compact support using only measures with compact support, or to encode measures via non-continuous density functions, for instance.
翻译:我们给统计编程语言提供了一种域论语义, 与最近一些更复杂的建议相反, 我们使用平坦的古老的 dcpos 类, 与一些更复杂的建议相反。 值得注意的是, 我们最起码的估价是通俗的, 从而可以按照人们的预期, 使独立随机抽取的顺序精确。 Jones 和 Plotkin 连续估价的月经没有类似的属性。 我们用真实的数字工作, 提供精确的准确的计算方法, 为可能的执行提供一座桥梁。 ( 执行本身没有在这里讨论。 ) 相反, 我们表明, 将自己限制在最低的估价上并不限制我们很多: 真正线上的所有措施都可以用最起码的估价来模拟, 以最精确的随机随机抽取的顺序。 我们给我们的语言提供了三种操作的语义性语义。 我们证明它们都足够尊重解析的语义学。 我们还探索了几个例子, 以证明我们的语义学结构的精细度是无法用一个精确的直截面的公式来支持。