paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Qualitative Collapse of Concurrent Games

并发博弈的定性坍缩
LICS 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2025匹配度 1/10 · 论文研究并发博弈到 Scott 域的定性坍缩,属于纯形式语义/域理论,与用户关注的 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析等方向没有直接关联。引用 0 inbox
Pierre Clairambault
crossref: 2026-09-12

AI 速览

一句话:构造从并发博弈到 Scott 域的保解释函子,给出定性模型提取定量信息的组合描述,并重证 Ehrhard 定性-定量对应。

本文研究并发博弈语义与 Scott 域语义之间的定量—定性联系。已有工作给出了博弈语义的关系坍缩,而 Ehrhard 的外延坍缩定理虽建立了定性—定量对应,却依赖抽象的 realizability 构造,缺少具体组合解释。作者构造了一个从并发博弈范畴到 Scott 域与 Scott 连续函数范畴的保解释函子,并给出其具体描述;核心是一个精细的组合引理,用于同步涉及相同资源但重数不同的策略状态。将该函子与已有的关系坍缩结合,作者重新证明了 Ehrhard 的定性—定量对应,并为从定性模型提取定量信息提供了具体、组合式的描述。

问题
如何将并发博弈的定性语义模型与 Scott 域上的定量信息具体联系起来,并给出比 Ehrhard 抽象 realizability 构造更直接的定性—定量对应证明。
方法
构造从并发博弈范畴到 Scott 域及 Scott 连续函数范畴的保解释函子;借助组合引理同步相同资源但不同重数的策略状态,并与关系坍缩结合。
评估
以范畴论与组合论证证明函子的保解释性,基于该构造重新证明 Ehrhard 的定性—定量对应定理;属理论证明,无实验评估。
原文摘要(Abstract)

We construct an interpretation-preserving functor from a category of concurrent games to the category of Scott domains and Scott-continuous functions. We give a concrete description of this functor, extending earlier results on the relational collapse of game semantics. The crux is an intricate combinatorial lemma allowing us to synchronize states of strategies which involve the same resources, but with different multiplicity.Putting this together with the previously established relational collapse, this provides a new proof of the qualitative-quantitative correspondence first established by Ehrhard in his celebrated extensional collapse theorem. Whereas Ehrhard’s proof is indirect and rests on an abstract realizability construction, our result gives a concrete, combinatorial description of the extraction of quantitative information from a qualitative model.

链接与引用

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

BibTeX
@inproceedings{paperbot8679,
  title = {The Qualitative Collapse of Concurrent Games},
  author = {Pierre Clairambault},
  booktitle = {LICS},
  year = {2025},
  doi = {10.1109/lics65433.2025.00045}
}