305网址：http://www.elsevier.nl/locate/entcs/volume65.html12页从奇偶博弈到循环证明Luigi Santocanale1LaBRI-波尔多第一大学351 cours de la Liberation，33405 Talence Cedex France摘要我们调查正在进行的研究，涉及的组合学的奇偶游戏代数的类别与nite产品，nite余产品，初始代数和nal余代数的可定义函子，即双完全类别。我们认为，奇偶性游戏与一个给定的起始位置发挥的作用，条款的理论bicomplete类别。我们表明，在集合和函数的范畴内的奇偶博弈的解释是一个玩家在游戏中的确定性获胜策略的集合讨论了两个奇偶对策之间的有界记忆通信策略及其计算意义。我们描述了如何试图将它们形式化的代数bicomplete类别导致开发一个演算的证明，允许包含周期。本文是对我们最近工作的一个综述，把自由格[1，2]上的结果提升到范畴集.格是一个具有足够的最小和最大不动点来解释形式项的格. 这个概念的推广导致考虑具有nite积、nite余积和足够多的函子的初始代数和最终余代数的范畴。我们称这些范畴为双完全范畴。这项研究的结果到目前为止在[3，4，5]中描述。我们的一个主要目标是了解如何代数的双完全范畴描述了计算的情况下，通过组合的游戏;当试图实现这一目标，计算逻辑和证明理论成为不可避免的成分。 本说明的目的是深入了解这四个世界是{类别，游戏，计算和逻辑}在这个上下文中相关。 为由于数学形式化的需要常常掩盖了这些关系，我们在这里只提出非正式的论点。读者将在上面引用的参考文献中找到这些陈述的1 电子邮件地址：santocan@labri.frc2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。306我X1- 双完全范畴和奇偶博弈1.1De ning-Bicomplete Categories范畴项是从乘积和余积的符号中生成的，通过替换和两个项构造器，一个用于最小定点，另一个用于最大定点。要构建x2X=）x2T（X）s2T（X）=）VIs;WIs2T（X）s2T（X）andx2X=）x：s;x：s2T（Xnfxg）Fig. 1. 分类-术语它们显示在图1中;在给定的可数变量集的nite子集上有X范围，在nite集上有I范围。一旦选择了范畴C，我们可以尝试将范畴项（或简称为-项）解释为形式为C X C的函子根据图2的归纳规则。试图解释任意类别C中的-项通常会失败jjxjj=pr：CXCjjVIsjj;jjWIsjj=Qi2Ijjsijj;`i2Ijjsijj：CXCjjx：s jj; jjx：s jj =参数化初始代数，的nal余代数jjs jj：CCXnfxgC：图二. 术语的解释由于缺乏某种结构：要想成功，C至少应该有nite积，nite余积，以及初始代数和nal余代数。 如果尝试成功并且所有的-项都是可解释的，那么我们说C是-bicomplete。 例如，任何局部可表示的范畴都是-bicomplete。1.2Parity Games集合和函数的范畴Set是局部可表示的，因此-bicomplete。在[3]中，我们已经展示了如何使用博弈论的思想来理解范畴项作为函子在范畴Set：out of a上的解释。- 术语和由自由变量索引的集合的选择，一个游戏被构造成使得用于307一个给定的参与者具有决定对- 任期。从这种结构中产生的游戏是奇偶游戏，这是模态演算理论的一个众所周知的工具[6，x4]。在一个对等博弈中，两个参与者和在一个位置和移动图上相互博弈。在夜间游戏中，胜利是由正常的游戏条件决定的：不能移动的玩家输了。由于图形可能包含循环，必须考虑到在夜间播放，在夜间播放的赢家根据以下规则确定。给出到位置集合的区域中的夜晚分区，每个区域具有高度{自然数}和颜色{或}。 一个在夜间播放是一个胜利的球员，当且仅当该地区的最大高度访问在夜间经常在这场比赛是彩色的。 我们从-项中得到的这种平价博弈也有在夜间高度的位置;这些位置是平局，因为没有移动是可能的，没有玩家必须移动。从这些数据中，可以通过为每个位置选择一个集合，并通过声明从这样的位置玩家必须从集合中选择一个元素，这样做他就赢了，来定义一个没有平局的游戏。1.3- 游戏在图3中，我们举例说明了如何用一个项来构造一个奇偶博弈。x：（z^y：（> _（y^x）2的项树显示在左侧，相关的奇偶博弈显示在右侧。读者会注意到，游戏的图形本质上与术语树相同。约束变量之间的依赖顺序的技术概念，来自模态演算理论[7]的标准，被编码到游戏的有序划分中，而自由变量z成为nite高度的位置。 已知在范畴Set中对这个项的解释是使每个集合E与树的集合相关联的函子，该树的集合具有以下性质：（1）树的每个节点都有子的nite列表，（2）在nite分支是可能的，（3）每个节点都被E的元素标记。读者现在面临的挑战是，在任何这样的树的右边，为博弈中的参与者构建一个确定性的获胜策略。为此，回想一下，当且仅当满足以下含义时，在夜间游戏中玩家才是赢家：如果游戏在夜间经常区域1中访问，则它也在夜间经常区域2中访问。 因此，我们建议通过循环遍历第一个区域来编码树的子树的nite列表，通过循环遍历第二个区域来编码innite分支。这个结构，如果正确猜测的话，在这些树的集合和确定性获胜策略的集合之间定义了一个双射对应， 这个游戏.2 我们在这里使用的是标准符号，例如>代表V;。308你好，J、J¸Jvz、vz、.__。2.__。！，J，z，`，\- -J，X，J，，^`，\，，.J，..J.J，，`，，\，、、、;__，_，__，，vz._______，，_______.1，J，z，`，s\J，J，，`y，\你好，，J，_，`，\，，，J，v，`z，\，J，，`，\，，J，，>`，s\， J、、、、，J，^，`，\J，s，s， J、、、、J，，`，\，，J，southy，`，s\ J、、，vzJ，X，X`，- -图三. 作为游戏的1.4奇偶博弈因此，一些奇偶博弈是范畴项的组合实现，作为对-term给定通过在相关的平价博弈中参与者的确定性获胜策略的集合。相反的问题{在奇偶博弈中确定性获胜策略集合的代数实现{出现了。也就是说，给定一个奇偶博弈，我们能找到一些描述该博弈中确定性获胜策略集的项吗？答案是肯定的，并在几个步骤中得到。我们总是可以从一个奇偶博弈中提取出一个代数表达式，这个代数表达式在每一个有nite积和上积的范畴中都是有意义的，同样是在这个范畴有足够的初始代数和nal余代数的假设下。这个表达式实际上是一个nite方程组（即迭代理论[8]或向量演算[6]的一个术语），其在集合和函数范畴中的解恰好是博弈中参与者的确定性获胜策略集合。 我们将通过解释如何在平价博弈中获胜来构造这样的表达式。从对手{玩家}必须移动的位置开始的获胜策略本质上是获胜策略的集合，对手的每一步都有一个。参与人的确定性获胜策略从一个他必须移动的位置的选择包括一个移动的选择和从下一个位置的策略。很明显，在有周期，，309，，J>> >J.__。1Xn+1=F（Xn;Xn+1;X！）9=X是某些方程组的解;更确切地说，是某些函子方程组的解，这些函子方程组的构造块是乘积和余积函数。我们在图4中建议这样做假设现在只有一个区域J，，`，\，，cJ，，`，\，8X= YX 9;>Y=Z+X=>J，，`，\，>：Z=1.- -图四、作为函子方程组的奇偶对策在夜晚的高度，这个区域被着色， ，就像图4所然后，所有的在夜间发挥是禁止的球员，和获胜的策略- gies（数学上，某种树的树枝是在游戏中发挥）不包含在夜间分支。一个简单的归纳表明，获胜策略的集合是对应的函子方程组的最小解{即初始代数{。另一方面，如果唯一的区域被着色，则在夜间游戏中玩家获胜获胜策略也 包含在nite分支中。标准论证表明，获胜策略的集合是最大解或方程组的最终余代数现在考虑一个在夜晚高度上有多个区域的奇偶博弈G。局中人的确定性获胜策略在这个游戏中，通过模仿奇偶博弈的结构递归构造的函子方程组的解的集合。在G中，通过擦除所有从极大区域中传出的信息，构造其前身博弈P（G）。 nite高度;该结构如图5所示。然后一个食谱，在G音中获胜如下：从最大nite高度简单地选择一些移动和获胜策略从下一个位置，并从一个位置在nite非最大nite高度选择一个策略，以赢得在前一场比赛，并使用它尽可能长的时间。因为通过这样做，你可以回到最大nite高度的区域，如果这个区域的颜色是，那么这个过程将非常频繁，如果这个区域的颜色是，那么将非常多次。这个配方被转换成具有以下形状的函子方程组：：n = SP（G）（Xn+1;X！）的 情况下;在这里X！是在nite高度的位置的向量，Xn +1是310你好，你好，._。！._。！，J，z，`，\，，J，z，`，\.----3，J，，`，\，，J，，`，\，，J，x，`，\J，，y`，\，、、 、、、、 ，，，，.- - _，_2;._，___ _2J， zz，，J，，`，\，，J，，`，\，，J，，`，\，，J，，`，\，........................................- - __，__。1.- - _，__。1tz，Jtz，J，J，，`，\J，，J，，`，\J，._。- -图五. 前身游戏最大nite高度的位置，Xn是所有其他位置;F是乘积和余积函子的向量，如示例中所构造图4，SP（G）是前一个博弈中获胜策略的集合;这确实是无穷大和最大位置集合中的函子夜间高度，视为变量。最后，如果最大nite高度的区域的颜色为，则该系统必须作为初始代数求解，并且 作为nal余代数。事实证明，奇偶博弈具有相同的表达能力的-项：初始代数和nal余代数，我们需要解释奇偶博弈{即，我们需要解决的函子系统的方程相关联的{正是那些需要解释的条款和定义新bicomplete类别。这一事实是初始代数的Beki c性质[9，x4.2]的一个推论。利用这个性质，也可以在算法上找到一个项来表示奇偶博弈中给定位置的获胜策略集。我们怀疑引入这样一个项是否有用，实际上我们更愿意直接处理奇偶对策，一旦它们的代数意义被阐明。2通信策略和循环证明总结上一节，我们已经论证了奇偶博弈可以扮演-双完全范畴理论的组合项的角色：它们有一个解释，并且模这个解释它们等价于- 条款 双完全范畴理论已经导致研究可定义函子之间的可定义自然变换。 博弈论也是一个有用的工具来激励这项研究为了理解其中的原因，我们需要将沟通策略的概念从博弈G引入到博弈H中。这是自由格、自由格和线性逻辑博弈论中的一个关键概念[10，11，12，1].在这些背景下，构造复合博弈G（H）以确定311博弈G是否小于或等于博弈H在G（H）中，一个被称为中介者的参与者同时在G上扮演和H上的角色，他的目标是在G上或H上获胜，或两者兼而有之。沟通策略是中介者在博弈中的获胜策略，是G H关系成立的证据。2.1计算解释游戏是众所周知的计算系统的数学模型，在游戏世界和计算世界之间来回转换概念是一种既定的富有成效的实践[13，11，12，14]。我们调整这种对应关系的数学设置的奇偶性游戏，-bicomplete类别，更喜欢认为游戏是描述双向同步通信信道。通信策略则被理解为用于让信道G的左用户以受约束但异步的方式与H的右用户通信的协议。图6表明通道G和H可以是电话线，协议M可以是应答机或操作系统。几议定书第一频道第二频道左用户ss，，r，~，~，J，r，~，~，Mss，正确使用者sst，z，ss，，rsssG，r，~，~，r，，~，，~，，r，~，~，，，钩，r，~，~，，sssH 、、、，r，~，~n，，，r，~，~，见图6。 游戏作为渠道，沟通策略作为协议博弈论的思想一旦在计算的世界中被分析，就会引起人们的兴趣例如，一个通信策略在夜间游戏中获胜的事实被转化为协议从不负责中断通信的事实，这是一个正确性条件：如果在使用协议时整个系统中发生死锁，那么G上的左用户或H上的右用户都要对此负责。在游戏G（H）中进行夜间游戏的获胜条件在计算上意味着协议是公平的：如果在整个系统中发生了夜间通信，则G上的左边用户或H上的右边用户都要为此负责;特别地，不会出现协议与其自身的312VWWV2.2作为通信策略代数的循环证明我们的主要目标是研究上述的计算情况，因此我们需要研究通信策略之间的差异，而不仅仅是它们的存在。代数这意味着解除的角度从偏序集类别和理论的格理论的双完全范畴。从计算的角度来看，有界记忆通信策略是一个有趣的问题，而且如果存在从G到H的通信策略，那么也存在从G到H的有界记忆通信策略。这一事实在格理论中特别有用，在格理论中，仅仅存在策略就很重要，因为它大大减少了寻找通信策略时的搜索空间;依靠这一事实，我们已经能够证明格理论的字问题是可判定的[1]，并且该理论的交替层次是严格的[2]。因此，我们已经开始了我们的分类调查代数有限的内存通信策略的手段演算循环证明[4] {一个逻辑设置，自然扩展[15]之一。代数学使得精确地描述发生在沟通策略。在范畴逻辑[16]中，耦合和元组操作{左引入规则和右引入规则}{分别描述了左用户在G上的动作和右用户在H上的动作。投影{左-引入规则{用于描述中介者在左侧板上的选择，注入{右-引入规则{用于中介者在右侧板上的选择。我们在图7中对此进行了验证，其中显示了两个奇偶博弈和一个循环证明。我们已经强调了博弈图和子项图之间的结构同构，这样就可以清楚地知道如何使用循环证明作为一种通信策略：在证明结构的转换之后，移动子项图上的两个标记，并通过同构移动博弈图上的两个标记。请注意，gure 7的证明其根位于底部，而游戏的起始位置位于顶部。推广图7的例子，总是可以将有界存储器通信策略（主要由一个集合和可能的循环图组成的组合对象）表示为代数对象，这些代数对象看起来像简单的微积分中的证明。这并不奇怪，因为在本节开始时我们已经指出，从G到H的沟通策略是关系G H成立的见证，即证明。另一方面，产生的证明对象是奇怪的，因为它们是圆形的。由于奇偶博弈包含循环，有界内存通信策略在其图中也会有循环，解释如何在夜间游戏中获胜，这些循环由证明对象继承。这是做代数时的一个主要问题，因为一些标准技术不再可用。在313LRcR>`>RV;ix`yh3rix`yh3r>`>_yRWfl;rg红黄> `yx`>_yRWfl;rg红黄x` y>_x_ x`yLxx`>_yRWfl;rg红黄x` yLWfl;c;rg.- -x`yr.- -1，J，，`，\，.河J.x`>_yRWfl;rg红黄x` y1，J，J，.R.J.，J，，`，\L..x，，y，，，J，，`，\L，J，，`J，\JJ，J，，`J，\> xx>_y_ _ _ _ _ - -LJ>_ _ _ _ - -LJ>见图7。 作为通信策略特别地，不可能使用标准归纳{在证明树的良基结构上}来将证明解释为任意双完全范畴的箭头。2.3循环证明针对这一问题，我们提出了如下解决方案循环证明通常被理解为任意双完全范畴中某些待定箭头上的有限方程组这一步从来没有问题;例如，图7的循环证明被转化为图8的方程组，其中我们使用f和g进行卷积运算，in用于注入，hi用于指向终端对象的唯一箭头，和;是初始代数同构。作为第二步，我们证明了每个系统的8>f1=f2>f 2 =f3inrf6l= hi9>f5c= f6c>>f3 =1f 4f6c =f3在r=>>f4=ff5l;f5c;f5rg>：f5l=f6lf5r=f6rf6r= f3inr>>;>见图8。 作为方程..314y由循环证明产生的方程有唯一解;这是[4，5]的主要结果为了实现这个目标，我们使用不动点理论。我们首先观察到，初始代数的泛性质可以解释为说明一个不动点的存在性和唯一性;然后我们注意到，如果范畴C有乘积，则泛性质的参数化版本也成立。即，如果y：F（x：F（x; y）; y）x：F（x; y）是函子F：C的参数化初始代数C，如果x;y;z：C（x; T z）Q（ x; y; z）C（ F（ x; y）;T z）是自然变换，T和Q的类型很容易从上下文恢复，则存在唯一的自然变换yy;z 2019 -05 - 22 01：02 01：03 01：02 01： 01x：F（ x; y）;Tz）使得图Q（x：F（ x;y）; y; z）yy;zC（x：F（x;y）; Tz），，yy;z;IDIC（1;T z）C（xJ：F（x; y）;T z）Q（x：F（ x; y）;y; z）x：F（x;y）;y;zC（：F（ x; y）; y）;Tz）上下班这种参数化的普遍性质的一个例子是迭代单子的替换定理[17，18]。解决由循环证明结构产生的方程组的第二个必要条件是，它们的循环应该是良性循环。“更准确地说，这些周期应该对应于解释如何在夜间游戏中获胜的获胜策略的周期在上图中观察到，自然变换y是一个方程的解，该方程在左边由1（初始代数的逆）保护。 当转化为代数时，通信策略在夜间比赛中获胜的要求陈述了以下相当合理的条件：相应的方程组必须被保护，要么在左边由某个初始代数的逆，要么在右边由某个最终余代数的逆。在图7的例子中，证明结构的循环是良性的，因为它们受到规则Lx的保护;图8中的相应方程是f3=1f4。存在的固定点和警卫是两个成分需要使用的贝琪引理，其中一个可以递归地解决方程组的解决方案，他们的子系统。HX315确认作者感谢加拿大NSERC的财政支持，Pa-c c数学科学研究所和欧洲联盟委员会通过玛丽·居里个人研究金。这些机构不对这里表达的任何观点或结果负责。作者希望感谢2002年计算机科学中的共代数方法研讨会的组织者邀请他介绍他的研究。引用[1] L.圣卡纳莱 -lattices，J. Pure Appl. Algebra 168（2-3）（2002）227{264.[2] L.李明，张文，张文。9（2002）166{197。[3] L. Santocanale，-bicomplete范畴和奇偶性函子，出现在理论信息学和应用。[4] L. Santocanale，循环证明的演算及其范畴语义，在：FOSSACS 02，第2303卷，计算机讲义。科学，2002，pp. 357{371.[5] L. Santocanale，循环证明演算及其范畴语义，技术。Rep. RS-01-15，BRICS（2001年5月）。[6] A. Arnold，D. 杨文，李文彬，李文彬. 阿姆斯特丹，2001年。[7] R. S. Streett，E. Emerson，命题μ演算的自动机理论决策过程，INF. Comput.81（3）（1989）249{264.[8] S. L. 布鲁姆，Z。李锡，迭代理论，北京，1993，迭代过程的等式逻辑。[9] D. J. Lehmann，M. B.李文，数据类型的代数规范：一种综合方法，数学系统理论14（2）（1981）97{139。[10] A.李文，李晓刚，李晓刚，等.线性逻辑中的博弈语义.北京：计算机科学出版社，1992.[11] S.阿布拉姆斯基河Jagadeesan，乘法线性逻辑的博弈与完全完备性，J。符号逻辑59（2）（1994）543{574.[12] A. Joyal，Free lattices，communication and money games，in：Logic andscienti c methods（Florence，1995），Kluwer Acad.公众，Dordrecht，1997，pp.29{68.[13] A. Nerode，A.亚赫尼斯河谷Yakhnis，Concurrent Programs as Strategiesin Games，in：Logic from Computer Science（Berkeley，CA，1989），Springer，New York，1992，pp.405{479.316[14] J. M. E. Hyland，C. H. L. Ong，关于PCF的全面抽象：I，II和III，通知。的Comput。163（2）（2000）285{408。[15] J. R. B. 科基特河A. G. 有限和积逻辑，理论应用。卡泰格8（2001）63{99（电子版）。[16] J. Lambek，演绎系统和范畴。I.句法演算和剩余范畴，数学系统理论2（1968）287{318。[17] L. S. Moss，参数协递归，理论计算。Sci. 260（1-2）（2001）139{163，计算机科学中的共代数方法（里斯本，1998）。[18] P. Aczel，J.阿达梅克河谷J.，一个coalgebraic视图在nite树和迭代，在：M. L. Andrea Corradini，U. Montanari（Eds.），《理论计算机科学电子笔记》，第44卷，爱思唯尔科学出版社，2001年。
我的内容管理
展开
