Game semantics and linear CPS interpretation
Game semantics and linear CPS interpretation
复制标题
游戏语义和线性 CPS 解释
DOI：
10.1016/j.tcs.2004.10.022
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Laird
中科院分区：
文献类型：
--
作者：
J. Laird
我们提出了一个基于博弈语义的函数式语言的“线性使用延续传递解释”的语义分析。这包括一个具有连贯性条件的游戏类别——产生一个仿射型理论的完全完整模型——以及一个独立于语法并完全嵌入Hyland-Ong / nickau风格的“良好括号”游戏类别。我们表明，这种嵌入在其对按值调用PCF的游戏模型的作用中精确地对应于线性CPS解释，从而为相关翻译提供了完全抽象的证明。我们讨论了语义的扩展，以处理递归类型、按名称调用求值、非局部跳转和状态。
We present a semantic analysis of the “linearly used continuation-passing interpretation” of functional languages, based on game semantics. This consists of a category of games with a coherence condition on moves—yielding a fully complete model of an affine-type theory—and a syntax-independent and full embedding of a category of Hyland–Ong/Nickau-style “well-bracketed” games into it. We show that this embedding corresponds precisely to linear CPS interpretation in its action on a games model of call-by-value PCF, yielding a proof of full abstraction for the associated translation. We discuss extensions of the semantics to deal with recursive types, call-by-name evaluation, non-local jumps, and state.