中文

Sequoidal 范畴与超限博弈:博弈语义中带状态对象的余代数方法

计算机科学中的逻辑 2017-06-02 v1

摘要

博弈上的非交换 sequoid 算子 \oslash 被引入以在代数上捕捉博弈语义中历史敏感策略的状态存在性,其方式是在博弈的张量积上施加因果关系。函子 A_A \oslash \_ 的余代数——即从 SSASA \oslash S 的态射——可被视为状态转换器:如果 A_A \oslash \_ 有一个终余代数 !A!A,那么此类状态转换器的变形将封装其显式状态,使其仅在连续调用之间共享。我们研究了 A_A \oslash \_ 的终余代数 !A!A 成为 AA 上余自由交换余单子载体的条件。也就是说,它是线性逻辑指数的模型,在其中我们可以在博弈语义环境中以余代数方式构造命令式对象(如引用单元)。我们证明,如果张量可分解为 sequoid,那么当存在从 !(A×B)!(A \times B)!A!B!A \otimes !B 的自然同构时,终余代数 !A!A 可被赋予余自由交换余单子的结构。如果 !A!AA_A \oslash \_ 的双自由代数,此条件总是满足,但通常必须施加此条件,我们通过给出一个 sequoidal 可分解博弈范畴的例子来证明这一点,在该范畴中允许博弈具有超限长度。在此范畴中,函子 A_A \oslash \_ 的终余代数不是 AA 上的余自由交换余单子:我们通过明确对比函子 A_A \oslash \_ 的终序列与 Melli\'es、Tabareau 和 Tasson 在构造作为极限的余自由交换余单子时所使用的对称张量幂链来阐明这一点。

关键词

引用

@article{arxiv.1706.00035,
  title  = {Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics},
  author = {William John Gowers and James Laird},
  journal= {arXiv preprint arXiv:1706.00035},
  year   = {2017}
}

备注

Accepted for publication in the proceedings of CALCO 2017, published in the Dagstuhl LIPIcs series. 15pp + 2pp bibliography + 12 pp Appendix (the appendix is not part of the conference version)