Full abstraction for non-deterministic and probabilistic extensions of PCF I: The angelic cases
Full abstraction for non-deterministic and probabilistic extensions of PCF I: The angelic cases
复制标题
DOI：
10.1016/j.jlamp.2014.09.003
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
J. Goubault-Larrecq
中科院分区：
文献类型：
--
作者：
J. Goubault-Larrecq
我们研究了Plotkin语言PCF的几个扩展和变体，包括非确定性和概率选择结构。对于每一个，我们给出了一个操作和指称语义，并比较它们。在每一种情况下，我们表现出健全性和计算充分性：两种语义计算相同的值在地面类型。除此之外，我们在许多情况下建立了完全抽象（观察前序与指称前序一致）。在概率情况下，这需要在语言中添加所谓的统计终止测试器。
We examine several extensions and variants of Plotkin's language PCF, including non-deterministic and probabilistic choice constructs. For each, we give an operational and a denotational semantics, and compare them. In each case, we show soundness and computational adequacy: the two semantics compute the same values at ground types. Beyond this, we establish full abstraction (the observational preorder coincides with the denotational preorder) in a number of cases. In the probabilistic cases, this requires the addition of so-called statistical termination testers to the language.