具有对称性的并发博弈的定量坍缩

我们探索 Castellan、Clairambault 和 Winskel 的瘦并发博弈与 Laird、Manzonetto、McCusker 和 Pagani 所研究的线性逻辑加权关系模型之间的联系。更确切地说，我们证明从前者到后者存在一个保持解释的“坍缩”函子。在对象上，该函子为每个博弈定义一组可能的执行状态。在态射上定义作用更为微妙，这是本文的主要贡献。给定一个策略与一个执行状态，我们的函子需要计数该策略中此状态的见证。瘦并发博弈中的策略显式描述非线性行为，因此一般地每个见证存在于可数无穷多个对称副本中。挑战在于定义恰当的见证概念，在消去此无穷性的同时匹配加权关系模型。理解见证如何复合尤为微妙，需要深入见证及其对称性的组合学。在其基本形式中，该函子连接瘦并发博弈与由 N $\cup$ {+$\infty$} 加权的关模型。我们还将考虑一个推广设定，其中两个模型均由任意连续半环的元素加权；这涵盖了概率情形等。见证现在额外携带来自半环的一个值，且我们的保持解释的坍缩函子推广至该设定。