Infinite trace equivalence
Infinite trace equivalence
复制标题
无限痕量等价
DOI：
10.1016/j.apal.2007.10.007
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
P. Levy
中科院分区：
文献类型：
--
作者：
P. Levy
我们通过为非确定性程序提供一个指称模型来解决一个长期存在的问题，该模型可以识别两个程序，当且仅当它们具有相同的可能行为范围。我们讨论传统方法的困难，其中分歧是底部的或者术语表示来自一组环境的函数。我们发现，以游戏语义的方式明确强制可以让我们避免这些问题。我们首先对具有顺序 I/O 和无限非确定性的一阶语言进行建模（使用此方法建模并不比有限非确定性更难）。然后，我们通过采用标准游戏语义，将模型扩展到具有高阶和递归类型的微积分。使用逻辑关系的传统充分性证明不适用，因此我们使用新颖的隐藏和非隐藏论证。
We solve a longstanding problem by providing a denotational model for nondeterministic programs that identifies two programs iff they have the same range of possible behaviours. We discuss the difficulties with traditional approaches, where divergence is bottom or where a term denotes a function from a set of environments. We see that making forcing explicit, in the manner of game semantics, allows us to avoid these problems. We begin by modelling a first-order language with sequential I/O and unbounded nondeterminism (no harder to model, using this method, than finite nondeterminism). Then we extend the model to a calculus with higher-order and recursive types, by adapting standard game semantics. Traditional adequacy proofs using logical relations are not applicable, so we use instead a novel hiding and unhiding argument.