具有对称性的薄博弈与并发 Hyland-Ong 博弈
计算机科学中的逻辑
2023-06-22 v5 逻辑
摘要
我们基于事件结构构建了一个笛卡尔闭范畴，称为 Cho。它允许对高阶状态并发程序进行更精细和精确的解释：一方面，在将纯函数式程序解释为无辜策略时，它相对于标准的 Hyland-Ong 博弈是保守的；另一方面，它具有更强的表达能力。程序的解释以组合方式构建了其执行的表示，展示了因果依赖关系并记住了非确定性分支点。该构建分为两个阶段。首先，我们构建了一个紧致闭范畴 Tcg。它是 Rideau 和 Winskel 的范畴 CG 的一个变体，不同之处在于 Tcg 中的博弈和策略配备了对称性，以表达某些事件本质上是相同的。这类似于 AJM 博弈的基础范畴用玩法规则上的等价关系丰富简单博弈。基于此范畴，我们构建了笛卡尔闭范畴 Cho，其对象为标准的 Hyland-Ong 博弈竞技场，策略由某些事件结构表示，并在作为这些竞技场展开形式的具有对称性的博弈上进行。为了说明这些构建并赋予其操作层面的直观理解，我们在 Cho 中解释了（理想化并行 Algol 的一个紧密变体）。
引用
@article{arxiv.1409.7542,
title = {Thin Games with Symmetry and Concurrent Hyland-Ong Games},
author = {Simon Castellan and Pierre Clairambault and Glynn Winskel},
journal= {arXiv preprint arXiv:1409.7542},
year = {2023}
}