游戏语义的数学基础及其与编程语言相关性

理论计算机科学电子笔记265（2010）231-244www.elsevier.com/locate/entcs通过相干空间安娜角，澳-地卡尔德隆1，2盖伊·麦卡斯克3巴斯大学计算机科学系英国巴斯摘要游戏语义学已经成功地为各种编程语言提供了完全抽象的模型，而这是使用其他指称方法无法实现的。 虽然这是一种灵活而准确的方式来给出语义对于一门语言来说，它的底层数学是笨拙的。例如，策略组合的证明和保持强加给它们的属性（如无辜性）的证明是复杂的，需要很多注意力。这项工作的目的是开始提供一个更优雅和统一的数学基础的游戏语义。我们的目标是找到数学实体，这些数学实体将保留使游戏成为向程序提供语义的准确方式的属性，但这些属性简单且易于使用。我们的主要结果是一个完整的，忠实的强monoidal嵌入一类游戏到一类的连贯空间，其中组成是简单的组成关系。保留字：博弈语义，连贯空间，关系，策略1介绍虽然游戏语义是一种灵活而准确的方式来建模编程语言的语义（例如[3]，[9]，[1]），但游戏的不同类别大量增加，并且经常有基本的结构事实（结合性，组合的有效性）被一遍又一遍地证明，每次都有微妙的差异。因此，尝试研究游戏语义的基本构建块是有意义的，旨在使该领域在数学上更加成熟，希望将来在提出新的游戏类别时，人们可以专注于新的或不同的Harmer，Hyland和Mellies我们1 这一版本的文件纳入了匿名参考人的意见，我们对此表示感谢。2电子邮件：acma20@cs.bath.ac.uk3 电子邮件：G.A. bath.ac.uk1571-0661© 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.08.014232A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231工作采取了不同的方法，目的是通过更熟悉的连贯空间类别来解释游戏语义[7]。受Hyland和Schalk [10]工作的启发，该工作提出了一个从游戏和确定性策略到集合和关系范畴的忠实函子，我们问是否有可能为游戏语义学提供一个更优雅和统一的在博弈范畴中，一个映射σ：AB由一个博弈上的一个策略给出AB，他的戏剧是A和B中戏剧的交织。Hyland和Schalk的函子将这样的策略映射到PA和PB（A和B的策略集）之间的关系，由{（s T A，s T B）|s∈σ}。 这个函子的忠实性有点令人惊讶的是，因为函子消除了交织信息，这似乎是成为游戏模型的精髓。虽然这个函子是忠实的，但它远不是满的，它没有保留很多博弈范畴的结构，例如monoidal结构。在这项工作中，我们试图通过连续细化codomain类别来改善这种情况这与Hyland和Schalk的工作有关[10]，如下面进一步详细讨论的。相干空间和线性映射（Coh）范畴可以被看作是Rel借助相干关系的一种细化，其目的可以被认为是将确定性强加于自然非确定性的关系模型我们首先证明了Hyland和Schalk然后，我们通过强加一种顺序关系来完善Coh，旨在模仿剧本上的前缀顺序。我们称之为精化范畴P coh，并证明它具有类似于博弈范畴的幺半群结构。我们的主要结果是，Hyland-Schalk函子提升到一个完全忠实的强monoidal嵌入到一个特定的子范畴的P coh。1.1相关工作最接近我们的工作是Hyland和Schalk [10]，它提供了一个完整而忠实的函子，从游戏和确定性策略的范畴，一个类别的地图组成的关系，这可能被视为一个广义范畴的连贯空间。然而，函子的提出并不是强么半群，即失去了博弈语义的我们的目标范畴确实具有这样的么半群结构，并得到了一个强么半群函子。[4，15，6]的工作定义了一个然而，一个有点不同的地点是一个新的客户群。Melli`es的工作[16，13，14]表明，无辜的策略是“关系”的，也就是说，可以被描述为位置之间的因此，他的工作产生了一个强monoidal函子从一类游戏和无辜的战略，以Rel，这是在本质上相同的时间遗忘地图。我们感兴趣的是潜在的非无辜的战略，因为A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231233一它们在建模命令式编程特性中的用途。在这种设置中，时间遗忘操作似乎对应于从理想化Algol [ 3 ]的游戏语义到干扰控制Algol [17]的Reddy的对象空间语义的崩溃。对这一情况及其与Melli`es结果的关系的进一步分析有待于进一步的2从游戏到关系2.1预赛我们首先定义的类别的游戏，我们的工作是基于，并审查海兰和沙尔克我们不知道以前发表的证明这个函子的忠实性，所以我们在这里提供一个符号给定集合X和Y，我们用Alt（X，Y）表示其元素在X和Y之间交替的序列的集合。给定一个序列s∈Alt（X，Y），对于s的子序列只由X的元素组成，我们写sTX，对于sTY也是如此。 我们用X+Y来表示X和Y的不交并，X是元素属于X的序列的集合。给定序列s，t，|S|表示s的长度。我们用“±”表示序列的前缀顺序，即t ± s当且仅当存在某个序列 u，使得t·u=s。 我们写t±evens当且仅当t±s和|不|均匀t±odds当且仅当t±s且|不|很奇怪定义2.1一个博弈A=（MA，PA），由一个集合MA=MO+MP组成，称为A A它的移动集合，以及Alt（MO，MP）的非空前缀闭子集PA，称为A A它的策略集，使得序列s∈PA的第一个元素属于MO。 我们把MO的元素称为对手移动，把MP玩家移动A A注2.2[奇偶性]给定一个博弈A，如果s∈PA，则由于s属于MO且s∈Alt（MO，MP），如果s以对手移动结束，则|S|是A A a奇数且如果s以参与人移动结束，则|S|是偶数。 这将是至关重要的工作相干空间。定义2.3博弈A上的策略σ由PA的偶数长度元素的非空集合组成，使得如果s∈σ且t±偶数s，则t∈σ。定义2.4设E和F是凝聚偏序集，定义凝聚偏序集EF为（E×-F，×E F 、）在哪里-你好-你好（e，f）×EF（e，f）i ∈×Ee表示f×Ff，如果e× e和f“f是的。然后和d（e，f）定义2.5博弈A上的确定性策略σ由满足确定性的策略给出，即如果sab，sac∈σ，|S|偶数，则b = c。定义2.6游戏AB定义为234A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231A B一B一BA组B组• MO=MO+MPA B B A• MP=MP+MOA B B A• PABAlt（MOPA B ）由所有序列s组成，使得sTA∈PA且sTB∈PB。注2.7设s∈PA 假设x是s的最后一步。 则如果x∈MO或x∈MP然后|S|是偶数，如果x∈ MP或x∈MO，则|S|很奇怪GAM范畴以博弈为对象，箭头A→B由下式给出：确定性策略σ：AB。像往常一样，组成是由平行合成加上隐藏和模仿策略给出的身份（参见，例如[12，9，2]）。引理2.8设s∈PAB.如果|S|那就奇怪了|STA|均匀|sTB|很奇怪从这个引理可以推断出，唯一允许在A中的组件A和B之间切换的主角B是参与人，即如果scx∈PAB和|S|是奇数，则如果c∈MA（分别为MB），则x∈MA（分别为MB）。这被称为切换条件[1]。定义2.9给定博弈A和B，我们将博弈A和B定义为：•MO=MO+MOA BB A• MP=MP+MPA BB A• PABAlt（MOPA组B组）由所有序列s组成，使得sTA∈PA，sTB∈PB。DefineIGAM：=（，{}）. Letσ：AB，τ：CD是一个定义和定义στ：={s∈PA<$C B<$D|sTA，B∈σ和sTC，D∈τ}命题2.10：GAM×GAM→GAM使GAM具有幺半群结构。定义2.11函子grel：GAM→Rel[10]定义如下：它对对象的作用将博弈A映射到其策略集PA;并且，给定博弈A和B，它对态射的作用将策略σ：AB映射到关系grel（σ）：={（sTA，sTB）|s∈σ}<$PA× PB。请注意，乍一看，这个函子似乎破坏了游戏的交错信息。例如，考虑一个策略σ：AB，策略为：A B 和A Bb1 b1b2a1b3a2a1b2a2b3a3a3，M，MA.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）2312352112这两个策略都被映射到（a1a2a3，b1b2b3）∈grel（σ）。然而，前缀闭包意味着b1a1，b1b2∈σ，这破坏了确定性。事实证明，确定性和前缀闭包足以恢复交织信息这将是至关重要的证明函子是忠实的。下面的引理将这个讨论形式化。引理2.12Let σ：AB是一个离散的统计量，其中p，p∈σ有位置. 如果pTA=p<$TAandpTB=p<$TB（1）np= p。我的律师。 我是一个很好的老师。根据PA B的定义，根据PTB=PTB的公式，我们知道，PAB通常会导致内部移动，因此，我们可能会考虑移动P A B和P A B的成本相等性。我...假设，寻求一个矛盾，pp，ten（1）impliesthat|p|为|p|安迪特一定是这样的情况，有移动序列s1和s2，p=ms1anddp=ms2where|S1|为|S2|/=0（2）我们将 介绍 如何 从移 动设 备和 移动 设备 中进 行移 动。 Supose|M|奇怪是，新的网络不能用一种不受欢迎的移动方式来写它。（1）第一章：第二章：wehavep=mab1sandp=mab2s当ereb1s时，=s1andb2s=s2和b1/=b2。因为策略是偶数长度前缀闭的，所以可以得出mab1，mab2∈σ，b1b2与确定性相我们得出结论，m的长度是偶数，因此，S1和S2中的第一步是由对手完成的，根据切换条件，它们必须与a处于相同的分量。由（1） b1=b2.但根据m的极大性， b1/=b2 ，sos1=s2 = b2，b1/=b2，sos 1 = b2. 我们可以得出p=p的 结论。Q下面的引理是决定性的一个简单推论引理2.13Let σ：AB是一种分布式存储器。 Letp，p∈σ，p=/pTA，pTA在移动时不存在p;np，p在移动时不存在B。命题2.14grel：GAM→Rel是忠实的p. If证据 令σ，τ：AB是确定性策略，grel（σ）= grel（τ）。让p∈σthenthere存在sp∈τwithpTA=pTAandpTB=pTB（3）我们将为所有这样的t±evenp，t±evenp显 示以下内容：L ett？evenp.If|不|= 0thent=0和t±evenp。对于inducivestep，suppose|不|>0。Thent=tmnfor somet±evenp;byinduction，t±evenp. Supposep=tmn;wewewilllshowthattmn=tmn.236A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231Since|不|这是一个很好的例子，因为它是一个简单的组件。 So，by（3）m=m. Supposen/=n. （3）对于n，n∈A，n ∈ B，n ∈B，n ∈A，n ∈ B，n∈ B，n ∈ A，n∈ B，n ∈B，n∈ A，n ∈ B，n ∈ B，n ∈A，n ∈ B，n ∈ B，n∈A，n∈ B，n ∈ B，n ∈ A，n ∈B，n ∈ B，n ∈ A，n ∈ B，n∈B，n ∈ A，n ∈ B，n ∈ B，A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231237111111---对称地）。 Writes=tmnandds=tmn. 我们现在知道了（sTA， sTB），（sTA，s<$TB）∈grel（σ）（sincegrel（σ）=grel（τ））.嘿，这是一个简单的1，∈σ，s1TA=sTAs1TB=sTBanddsTA=sTAsTB=sTB观察到n∈A是A中的对手移动（因为它是AB中的玩家移动）。Now，s1TA，s TA通过公式2.13，s1，s2定义了移动和移动的差异第一dierinB. 现在，s1TB，s1TB表示dinn∈B，其中h ich是可移动的;但这是对σ的连续定义。因此，n=n，并且对于给定的p，p是连续的。从这里可以看出，p=p，σ=τ。一个对称的论证表明τ<$σ，因此σ = τ是必要的。Q注释2.15函子grel只在顶层消除了交错：保留了A和B中的全部细节。这与[4，15，6]中研究的“时间遗忘”操作相反3从博弈到相干空间我们转移到范畴Coh[7]，它有作为对象的相干空间，以及作为受某些约束的态射关系，我们已经可以在这个范畴中看到一些博弈结构我们确定grel：GAM→Rel提升到一个忠实的仿函数gcoh：GAM→Coh.定义3.1-• 集合E上的凝聚关系记为×E，是对称自反关系×-对大肠我们写e1-e2当且仅当e1=e2或e1×e2。•- -一个相干空间（E，×E）由一个集合E和一个相干关系×E组成。-• 一个相干空间E的构形是E的子集F，使得f1× f2，对任意f1，f2∈F.定义3.2我们现在描述一个范畴Coh。它的对象由凝聚空间给出。给定两个相干空间E，F，箭头E→F由下式给出：对于每个函 数（e，f），（e，f）∈Γife×Ee-则f ×Ff，-你好如果e×Ee且f=f，则e=e。 组成和特性如集合和关系的范畴，Rel。注意，地图上的条件相当于要求所有（e，f），（e，f）∈Γife×Ee-则f ×Ff≠，如果f =fthene=e。定义3.3设E和F是相干空间，我们定义相干空间EF为（E×-EF-你好EF-e（f×Ff）F，×且（f=f）e= e观察到范畴Coh中的箭头E→F由以下构型给出：EF.238A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231grel（σ）withs× t. 我们知道给定一个博弈A，其策略集为PA，我们可以通过定义-s × t当且仅当s和t的最大公前缀长度为偶数或s= t。-则（PA，×）是一个相干空间，记为gcoh（A）.下面的命题表明，这种连贯性的概念准确地抓住了战略的确定性。命题3.4给定博弈A和B，策略σ：AB是确定的当且仅当grel（σ）：gcoh（A）→gcoh（B）是Coh中的a映射。证据 设A和B是博弈，并假设σ：AB是确定的战略 设（s1，s2），（t1，t2）∈1-1s，t∈σ，其中（sTA，sTB）=（s1，s2），（tTA，tTB）=（t1，t2）. 如果s=t，则显然-t2×s2和t2=s2和t1=s1。假设s/=t，则通过确定性，它们的第一个分歧点m∈MA B，必须是A中的对手移动 B，因此m∈A，一个玩家的移动或者m∈B，它是对手的移动。如果m∈A，则s11× t，所以必须是m∈B;注意m也是-s2和t2，因此是s2×t2。 假设s2=t2，因为我们已经证明了，并且t必然是B中的第一个变量，我们必须有s1=t1，因此grel（σ）是一个构形。另一方面，假设grel（σ）是一个配置。设sab，sac∈σ，其中|S|是偶数，a，b，c∈MA B。我们说b=c。观察b，c是玩家在AB中的移动，因此每个都是A中的对手移动或玩家移动。移动到B。• b，c∈A，则不存在atsabTA=saTA·bsacTA=saTA·c. Ifb/=c;tens，t-b（或c）处的第一步，这是A中的对手移动。因此sabTA× sacTA。现在，sabTB=sacTB，所以它必须是，因为grel（σ）是一个配置，sabTA=sacTA，所以b=c。• b，c ∈ B. 我们有sabTA=saTA=sac TA-因此sabT-A×sacTA这么说sabTB×sacTB。由于b，c是玩家移动，因此，|SATB|是奇数，它mustbethatb=celsesabTB-×sabTC• b、c分别属于A的不同组分b∈B，c∈A。 然后我们有sabTA = saTAanddsacTA = saTA·c，c是A和s中的不受约束的运动，|萨塔阿|- -是偶数，因此sabTA×sacTA;这意味着sabTB×sacTB。现在我想，sabTB = sa TB·b和sac TB = sa TB但b是参与人移动，所以|SA TB|是奇数-这与sab T B × sac T B相矛盾，因此这种情况不会发生。Q推论3.5grel提升到一个忠实的函子gcoh：GAM→ Coh。4从博弈到凝聚偏序集我们现在在Coh上施加一个更像游戏的结构，并得到一个新的类别，我们称之为Pcoh，更具体地说，我们施加了一个顺序关系，旨在模仿游戏上的前缀排序。A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231239-定义4.1相干偏序集（E，×E，E的最小元素为-E和E上的相干关系×E，满足：-• 对任意e ∈ E，e × n。•- -e1×e2，e1<$e2，e2×e3，e2<$e3意味着对任意e1，e2，e3∈E，e1×e3.定义4.2我们现在描述一个范畴P coh。它的对象由凝聚偏序集给出。 给定两个相干偏序集E和F，箭头E→F由下式给出：r∈F，则（e，f），（e，f）∈-r-我...Γ ife×Ee则f ×Ff，并且，如果e×Ee和f“E e。复合是关系复合，给定一个相干偏序集E，idE：E→E由恒等关系给出。定义4.3设E和F是凝聚偏序集，定义凝聚偏序集EF为（E×-F，×E F 、）在哪里-你好-你好（e，f）×EF（e，f）i ∈×Ee表示f×Ff，如果e× e和f“f是的。然后和d（e，f）观察到范畴P coh中的映射E→F由相干偏序集EF的配置给出。-给定一个博弈A，我们可以建立一个相干偏序集（PA，×，A的游戏，与前面的连贯关系一样，函子gcoh：GAM→Coh提升为忠实函子gcoh：GAM→P coh。如上所述，博弈A被映射到一个相干偏序集，而策略σ被映射到一个配置gcoh（σ）。注4.4对于函子gcoh：GAM→Coh和gcoh：GAM→P coh，我们都写gcoh;这应该不会引起混淆，因为从上下文中可以清楚地看到上域范畴是什么。-设（F，×，我们写tmaxs，只要t在F中是最大的，使得ts。定义4.5设E，F是相干偏序集，并假设Γ：E→F是一个构形。 我们称Γ为有记忆构形，如果对每一个（e，f）∈ Γ，如果有存在某个f∈F，使得f-× f和f如果存在不确定性，-e 并且，如果存在某个e∈E，其中e=e并证明了存在唯一的f∈“f”，满足f ∈ = f和d（e ∈，f ∈）∈ Γ。引理4.6存在P coh的子范畴P cohm，其中P cohm的对象是那些P coh，和其地图组成的配置与记忆。现在，函子gcoh：GAM→Pcohm使得我们可以从gcoh（σ）恢复σ的然而，它仍然不是满的：没有任何东西对应于切换条件，所以给定（s，t）∈Γ：gcoh（A）→gcoh（B），我们不能总是以交替的方式交织它们以恢复AB的播放。此外，r可以包含一些奇数长度序列。下面的条件解决了这两个问题。∗240A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231注4.7我们现在只处理P cohm的对象X，它满足对每个s∈X，{s∈ X|ss}isfinite.定义4.8设E，F是凝聚偏序集。 A配置Γ：EF满足如果对于（e，f）∈Γ，则特征值为一个具有最大值x-ε的相同的特征值∈E当且仅当存在某个f∈F且f∈maxf和f-×f.e和e × e推论4.9我们定义Pcoh的一个子范畴Pcohm，s，它的箭头由满足转换的具有记忆的构形给出。引理4.10假设Γ：gcoh（A）gcoh（B）是满足切换的配置。 设（s，t）∈Γ，则|S|当且仅当|不|是偶数。证据 根据切换和观察，只要s，t ∈ gcoh（C），对于一些C，s最大值-t s× t意味着|均匀|不|是奇数，且s = t|is odd, and s≺maxt s = t意味着|S|很奇怪，|不|是偶数。Q定理4.11gcoh： GAM→Coh提升到一个完全忠实的函子gcohm ：GAM→P cohm，s证据忠实性已经建立，我们继续证明函子是满的。设A，B是对策，并假设Γ：gcoh（A）gcoh（B）是一个构形。现在我们归纳地定义元素（s，t）∈Γ的交错u，并证明u∈PA B。我们把所有这样的u的集合表示为σ。我们将（s，t）∈Γ映射到u∈σ如下：Map（，）∈Γ to∈σ.首先观察到，对于任何非空s∈PA，（s，n）/∈Γ。所以情形是：如果（n，b1b2）∈Γ，则将（n，b1b2）∈Γ映射到b1b2∈σ.若（a1，b1）∈Γ，则将（a1，b1）∈Γ映射到b1a1∈σ.given（s，t）∈Γ，其中hu∈σ定义为（u∈PABsuc hthatuTA=sanduTB=t），search对于所有元素s（s，t）∈Γsuchthat（s，t）max（s，t），map（s，t）∈Γ至v∈σ如下：观察到如果|s|、|t|由于两种移动方式都有可能导致这种情况，而且它的速度和移动速度都很快。因为如果你是我的话，-b1× t与记忆我知道了∗∗∗这意味着存在唯一“× s和（s，t·b1）∈ Γ. 但后来（s，t）（s，t·b1）（s，t）contradicts（s，t）ax（s，t）. 如果s>s·aiai+1，则sin ces·aiai+1=sitfollwsthat（s·aiai+1，t）∈Γ，对于一个单一的q u et，hich又与极大性相矛盾。如果（s，t）=（s·aiai+1，t）thenv=u·aiai+1.如果（s，t）=（s·ai，t·bi）则v=u·aibi如果u的最后运动是f的最后运动如果U的最后移动是T的最后移动，则S_ndv=u·bia。若（s，t）=（s，t·bi），或r（s，t）=（s·aiai+1，t·bi），或r（s，t）=（s·ai，t），则his与转换矛盾，因此这些元素不能存在于Γ中。如果|s|、|t|由于移动速度非常快，因此可以通过两次移动来快速地移动和存储。∗A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231241我×tn+1此外，obserevet（s，t）可以不等于或r（s，t）=（s·ai，t）beca use rs atisswit chin g.若（s，t）=（s，t·bibi+1）则v=u·bibi+1.如果（s，t）=（s_i·ai，t_i·bi）则v=u·bi_i 如果f_u的最后移动等于t_i的最后移动，则v=u ·ai_i如果f_u的最后移动等于s_i的最后移动，则v = u·ai_i如果f_u 的 最后 移动等 于t_i 的 最后 移动 ，则v = u· ai_i.要看到这些序列在A中给出的剧本注意到如上定义的序列的第一个元素总是B的元素。满足交替条件是因为转换，因为对于任何（s，t）∈Γ，s和t是游戏，因此是交替的，以及我们构造序列的方式可以证明，所有这些策略的集合σ形成了一个策略：前缀闭包由记忆条件得出，确定性由类似引理3.4的论证得出。Q4.1Monoidal结构我们现在概述P coh上的幺半群结构。 有了这个结构，函子gcoh：GAM→Pcoh是强么半群。注4.12我们从1开始索引序列，使得长度为n的序列s的元素为s1，s2，.，sn.按照惯例，我们用s0表示n。定义4.13设E，F 是凝聚偏序集。我们定义了凝聚偏序集E<$F如下;集合E<$F由满足以下条件的所有s∈Alt（E\{n}，F\{n}si−2<$Xsi<$i∈{2， . . 、|S|}X=E，F-si−2×Xsi∈{2， . . 、|S|}X=E，F.- -×E<$F，和t1位于不同的相干偏序集上，或对每个n ≤ min {|S|、|不|} s1. sn= t1. tn这意味着，sn+1-。s“E<$Ft当且仅当s±t或s=s1... si+1，t = t1. ti+n，n ≥ 1且s1. si=t1... ti和si+1“t i +1。张量定义背后的想法是模仿游戏中发生的事情，如下面的例子所示。考虑博弈N，其中MN：={q}<$N，左边是N<$N中的博弈，右边是gcoh（N）<$gcoh（N）中的等价序列。242A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231NNgcoh（N）gcoh（N）Q1Q7Q2七方六方Q7Q4Q6一年二年四月一年二年四月观察到q1q2gcoh（N）q1q2q4，由于|一季度二季度|是偶数。-q1q 2q 4，因为q1q 2<$q 1q 2q 4和q1q 2×gcoh（N）同样地，q7=gcoh（N）q 7q 6和q7=gcoh（N）q 7q 6。所以s=（s1）（s2）（s3）（s4）=（q1q2）（q7）（q1q2q4）（q7q6）∈gcoh（N）∈gcoh（N）.引理4.14我们可以将P cohm，s×P cohm，s→P cohm，s推广到双函子张量单位定义为I：=（{k}，id，id）。给定配置Γ：E→F和Δ：G→H，我们将Γ Δ定义为{（s，t）∈ E <$G→ F <$H|i ≤ |S|j ≤|不|S. t.如果si∈E，则tj∈F且（si，tj）∈ Γ若si∈G则tj∈H且（si，tj）∈Δ和i若siJ∈E，则ujJ∈F且（siJ，ujJ）∈Γ如果siJ∈G，则ujJ∈H且（siJ，ujJ）∈Δ，且j若UJJ∈F则siJ∈E且（siJ，UJJ）∈Γ若UJJ∈H则siJ∈G且（siJ，UJJ）∈Δj≤|u|i≤|S|S. t.如果tj∈F，则si∈E且（si，tj）∈Γ如果tj∈H，则si∈G且（si，tj）∈Δ且i若siJ∈E，则ujJ∈F且（siJ，ujJ）∈Γ如果siJ∈G，则ujJ∈H且（siJ，ujJ）∈Δ，且j若UJJ∈F，则SIJ∈E且（SIJ，UJJ）∈Γ如果ujJ∈H则siJ∈G且（siJ，ujJ）∈Δ}A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231243下面的引理给出了张量运算的另一种表征244A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231并协助证明其功能性。引理4.15设Γ：E→F和Δ：G→H是构形。 则（s，t）∈Γ Δ当且仅当存在唯一函数f：{0，.、|不|} → {0，.、|S|}是保序满射的，使得对所有i≤|不|.引理4.16Pcohm，s×P cohm，s→P cohm，s使P cohm，s具有幺半群结构大部分的工作是证明相干结合同构的存在;我们在这里给出定义。给定凝聚偏序集E，F和G，同构γ：（E<$F）<$G→E<$（F<$G）由两个偏序集同构α：（E<$F）<$G→E<$F<$G和β：E<$F <$G→E<$（F<$G），其中E<$F<$G<$（（E+F+G）\<$）<$是张量的明显三元版本给定一个序列，s∈（E<$F）<$G，例如s=（e1f1e2）g1（e1f1e2f2）g2，同构α消除了E<$F中的所有重复，得到一个序列s=e1f1e2g1f2g2.同构β重新括起这个序列，在必要的地方重复元素以获得序列t∈E<$（F<$G），在这种情况t=e1（f1）e2（f1g1f2g2）.α有一个简单的归纳定义：• α（λ）=λ• α（s）=s如果s=g，g∈G或s=s1. sn∈E<$F。• α（s）= α（s1. si）·si+1如果|S|= i +1，si+1∈ G.• α（s）=α（s1. si）·si+1\u如果|S|=i+ 1si+1∈E<$F其中u是si+1和si−1的最大公共前缀，如果i >1，否则u=1，si+1\u表示si+1，去掉前缀u。在β的定义中，必须小心，因为例如给定e1f1e2f2g1f3g2，我们必须小心地产生序列e1（f1）e2（f2g1f3g2），而不是序列e1（f1）e2（f1f2g1f3g2）/∈ E（F G）。为此目的，我们定义算子，其中给我 们 一 些 时 间，|不|=i，|t|=ntt=t1.. . 我.. . . tifttannd1N1tt=t1.. . ti−1·t.. . 我不知道。1N1我们定义β：E<$F<$G→E<$（F<$G），因为，给定t∈E<$F<$G，t=t1... titi+1. ti+n和ti+1. ti+n/∈E，ti∈E，若n = 0，则β（t）=（β（t1. ti−1））·ti，else：• 如果i= 0，则β（t）=（t1. tn）• 如果i= 1，则β（t）=t1（t2. tn+1）• 如果i >1，则β（t）=β（t1. ti）·（last（β（t1... ti−1））ti+1. ti+ n）），其中last（β（t1. ti−1））是β（t 1.的最后一个元素。 ti−1）。现在我们将定义一个自然同构δ：gcoh（A）<$gcoh（B）→gcoh（A<$B）。 δ由下式给出：A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231245• δ（θ）=θ• δ（s）= s，如果|S|= 1个• δ（s·si）=δ（s）·si\si−2。我们解释了通过example.让一和B被游戏和让我，我，我∈N是A和B中的对策分别同构δ：gcoh（A）<$gcoh（B）→gcoh（A<$B）映射一个序列gcoh（A）gcoh（B）to a playABs1s1s2s1s2s3s1t1S1t1t2t2S2t1t2t3t3S3直接验证δ是满足适当相干图的自然同构，连同定理4.11，得到：定理4.17gcoh：GAM→Pcohm，s是一个完全忠实的强monoidal函子.5未来工作作为当前工作的扩展，我们将分析更多的P coh的范畴结构，包括对序列结构（Laird术语[ 11 ]）和它在P coh上诱导的线性指数余项的研究这也将是有趣的调查那些部分P coh的谎言以外的图像gcoh。也许这一类别使我们能够接触到“游戏类”对象，这些对象不能轻易地表示为游戏，但在建模逻辑或编程语言中很有用。例如，我们是否可以拥有不总是具有指定初始移动的类似游戏的结构，如果可以，我们可以用这样的结构建模什么如前所述，与“时间遗忘”的地图Baillot等1。 [5]与Melli`es关于位置性和无辜策略的研究相比，我们应该更紧密地理解这一点。值得研究的是，如何在Pcoh中定位无辜策略（也许可以使用[ 8 ]的技术），以及如何将Melli`es的工作扩展到对无辜策略进行排序。我们相信这将在游戏模型和Reddy的对象空间模型之间建立更深层次的联系引用[1] Abramsky，S.和R. Jagadeesan，乘法线性逻辑的游戏和完全完备性，软件技术和理论计算机科学的基础（1992），pp. 291-301246A.C. Calderon，G.McCusker/Electronic Notes in Theoretical Computer Science 265（2010）231[2] Abramsky，S.，R. Jagadeesan和P.Malacaria，PCF，信息和计算163（2000），pp. 409-470[3] Abramsky，S.和G. McCusker，线性，共享和状态：一个完全抽象的游戏语义理想化的Algol与积极的表达式（扩展的抽象），在：1996年研讨会线性逻辑，电子笔记理论计算机科学3（1996年），页。2比14[4] Baillot，P.，V. Danos，T. Ehrhard和L. Regnier，Timeless games，in：Computer Science Logic：11th International Workshop Proceedings， Volume 1414 of Lecture Notes in Computer Science.EACSL（1998），pp. 56比77[5] Baillot，P.，诉达诺斯，T.Ehrhard和L.Regnierl，Believe it or not，ajm68比75[6] Boudes，P.，厚子树，游戏和实验，在：诉讼，TLCA 2009，编号5608在计算机科学讲义（2009），页。六十五比七十九[7] Girard，J.-是的，Y. Lafont和P. Taylor，[8] H ar m er，R.， M. 海兰丹。-A. Melli`es，Categor icalcomnatorinateg is，n：Proceedings，22nd IEEE Symposium on Logic in Computer Science（2007），pp.379-388.[9] Hyland，M.和C.-H. L. Ong，关于PCF的完全抽象：I，II和III，信息和计算163（2000），pp. 285-408[10] Hyland，M.和A. Schalk，线性逻辑的抽象游戏扩展摘要，理论计算机科学电子笔记29（1999），pp.127-150.[11] Laird，J.，高阶存储的范畴语义，在：R。Blute和P.Selinger，编辑，Proceedings，第9届范畴理论和计算机科学会议，CTCS 2002，理论计算机科学电子笔记（2003）。[12] McCusker，G.，游戏和FPC的完整抽象，信息和计算160（2000），pp。1比61[13] 我来了，P。-A. 如图3所示：电子日志的非实时更新，电子日志。 不，不，不。Comput. Sci. 122（2005），pp. 171-192.[14] Mellies，P.-一、Asynchronous games 4：A fully complete model of propositional linear logic，in：LICS386-395.[15] 我来了，P。-A. 一个简单的几何形状和一个简单的函数， 我也是。 SCI. 343（2005），pp. 237-281。[16] 我来了，P。-A. 如图2所示：网络操作的过程，或。 来吧。 SCI. 358（2006），pp. 200-228[17] Reddy，U.美国，全局状态被认为是不必要的：无干扰命令式程序，Lisp和符号计算9（1996），pp。7比76