论文标题
分类代数的基础游戏语义
Grounding Game Semantics in Categorical Algebra
论文作者
论文摘要
我提出了代数效应和游戏语义之间的正式联系，这是编程语言语义上的两种重要作品，并在组成软件验证中进行了应用。 具体而言，可以将计算可能副作用的代数签名列为游戏，并且该游戏的策略构成了完全部分订单（CPO）类别的签名的自由代数。因此，策略提供了一种方便的计算模型，并具有未解释的副作用。特别是，游戏语义的运行味道以最初代数和CPO内膜末端界面之间的巧合形式延续到代数环境。 相反，代数的观点为游戏语义的策略构造提供了新的启示。策略模型可以作为部分策略树（代数术语中的免费DCPO）的理想完成。将框架扩展到多组签名将使该构建可用于大型游戏。
I present a formal connection between algebraic effects and game semantics, two important lines of work in programming languages semantics with applications in compositional software verification. Specifically, the algebraic signature enumerating the possible side-effects of a computation can be read as a game, and strategies for this game constitute the free algebra for the signature in a category of complete partial orders (cpos). Hence, strategies provide a convenient model of computations with uninterpreted side-effects. In particular, the operational flavor of game semantics carries over to the algebraic context, in the form of the coincidence between the initial algebras and the terminal coalgebras of cpo endofunctors. Conversely, the algebraic point of view sheds new light on the strategy constructions underlying game semantics. Strategy models can be reformulated as ideal completions of partial strategy trees (free dcpos on the term algebra). Extending the framework to multi-sorted signatures would make this construction available for a large class of games.
