对话博弈与图博弈在计算机科学中的关系和应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记336（2018）189-206www.elsevier.com/locate/entcs关于对话博弈和图博弈Cl'ementJacqPaul-Andr'eMelli`es在数据库中，数据库管理系统（IRIF）、CNRS、UniVSit ititeParisDiderot摘要DialoguegameswerereintreducedbyyMelliiesanattemtttounifyytwohistoricalparadigmsofgamee-mantics：concrete data structures and arena games. 对话游戏的定义依赖于竞技场游戏的移动m可以分解为由单元α和值v组成的对m=（α，v）的想法。因此，一个对话游戏被定义为一个四分森林，其节点被分为四类：对手单元，对手值，玩家单元，玩家值。 虽然从竞技场游戏到对话游戏的转换本质上是直接的，但对话游戏与具体数据结构之间的关系更为复杂。为了澄清这一点，我们研究了Hyland和Schalk提出的对话游戏和图游戏之间的关系，为Berry和Curien的序列算法模型提供了一个图论解释。我们构造了一个完全忠实的函子，从对话游戏的范畴到图游戏和无冲突策略的范畴。这导致我们将图游戏中的无冲突策略定义为对话游戏中的平衡和双不变策略。保留字：游戏语义学，竞技场游戏介绍Didentical game的概念是由Melli`esin[14]（Chapter4，Section4）生成的，以便用有限和直接描述张量逻辑的公式A，B，A，B：= <$A|A组B组 |A组B组|A ⊕ B | 0模以下方程：和张量的结合性和交换性，0和1的酉性，张量积在有限和上的分配性（asymmetry）（AB）C=A（BC）（AB）C=A（BC）（单位）A =AA=A（dist）A（BC）=（AB）（AC）A= 0（）AB=BAAB=BA由ludics[3]和极化线性逻辑[8]启发的关键观察是，有限对话游戏与此类公式的等价类是同一回事。人们以这种方式建立了一个连贯性定理，它是自由对话的https://doi.org/10.1016/j.entcs.2018.03.0231571-0661/© 2018由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。190C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189一个给定类别C生成的有限和的类别作为对话游戏和无辜策略的特定类别，详见[14]（其中细化[13]）。对话游戏的一个主要新颖之处在于，游戏的移动m不是被视为原子的：它们被分解为由单元α和值v组成的对m=（α，v）。这意味着对话游戏的每一步m都被识别为用特定值v“填充”特定单元格α的动作因此，对话游戏的每个单元格和每个值都被分配一个极性玩家或对手。因此，对手移动m=（α，v）的目的是用对手值v填充对手单元α，而玩家移动n=（β，w）的目的是用玩家值w填充玩家单元β。将对话游戏的每一步m分解为一对m=（α，v）的想法来自于以下证明理论观察：给定一个带和的张量逻辑公式A，在相关对话游戏A的单元α和规范的张量否定X<$→ <$X之间式A的形式。所谓标准形，我们指的是从A得到的公式通过从左到右定向等式（dist）和（unit）。通过举例说明，布尔博弈B被定义为双重否定图1示出了具有两个玩家值真和假的对话游戏1的游戏1的游戏1的游戏1的游戏1（1）。根据上面观察到的胞元和张量否定之间的对应关系，博弈B有两个胞元：根上的对手胞元α对应于外部否定，而参与者胞元β对应于内部否定：αβ=<$<$（1 1）因此，对手通过移动q=（α，q）开始游戏，该移动用值q填充单元格α。这个Opponent值q恰好代表了Player单元格β。这使得玩家能够通过使用移动n =（β，v）来对对手的移动q做出反应，该移动在[ 14 ]中采用了“单元”和“值”的术语这个术语的选择反映了我们希望将对话游戏与Berry和Curien设计的顺序算法模型统一起来，也是基于具体的数据结构，详见[1]。本文的目的正是要探讨这一点。与其使用模型的原始公式，我们发现从Curien和Lamarche基于Filiform具体数据结构的重新公式开始是方便的与对话游戏的比较将我们带到了15年前由Hyland和Schalk开发的图形游戏的研究中[6，15]。这导致我们比较下面的三个游戏模型：• 顺序数据结构• 图游戏• 对话游戏为了将对话游戏与图形游戏联系起来，我们需要驯服通常的BC. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189191异步轨迹的对话游戏，并限制他们的特定类别的轨迹，称为平衡轨迹。这些平衡轨迹反映了序列数据结构和图形游戏轨迹所需的隐含正如我们将看到的，约束是在对话中形成的游戏作为轨迹上的位置支付条件，详见§3。我们骗-以这种方式构建了一个对话类DG的对话游戏和平衡策略。本文的一个主要观察是，存在着一对等价关系的平衡轨迹之间的对话游戏，对于张量逻辑的公式A，详见§4。这对等价关系-tions的灵感来自于[12]中用于描述异步博弈中无辜策略和反策略的对手-玩家和玩家-对手排列BLOOP和BLOPO有点令人惊讶的是，我们建立（Prop. 4.4），这两个等价物是由一些原子排列瓦片的formsOP t和sPOt生成的。由于在一系列移动中置换了两个对手移动m1、m2和两个玩家移动n1、n2的顺序，因此，s=m1·u·n1·m2·v·n2Pt=m2·u·n2·m1·v·n1偶数长度，其中u，v是偶数长度的移动序列。类似地，每一个移动瓦片的移动P O也可以在移动序列中移动m1、m2和两个玩家移动n1、n2的两个操作点的顺序。s=n1·u·m1·n2·v·m2P Ot=n2·u·m2·n1·v·m1偶数长度，其中u，v是偶数长度的移动序列。典型地，每个Per_rm_til_s_OP_t都在下面的代码中被定义：（一）因此，在顺序算法理论的核心，我们可以将两类可分割的块S-P和D-P-O的最小化算法恢复到异步无罪理论中所涉及的2-D的最小化算法[12，14]。关键的区别在于，在无罪的异步定义中，两个移动序列u，v是空的，OP-置换瓦片的形式是s= m1·n1·m2·n2Pm2·n2·m1·n1= t.从图形游戏转变为对话游戏的一个好处是，相同的移动序列u描述了原子瓦片图（1）中的两个不同轨迹，移动序列v也是如此。因此，两个平衡的轨迹是通过自动化来实现的，直到通过自动化来实现自动化n1M2uvM1n2M2n1un2vM1192C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189tileso c k e t Otplayyxachty theamemo movein thediallogggame，but inadifficult order.（tile socketOtpl ayy xachty theamemo move in the dial logggame，但不按顺序移动。）换句话说，两个轨迹s，t是等价的模对话游戏的通常置换关系，见[12，13，14]。为了阐明对话博弈与图博弈的关系，定义了对话博弈中的无冲突策略概念，并构造了一个DGbal−→ GGG的函子对话游戏和平衡无冲突策略，到图的GG类游戏的定义[6，15]。本文的一个主要结果是函子G是完全忠实的。这使我们能够将张量层次的每个图博弈G（A这一结果揭示了Hyland-Schalk图游戏的组合结构，以及它们被原子秘密调节的事实。Permu tation tilespueroPanddpueroP O.纸的计划。在§ 1中回顾了对话游戏的定义以及§ 2中它们与张量逻辑的关系之后，我们在§ 3中构建了一个对话游戏和平衡策略的对话范畴DG。我们在§ 4中分析了这两种排列在一个对话游戏中，轨迹之间的PINOP和PINPO，并表明它们是由一个简单的PINOP和PINPO生成的。在回顾了Hyland-Schalk[6]关于图博弈和预策略的定义之后，我们在[6]中构造了一个面向对话的图博弈和面向对话的图博弈的范畴DG类，并证明了它完全忠实地（作为一个对话范畴）嵌入到图博弈的范畴GG中. 最后，我们在§7中建立了一个双不变性定理。1对话游戏在本节中，我们回顾了[14]中对对话游戏的定义。定义1.1有根对话游戏是一个有限的二部有根树，其节点被分成两组单元和值。我们注意到父节点和子节点之间的关系。通过二分树，我们的意思是d单元格×值+值×单元格。这意味着值的子级是单元格，而单元格的子级是值。一款有根的对话游戏，配备了极性功能λ：CellsValues→ {−1，1}，对于αa cell和va value，我们有：αdv<$λ（α）=λ（v）v d α<$λ（α）= −λ（v）最后，有根对话游戏的根是极性值+1。按照惯例，我们将玩家称为具有正极性的节点，将对手称为具有正极性的节点。一个负的节点。 我们可以说一个有根的对话游戏是四方的C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189193其分支以如下方式交替：球员值d对手单元格d对手值d球员单元格d球员值.定义1.2一个对话游戏A是一个家庭（A i|i∈I）的有限集合I索引的有根对话游戏。它可以被看作是一个森林，其连接组件是根对话游戏Ai。我们把A的根的集合记为根A。注意，对话游戏A =（A i）的每个根∈根A|i∈I）是一个Player值，并且在根A和A的有根分量的集合I之间存在一一对应。这里的基本直觉是，我们将对话游戏视为Berry和Curien的具体数据结构的游戏语义扩展，我们通过将单元和值分配给不同的玩家来对称这些结构。接下来，我们将介绍用于模拟在游戏中一次只能用一个值我们在根树的节点上取通常的顺序关系，并写a≤b，当a是b的祖先，而a/b是a和b的最大共同祖先。我们定义了以下兼容性概念：定义1.3当a和b是一个值时，两个节点a和b被称为兼容的。否则它们被称为不相容直觉上，兼容节点代表并发选择，我们可以选择一个节点，然后回溯并尝试另一个节点，而不兼容节点代表一个确定的选择：如果我们选择一个节点，其他分支在当前的探索中永远丢失。定义1.4有根对话博弈A的位置是A的两两相容值的非空下闭集x：• n v，w ∈值，v ≤ w且w ∈ x v∈x• n ∈ v，w ∈值，v ∈ x和w ∈ x 与w兼容的一个对话游戏的位置A =（A i|i∈I）是森林A的两两相容值的非空下闭集合w，恰好存在于对话博弈的一个有根分量A i中。我们把Pos（A）写为对话游戏A的位置集合。定义1.5有根对话博弈A的一步棋是一对（α，v），由一个单元α和一个值v组成，使得αd v。我们把A的步数集写成步数A。定义1.6有根对话游戏A的位置图图A是一个图，其顶点是A的位置，其边是A的移动，使得对于两个位置x和y以及移动（α，v），我们有（α，v）：x→y当且仅当y=x{v}。 对话游戏A =（A i）的位置图|i ∈ I）是有根对话游戏A i的图的不交和。定义1.7有根对话游戏A的轨迹s：x→y是图A中位置x和y之间的路径。因此，它可以被看作是一系列的动作，194C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189曲霉一个轨迹s：n→x从一个有根对话游戏A的根节点开始，在对手和玩家之间交替移动，被称为该游戏的一次游戏。我们为A的一组剧本写剧本A。定义1.8有根对话博弈A的参与者策略σ是一组偶数长度的策略，使得：• σ包含空场，• σ是由偶数长度前缀封闭的，在这个意义上，s∈策略A，• σ是决定性的，在这个意义上，s ∈棋A，m，n1，n2∈移动A，s·m·n1∈ σ，s·m·n2∈ σ <$n1= n2.2对话博弈与张量逻辑正如在引言中所解释的，对话游戏的概念已经在[14]中引入（作为[13]的修订），因为它与张量逻辑的公式一一对应。我们现在解释对话游戏和这些公式之间的对应关系，并在本节的最后制定了反策略的概念，这将使我们能够构建我们的对话游戏类别。首先，对话游戏0被定义为一个空的有根对话游戏族;而有根对话游戏1被定义为没有单元格的游戏和一个定义其根的唯一值。两个对话游戏的和A<$BA=（Ai|i∈I）且B=（B j|j∈J）定义为不相交的并集AB =（C k|k∈I J），其中对于i∈ I，Ci = Ai，对于j ∈ J，Cj= Bj. 注意，求和是结合的，并且每个对话游戏A =（A i|i∈I）是有限个有根对话游戏Ai的和。还要注意的是，来自和的不同博弈的两个节点必然是不兼容的，因为它们没有共同的祖先。 因此，A和B中的游戏要么是A中的游戏，要么是B中的游戏。 与对话游戏A相关联的有根对话游戏<$A =（A i|i∈I）的定义是通过反转A i的每个有根对话游戏的极性，然后添加一个根值α，该根值α证明了一个细胞α，该细胞α证明了有根对话游戏A i的每个根α i。因此，否定改变了这个对话游戏：*i*m*一个C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189195opopop*一个*i*mα*αβ*Aγ*Bαβγ*在对话游戏中：在这里，我们将Player值描述为浅蓝色的圆盘，Opponent值描述为暗红色的圆盘，单元格描述为白色的节点。两个有根对话游戏A和B的张量积是通过将根值A和B合并为单个根值来定义的有根对话游戏。通过说明，两个根深蒂固的对话游戏通过以下操作将它们转换为张量积A<$B两个对话游戏的张量积A =（A i|i∈I）且B =（B j|j∈J）则定义为对话游戏A<$B=（A i<$B j|（i，j）∈I×J），其组件是刚才定义的有根对话游戏A i<$B j。当我们需要将来自A的值与来自B的值分开时，我们偶尔会注意到A → B的位置x = y。 对话游戏与张量逻辑公式的对应性来自于每个对话游戏A =（Ai|i∈I）可以分解为有根博弈A i的和，并且每个有根博弈A i都是有限个否定对话博弈<$B ij的张量积。每一对对话游戏A和B都定义了一个有根对话游戏A−·B，其公式如下：αβA−·B=B）其中我们用α和β标记两个张量否定，以指示相关细胞的名称为了定义各种类型的对话游戏，我们196C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189B B−·第一步O第二步，P第三步O第四步，PB BQQQQ我将在对话博弈A-·B中使用横向策略的概念。定义2.1A−·B上的策略称为横向策略，当（α，val）·（β，wal）∈σ.因此，A−·B的策略σ是横向的，当它对对手的每个初始移动（α，val）做出反应时，对于一个值val∈根A，通过一个形式为（β，wal）的移动，对于一个值wal∈根B，在对话博弈A−·B的分量<$B中进行=<$（A <$<$B）而不是分量A。3对话游戏和平衡策略在本节中，我们将介绍对话游戏中的平衡位置和平衡轨迹的概念。我们在第3.1节中描述了头寸的支付条件，它在平衡的策略和轨迹上强制执行适当的“转换条件”。然后，我们在第3.2节中解释了如何以对话游戏为对象，以平衡策略为态射来构造对话范畴DG。3.1平衡的位置和轨迹对话游戏和顺序数据结构（或简单游戏）之间的一个主要差异取决于两个框架中定义轨迹的方式。特别是，在对话博弈A和B中，博弈s的全局定义意味着：其限制S|A和s|B到子组件A和B的关系不再需要在对手和玩家之间交替。提供了一个典型的例子通过对话游戏的玩法（B<$B）−·（B<$B）=<$（B<$B<$$><$（B<$B）），其特征在于它的四个移动序列如下：这条轨迹很有趣，因为它是由模仿策略idB B B B所执行在对话游戏和创新的类别中与对话游戏B在[13，14]中制定的三分之一战略。为了禁止这种行为，我们引入了平衡位置和平衡轨迹的概念。一种简单C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189197简洁的方式启发[11，10]来定义它们是装备每一个对话游戏A带支付功能κ：Pos（A）→ {+1，-1，fail}payo会给对话游戏的每一个位置分配一个值+1、-1或失败。 其思想是，每一个支付为0.001的位置都是玩家的胜利，因此对手有权从它开始走一步;对称地，支付为0.001的位置是对手的胜利，因此玩家有权从它开始走一步。支付为0.001的位置是不平衡的，因为任何平衡的打法都无法到达它们。定义3.1与对话游戏A相关联的支付函数κ：Pos（A）→ {+1，-1，fail}由张量逻辑的基本公式A上的结构• 对话游戏1的单个根具有+1的payo• 当对话游戏A的位置x在根处时，该位置x的支付额为+1，否则为对话游戏A中该位置x的支付额的倒数，• 对话游戏A的A或B部分中的位置的支付点是其在其部分中的支付点，• 张量积AB的位置xy的payo使用以下payo表计算：κ（y）=+1κ（y）=−1κ（y）=未通过κ（x）=+1+1个−1失败κ（x）=−1−1失败失败κ（x）=失败失败失败失败因此，当两个位置x和y具有负的支付时，对话游戏A <$B中的位置x <$y是不平衡的，κ（x）= κ（y）= −1。原因是，一个到达这样一个位置x y的打法s：→ xy需要在某个点上连续走两步对手棋。还需要注意的是，对话博弈A的根博弈总是正的支付+1。最后，在{+1，-1，fail}中的支付的逆定义为预期，而fail的逆定义为自身。这个定义为对话博弈A −·B导出了一个支付表，它计算了对话博弈A−·B的位置x−·y的支付，给定A中位置x的支付κ（x）和B中位置y的支付κ（y）：κ（y）=+1κ（y）=−1κ（y）=未通过κ（x）=+1+1个−1失败κ（x）=−1失败+1个失败κ（x）=失败失败失败失败198C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189定义3.2对话游戏A的轨迹s：x1→x2→···→xn称为当所有的位置xi都是平衡的，对于1≤i≤n。定义3.3对话游戏A的平衡策略s：n→x是从游戏的根节点开始的平衡轨迹。我们为平衡策略集写BalA我们建立了以下性质，它表征了对话游戏A的一般异步游戏中的平衡游戏：命题3.4在有根对话博弈A中，博弈s：n→x是平衡的，当且仅当它对对 话博 弈A的每个子成分的限制是交替的。这个性质是通过对被看作张量逻辑公式的有根对话博弈A3.2平衡战略对话范畴DG既然我们已经在对话游戏中引入了平衡游戏的概念，我们以对话游戏为对象，以平衡策略为态射，构造了一个对话范畴DG定义3.5有根对话博弈A的策略σ是平衡的，当σ的所有策略都平衡时，或者等价地，当σ超过BalA时。我们现在准备好用在《定义》中引入的横向策略的概念来定义DG范畴。 2.1.定义3.6范畴DG以对话博弈A、B为对象，以A−·B=B）的transverse平衡策略为态射A→B。A−·B和B−·C的两个横向平衡策略如预期的那样组成。对话博弈A的同一态射id A被定义为A −· A的transverse平衡策略，由copycat定义。 回想一下第3节开头的讨论，id A只包含平衡策略的事实意味着它比对话游戏中通常的无辜身份态射对环境的限制更大。定理3.7范畴DG定义了一个具有有限和的对话范畴，张量极点定义为有根对话博弈<$1 =<$1。α回想一下，对话游戏<$1 =<$1具有唯一的对手移动q=（α，q）通过用唯一的对手值q填充唯一的对手单元格α来定义。4轨道上的两个置换等价我们通过在§4.1中引入对话博弈A的平衡轨迹s，t：x→y上的两个等价关系RQOP和RQPO，来分析对话博弈和序列算法之间的联系。这两种关系是C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189199OPPO由对对话游戏A的深度的归纳来定义，在这种情况下，我们将其视为张量逻辑的公式然后，我们在§ 4.2中展示了一类原子OP-p-m-p -O-p然后，我们在§ 4.3中建立了一个连通性性质，该性质表明，具有相同源和目标的每对平衡轨迹s，t：x→y都通过一个序列的CNOOP和CNOPO关系相关联，如下所示：% s=% s%1% P%s %2%PO%S3-3000 ...公司简介 s n= t。连通性意味着两个等价关系OP和PO足以恢复底层对话游戏的通常置换等价关系，它识别出两个轨迹s和t，它们在对话游戏中走相同的步，但顺序不同，参见[12，13，14]。4.1两个置换等价式：我们回忆一下[4]中给出的调度函数（或调度）的定义，我们将使用它来研究轨迹中移动的可能顺序定义4.1sechedule是一个函数：{1， . . ，n}→{0，1}。因此，时间表e是0和1的序列 我们写|e|对于长度n在时间表E中，|e|0表示0的数量，|e|1代表1的个数。所以，|= n =| e|0 +|e|1 .一、|1.很明显，对话游戏A → B中的每个平衡轨迹s：x→y都定义了一个长度相同的时间表e |e|作为轨迹s，|e|0等于s的长度|A和|e|1等于s的长度|B.这个时间表使得e（i）= 0当且仅当s的第i步在A中。这两个等价关系是由对话游戏A上的结构归纳定义的，被视为张量逻辑的公式。注意，构造的最重要步骤是张量积。定义4.2两个等价关系而过平衡轨道，具有相同源和目标的存储库s，t：x→y通过对话游戏A上的相互归纳来定义。A= 0和A= 1的情况是平凡的。在和的情况下，人们通过不相交的并来定义两个等价关系：ACIBBAB.OPOPPOPO PO在张量否定的情况下，人们定义了两个等价关系，通过将具有相同源和目标的轨迹s，t：x→y限制到子分量A，并且通过反转两个等价关系以反映视角的改变sAs |A At |As A t s |A A不|一OP PO PO OP在张量积的情况下，给定两个轨迹s，t：xy→xJyJ，具有相同的源和目标，我们定义两个等价关系如下：200C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189t正是当s|A At|一和S|B B不|BOP OP OPt正是当s|AAt|一 和 S|BB不|BPO PO PO而且，s和t具有相同的时间表。这两种关系之间的关键区别在于，在张量水平上，允许在组件之间切换移动，而CIPPO不允许通过推论，在对话游戏A-·B=B）中通过BLOOP相关的两个轨迹s，t：x-·y→xJ-·yJ具有关于组分A和B。直觉是，对手不允许使用CNOOP改变对话游戏A −· B中的轨迹时间表。4.2原子在质子和质子中的相互作用在本节中，我们将说明等价关系BLOOP和BLOPO是由两个类生成的，它们分别是a到micpemu t i n tilesBLOOPPt和s BLOPO到bancedtrec-tories。通过这一点，我们的意思是，SLOOP是平衡轨迹上的最小等价关系，使得sSLOOPt，无论何时s=u1·v·u2andt=u1·vJ·u2andvOPvJ对于一些平衡轨迹u1，u2，v，vJ.换句话说，BLOOP是最小的等效相关性，其可用于计算BLOOP和BLOOP的闭合和合并概率。简 单 地 说 ， IP O是与IP O 相 关 联 的 最 简 单 的 对等关系并在平衡轨迹的组成下关闭正如我们将看到的，所有的permu-tation瓦片SOP和dPO都是在引言中描述的针对某个目标的简单实现。我们现在定义两个生成类的原子置换瓷砖S-P和D-P-O通过inductiononthedhh的didialoguegameA，Sen作为一个公式的张量逻辑。定义4.3我们将每一个对话游戏A关联到一类原子OP-p-muttinsSOPt和 一类tomicP -p-mut insP Ot。我们通过结构化和互动式的游戏进行深度的对话。 我们从张量积的例子开始，这是最重要和最有趣的例子。TensorproductfororP.AnatomicOP-pérmutationspérmutionspérmutionspérélattttwoOP-轨迹s，t：x→y（即，两个轨迹以对手移动开始，以玩家移动结束）。在三种不同的情况下，对话游戏A和B。• 基本情况：两个OP轨迹s，t：x→y的形式为：s=m1·n1·m2·n2t=m2·n2·m1·n1其中，在对话游戏A中，m1是对手移动，n1是玩家移动而在对话游戏B中，m2是对手移动，n2是玩家移动。C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189201• 左诱导病例S|AOPt|一在这一点上，|B=t|B在第二次世界大战中，• 诱导病例右侧：S|A=t|一在这一点上，|BOPt|B在动态博弈B中，TensorrpoductorP o O。在两种不同的情况下，对话博弈A和B中的两个 PO-轨迹s，t：x→y是一个自适应PO-执行过程• 左诱导病例S|AP Ot|一 在这一点上，|B=t|B在第二次世界大战中，• 诱导病例右侧：S|A=t|一在这一点上，|BP Ot|B在这一点上，我们的游戏B。单位对于基础的独立游戏0和1，不需要进行任何操作即可将游戏升级为独立游戏O我是否定的。 微分方程A的OP-突变点是微分方程A的P O -突变点，它是微分方程A的平衡轨迹之间的突变点。对称地，<$A是微分方程A的一个OP-微分方程组，它在<$A的平衡轨迹之间看到一个微分方程。总计。 一个非OP-P-mut i t i n t i t iesaOP-m u t i n t i t i n t i t ies aA或一个OP-mut in t i t int iesB。对称地，A的PO-置换瓦片A的PO -置换瓦片或B的PO-置换瓦片。通过下面的生成引理来证明由P和P O的等价性所定义的定义，该引理对每个对话游戏A都成立。命题4.4（生成）OP-置换等价性是由原子置换类生成的。 对称地， P0-置换方程是由原子置换 序列P0 的类来表示的。4.3连通性定理现在我们更好地理解了两个置换等价关系的组合性质，我们想把这两个关系联系到给定对话游戏A的平衡轨迹图G（A）的结构。我们首先为每对具有相同源和相同目标的平衡轨迹s，t：x→z命题4.5假设两个平衡的轨迹s，t：x→z开始于两个不同的对手移动m：x→y的轨迹s，和mJ：x→YJ的轨迹t。 然后，存在平衡轨迹u：YJ→z，使得 我的天啊。命题4.6假设两个平衡的轨迹s，t：x→z开始于两个不同的玩家移动，对于轨迹sn：x→y，对于轨迹t nJ：x→YJ。然后，存在平衡轨迹u：YJ→z使得s<$POnJ·u。202C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189这两个命题是通过对话游戏A上的结构归纳共同建立起来的。见附录中的证明。它们一起暗示着每个对话游戏A都满足以下重要的连通性性质：定理4.7（连通性）假设给定两个平衡轨迹s，t：x→y，具有相同的源和目标。然后，存在一系列平衡轨迹s1，...，Sn：x→y与置换等价% s=% s%1% P%s %2%PO%S3-3000 ...公司简介 s n= t。5图形游戏在本节中，我们快速回顾图博弈的概念和图博弈的构造。GG由Hyland和Schalk在[6]中引入。定义5.1一个图博弈A被定义为：• - 位置集合A=AP+AO连同初始位置ΔA，• 一组定向边，使图二分和非循环。这里，AP表示图游戏A的玩家位置的集合，并且AO表示图游戏A的对手位置的集合。 我们假设最多只有一条边图中两个位置之间的a→b。图博弈A中的一个局被定义为从初始位置A开始的路径s：A→x。 注意，根据定义， 在图博弈中，这样的路径必然是交替的。定义5.2设α是从AO到AP的部分函数，使得对于α的定义域中的每个对手位置a，都有一条边a→α（a）。部分函数α的可达位置集R（α）由归纳法定义如下：•A∈R（α）• 若a∈R（α）<$AP且a→aj，则AJ∈R（α）。• 如果a∈R（α）<$AO且α（a）被定义（因此a→α（a）），则α（a）∈R（α）。5.3图博弈A的预策略是从AO到AP的部分函数α，使得当α（a）被定义时，a→α（a），并且使得它的定义域是R（α）的子集。定义5.4预策略是无冲突的，当对于所有参与者位置a∈R（α）<$AP从aJ∈R（α）<$AO可达，则定义了α（aJ），并且a从α（aJ）可达。无冲突的直觉是，如果对手的起始位置允许进入一个潜在的未来玩家位置，那么任何玩家的移动都不应该阻止进入该位置。换句话说，只要对手选择与给定目标位置兼容的移动，策略C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189203定义5.5线性函数空间AB是与• P-位置AP×BP+AO×BO• O-位置AP×BO初始位置是A，B，并且恰好在• b=bJ和a→aJ是A• 或者a=aJ，b→bJ是B定义5.6图游戏GG的类别是由以下定义的类别：• 图形游戏作为对象• 对于两个图博弈A，B，A的无冲突预策略B如箭头A→ B我们现在已经回顾了图游戏和无冲突的前策略的类别在下文中，我们将把这一类别与我们的对话游戏联系起来。6从对话游戏到图游戏的函子我们现在制定一个概念的无冲突策略的对话游戏。无冲突的概念起源于重写理论，见[9，11]，并采用了Hyland和Schalk在图游戏框架中提出的概念[6]。定义6.1平衡策略σ是无冲突的，当对于策略σ中的每一对平衡对策s：x→x和t：x→y，以及对于每一个对手移动m：x→z和平衡轨迹u：z→y，存在一个参与者移动n：z→xJ和一个平衡轨迹v：xJ→y，使得s·m·n∈σ。我们将在特定类别的DG平衡中进行具体的评估，包括远程分布式游戏和平衡的无冲突策略。为了进行比较，图游戏中，我们通过只考虑其平衡位置来调整与对话游戏相关联的位置图（定义1.6）定义6.2有根对话游戏A的平衡图G（A）是图A对平衡位置和它们之间的边的约束。注意G（A）的路径恰好是A的平衡轨线。平衡图G（A）的这个定义使我们能够构造一个函子G： DGbal −→GG从Hyland和Schalk [ 6 ]定义的广义遗传算法的离散化类别DGb到离散化类别GGb，参见附录5中的定义。与对话博弈A相关联的图博弈G（A）以如下方式定义是payo +1的平衡位置集合，而G（A）O是payo-1的平衡位置集合。与平衡无冲突策略σ相关的策略G（σ）定义为分配给每个位置的部分函数G（σ）204C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189B BQq真Q假假a∈G（A）O表示位置G（σ）（a）∈G（A）P，只要存在平衡对策s：n→a使得对策s·n：n→a→G（σ）（a）是策略σ的一个元素.下一个结果在对话游戏和图形游戏之间建立了清晰的对应关系：定理6.3函数G：DGbal→GGs完 全 可 靠 地 将 DGbal的径向结构映射到GG的任何径向结构上.证明背后的直觉是，在范畴D G b al中的每个无冲突平衡策略都是由函数rG到Hyland和Schalk意义下的无冲突平衡策略的映射，从而到GG的态射。7双不变定理在前面两个章节（第4.7节和第6.3节）中建立的图形游戏和对话游戏之间的关系使我们能够以不同的、更组合的方式来表述无冲突的概念。定理7.1（双不变）在对话博弈A，平衡策略σ是无冲突的当且仅当它是双不变的，s ∈σ，直觉是，平衡策略σ是双不变的，只要它能够通过改变自己的执行顺序（沿着BPO）来适应对手在执行顺序（沿着BOP）上执行的改变。这种对无冲突策略的描述让人想起了[12]中无辜策略的图解定义，另见[14]（第3章，第3.4节）。双不变性定理的一个基本说明是由（B <$B）型严格合取的从左到右实现σLR提供的B. 策略σLR是无冲突的，包含以下策略sLR这是一个LRP-相当于下面的策略的LRC. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189205B BQQ假q真假显然，游戏sRL是严格合取的从右到左实现σRL的元素，而不是从左到右实现σLR的元素。此外，通过对等价性的归纳定义，q·sLR·true和q·sRL·true在平衡的对话游戏中，（（BB）B）、B= （（B <$B）−·（1 <$1））−·（1 <$1）请注意，在这个博弈中，等价关系是平凡的 由此可以得出双不变性定理（因为关系式 PO是平凡的），即每个包含对策q·s LR·true的无冲突策略也包含对策q·sRL·true。结论我们已经构建了一个完全忠实的翻译，从对话游戏和平衡策略的范畴到Hyland-Schalk图游戏和无冲突策略的范畴[6，15]。对话游戏和图形游戏之间的桥梁揭示了一些有趣的组合结构。特别地，我们建立了Hyland-Schalk图对策的结构可以从原始图恢复一个简单的实例的多个分区的多个分区和多个分区。这是一个令人难以置信的数字，一个commlementanddcounterpont ton to n t o rto nto nt o n t o rherkbyHarmer，HylandanddMelli`es[4]，并传达了对现有游戏语义范式之间更紧密联系的希望，从具体的数据结构到竞技场游戏。引用[1] G.贝瑞和P. - L.古瑞恩具体数据结构上的顺序算法。理论计算机科学，第20卷，第265-321页[2] P. - L.古瑞恩论顺序性的对称性。在编程语义学的数学基础中，计算机科学讲义中的第802号。Springer-Verlag，1993.[3] J.Y.吉拉德唯一轨迹：从逻辑的规则到规则的逻辑。Mathematical Structures in Computer Science，11（03）：301206C. Jacq，P.A. Melliès/Electronic Notes in Theoretical Computer Science 336（2018）189[4] R. H ar m er，J. M.E. 嗨，嗨，嗨。A. 我会的。 CategoRicalcombintoRicsfornocenttr ategi es. 在LICS，第379-388页[5] M.海兰游戏语义学在逻辑和计算的语义学，第131-184页。牛顿研究所出版物，剑桥大学出版社，1997年。[6] M. Hyland和A.沙尔