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