一句话:以事件结构统一刻画并发博弈与策略,构造双范畴并证明其紧致闭结构,为并发高阶计算提供语义基础。
本文详细、自包含地重述并小幅更新 Rideau 与 Winskel 2011 年提出的并发博弈与策略理论。作者将博弈和策略表示为事件结构,引入基于事件结构的预策略概念;刻画了哪些预策略(称为策略)在与 copycat 策略复合时保持不变;进而构造这些策略构成的双范畴。文章还证明相应范畴具有紧致闭结构,从而可作为并发高阶计算的语义基础。该工作属于理论语义研究,核心贡献是给出统一的事件结构框架、复合封闭性刻画以及范畴结构定理,而非经验评估。
In 2011, Rideau and Winskel introduced concurrent games and strategies as event structures, generalizing prior work on causal formulations of games. In this paper we give a detailed, self-contained and slightly-updated account of the results of Rideau and Winskel: a notion of pre-strategy based on event structures; a characterisation of those pre-strategies (deemed strategies) which are preserved by composition with a copycat strategy; and the construction of a bicategory of these strategies. Furthermore, we prove that the corresponding category has a compact closed structure, and hence forms the basis for the semantics of concurrent higher-order computation.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{CastellanCRW17,
title = {Games and Strategies as Event Structures},
author = {Simon Castellan and Pierre Clairambault and Silvain Rideau and Glynn Winskel},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:35)2017}
}