paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Categorical combinatorics of scheduling and synchronization in game semantics

博弈语义中调度与同步的范畴组合学
POPL 3(POPL)2019匹配度 1/10 · 论文属于博弈语义与范畴组合学的基础形式语义工作,关注调度/同步策略的可组合性,与用户画像中的静态分析、Agentic/LLM、浮点程序分析与贝叶斯程序分析均无直接关联,仅在广义程序语义与并发理论上有非常微弱的联系。引用 12 inbox
Paul-André Mellies
crossref: 2026-09-10

AI 速览

一句话:提出用同步模板与范畴组合学统一刻画博弈语义中可组合的调度策略,并构造交替与非交替线性逻辑博弈模型。

论文研究博弈语义中一个长期问题:给定调度策略为何能保证策略正确同步并在组合时保持可组合性。作者将调度策略编码为同步模板,利用范畴组合学和小范畴范畴,提炼若干基本组合结构,证明这类模板可定义游戏、策略与模拟的对称幺半闭(乃至星自治)双范畴。方法结合进程演算中的同步代数与博弈语义、范畴代数。作为示例,作者用同一套范畴构造给出线性逻辑的两种模板博弈模型:交替式与非交替式,从而说明统一框架可覆盖顺序与并发语言的调度行为。

问题
研究博弈语义中调度策略何时以及为何能保证策略正确同步、并在组合时保持可组合性;顺序语言通常要求严格交替,并发语言则允许非交替。
方法
将调度策略编码为同步模板,借助范畴组合学、小范畴及进程演算中的同步代数,构造游戏、策略与模拟的双范畴语义框架,并给出线性逻辑的交替与非交替模板模型。
评估
通过构造两个具体模板博弈模型(交替式与非交替式)展示同一范畴组合学可用于不同风格的线性逻辑模型,以论证框架的普遍性与可组合性。
原文摘要(Abstract)

Game semantics is the art of interpreting types as games and programs as strategies interacting in space and time with their environment. In order to reflect the interactive behavior of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) will play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent will be allowed to play several moves in a row, in a non-alternating way. In both cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronize properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this paper, we exhibit a number of simple and fundamental combinatorial structures which ensure that a given scheduling policy encoded as synchronization template defines a symmetric monoidal closed (and in fact star-autonomous) bicategory of games, strategies and simulations. To that purpose, we choose to work at a very general level, and illustrate our method by constructing two template game models of linear logic with different flavors (alternating and non-alternating) using the same categorical combinatorics, performed in the category of small categories. As a whole, the paper may be seen as a hymn in praise of synchronization, building on the notion of synchronization algebra in process calculi and adapting it smoothly to programming language semantics, using a combination of ideas at the converging point of game semantics and of categorical algebra.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot662,
  title = {Categorical combinatorics of scheduling and synchronization in game semantics},
  author = {Paul-André Mellies},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3290336}
}