Deconstructing General References via Game Semantics
Deconstructing General References via Game Semantics
复制标题
通过游戏语义解构一般参考
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
N. Tzevelekos
中科院分区：
文献类型：
--
作者：
A. Murawski;N. Tzevelekos
我们通过 Abramsky、Honda 和 McCusker (AHM) 的完全抽象游戏模型研究了一般引用的游戏语义，该模型证明了游戏中的可见性条件对应于高阶引用相对于整数引用所提供的额外表达能力。
首先，我们通过将任何策略分解为可见策略和对应于单元→单元类型的参考单元的单个策略，证明了 AHM 可见因式分解结果的更强版本（AHM 仅考虑有限策略，其结果涉及无限多个单元）。
我们证明了该定理的强化版本意味着该模型的普遍性，因此，我们可以依靠它来提供程序转换结果的语义证明。特别是，可以证明任何具有通用引用的程序都等效于用单个单元→单元引用单元和单个整数单元增强的纯函数程序。我们还提出了一种实现这种转换的句法方法。
最后，我们提供了术语的类型理论表征，其中可以使用整数引用单元或通过纯函数计算来模拟一般引用的使用，而无需对底层类型进行任何更改。
We investigate the game semantics of general references through the fully abstract game model of Abramsky, Honda and McCusker (AHM), which demonstrated that the visibility condition in games corresponds to the extra expressivity afforded by higher-order references with respect to integer references.
First, we prove a stronger version of the visible factorisation result from AHM, by decomposing any strategy into a visible one and a single strategy corresponding to a reference cell of type unit→unit (AHM accounted only for finite strategies and its result involved unboundedly many cells).
We show that the strengthened version of the theorem implies universality of the model and, consequently, we can rely upon it to provide semantic proofs of program transformation results. In particular, one can prove that any program with general references is equivalent to a purely functional program augmented with a single unit→unit reference cell and a single integer cell. We also propose a syntactic method of achieving such a transformation.
Finally, we provide a type-theoretic characterisation of terms in which the use of general references can be simulated with an integer reference cell or through purely functional computation, without any changes to the underlying types.