名词模型中的博弈语义 - 基于名义序列的游戏模型的数学处理【游戏语义，名义集合，等变性】

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）173-189www.elsevier.com/locate/entcs名词模型中的博弈语义默多克·加贝赫瑞瓦特大学英国爱丁堡www.gabbay.org.uk丹·吉卡英国伯明翰大学计算机科学学院摘要我们提出了一个基于名义序列的游戏模型，它概括了原子序列和一个新的概念。这给出了一个新的，精确的，和组合的数学处理正义指针在游戏语义。关键词：博弈语义，名义集合，名义抽象和共同抽象，等变性1介绍游戏语义学是一个成功的集合技术给予表示的逻辑和计算。它通过解决PCF的完全抽象的开放问题而变得特别突出[2，19]，并被广泛用于哲学和逻辑，以模型检查和数字电路的合成[22，13]。游戏隐喻是支持者和反对者之间的对话：游戏记录了一个术语（支持者）和它的上下文（反对者）之间的交互，以及它们是如何安排的。一种建模方法是将一个游戏作为一个标记的非循环图，称为指针序列。图中的每个节点都是一个Proponent或Opponent移动，图中的边表示该移动的合理性。因此，指针序列记录了进行了哪些移动、以什么顺序移动以及为什么移动。我们提出了一个基于名义集的游戏模型，灵感来自指针序列，与不同的是，我们使用原子从名义技术（我们也可以称之为名称）的边缘模型为什么这是有用的将在一瞬间变得清晰1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.08.012174M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173≤≤≤原子只是一组可数的、无限的、不同的符号：a、b、c、.......................A图显示了这些函数如何对指针序列进行建模。左边的指针序列对应于右边的标称序列对应于qc[a]qJa[b]aaJbaJJb问题和答案用q和a来写，原子被用作指针。符号[a]和[b]可以被认为是命名问题q和qJ，并且是“未来”的粘合剂所以我们看到上面的q只代表两步：qJ和a。指针（上图中的箭头）被渲染为一对原子。 尖端 由一个共同抽象[b]表示，它必须是唯一的（这是由定义2.8中的条件b/a∈tom s（e）形式化的）。不需要是唯一的，但可以是名称的出现这直接涉及悬挂指针，它们被视为自由名称;在上面的序列中，c是自由的。名义序列具有以下良好性质：(i) 标称序列的子序列是标称序列。指针序列的子图不是指针序列，因为它可能有“悬空指针”。从这个意义上说，名义序列概括了指针序列，并有助于更容易地谈论(ii) 两个名义序列的连接是一个名义序列;名称连接起来，没有重新索引同构。如何连接指针序列还不是很清楚(iii) 名义序列是一种归纳数据类型，可以用标准工具进行操作（为了充分受益，需要一个机械化的名义系统[26]，但我们将看到我们的序列也简化了纸笔证明特别是使用名称有一个重要的，特别是名义上的优势：它可以特别有效地管理重命名指针，以避免我们使用名称来命名移动而不是数字是重要和有用的，因为名称在定义上是对称的（即可以排列）;我们不仅可以使用排列来进行α转换，而且可以将名称及其排列对称性作为原始保存排序，因为排列必然会传播到我们使用它们构建的东西，例如游戏和策略。[1]这种名称管理风格是名义技术的特征，我们将看到它在这里是有效的。我们形式化PCF [19，23]和并发Algol [14]的游戏模型，在低[1]关于这一点的一般陈述是等方差原理（见[7，4.2小节]，[12，引理4.7]）。等变性原理意味着，如果我们在定义和定理的所有参数中一致地置换名称，那么我们得到另一组有效的定义和定理。这对于数来说是不正确的，因为我们的数学基础通过构造使数具有诸如小于或等于之类的数值性质，这些性质可以从没有参数的第一原理中定义因此，如果我们使用数字来建模指针序列，那么我们不关心，因为我们只需要一组可数元素，但我们必须反复证明我们没有使用不对称属性，如.相反，如果我们假设名义基础并使用原子，那么我们不必明确证明对称性，因为我们只需查看我们的数学基础并注意到它在置换名称下是自然对称的;我们为自然对称的活动保留数字，例如计数。QQ'一a'a''M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173175头顶用原子来修饰序列并不比用指针来修饰多一点开销，而等变性是管理重命名的一种非常有效的方法，因此开销很低，而且在精确性和简洁性方面的优势似乎很明显。我们不能在这篇会议论文中复制这两篇大型论文中的所有定义和证明，我们并不主张把上面的工作做得微不足道。然而，我们确实声称，使用我们的公式，游戏语义可以更快，更准确，更透明地进行。这不仅对良好实践很重要：我们推测，通过我们的公式化，游戏语义证明的实现和机械化明显更容易。读者可以将本文中的定义与原始版本[19，14]进行比较，并判断在Isabelle这样的证明者中哪个更容易使用。此外，游戏语义可以为程序验证和硬件合成提供理论基础，因为规模或安全性，或两者兼而有之，许多以前的工作必须通过机器检查证明来增强纸笔风格在这里，上面列举和讨论的组合性，计算性和对称性确实很重要。最后，博弈语义可以通过抽象机器的通信来协调指称语义的组合性和操作语义的有效性[16];在这里，指针的传统表示可以说是积极违反直觉的，而使用名称作为消息的标签则带有直接的计算直觉。2名词性博弈语义学2.1名义序列定义2.1在有限个原子A和常数的集合中可数地固定不相交。 a、b、c将在不同的原子上变化（置换约定）。f、g、h将在常数范围内变化，不一定是不同的。定义（标称）序列，e：：= ε |EA |e f |e [a]。注2.2把ε称为空链表，把e eJ记作链表连接。 “呼”，“呼”，“呼”。这让我们想起了原子--名义技术的抽象[12]--但是在e[a]中，a“我们在结论中对比了抽象和共抽象的预期含义定义2.3定义共抽象和自由原子ca（e）和fa（e）：ca（ε）=fa（ε）=ca（ea）=ca（e）fa（ea）=fa（e）（{a}\ca（e））ca（ef）=ca（e）fa（ef）=fa（e）ca（e[a]）=ca（e）<${a}fa（e[a]）=fa（e）用atoms（e）=fa（e）ca（e）定义原子176M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173引理2.4 ca（e eJ）= ca（e）ca（eJ）和fa（e eJ）= fa（e）（fa（eJ）\ca（e））。定义2.5重命名ρ是从原子到原子的函数，do m（ρ）={a|ρ（a）=/a}是有限的。 用于重命名suc h的IDE类型的写入IDid（a）=a和ρJ<$ρ对于复合使得（ρJ<$ρ）（a）=ρJ（ρ（a））。称之为双射ρ置换。在[12]之后，让π在排列上的范围（在名义上下文中重命名的应用可以追溯到[11]）。定义2.6用y定义序列上的重命名作用ρ·eρ·ε=ερ·（ea）=（ρ·e）ρ（a）ρ·（ef）=（ρ·e）fρ·（e[a]）=（ρ·e）[ρ（a）]2.2名词性博弈语义学博弈是一个竞技场（定义2.7），伴随着一些合法的策略，这些策略是支持者或反对者的一系列行动--确切地说，什么样的策略是合法的，决定了他们所玩的博弈的类型定义2.7一个arena是一个元组A=（qstA，ansA，λA，λA，iniA）：• 不相交的问题集q∈qstA和答案a∈ansA。记为m∈mvsA=qstA 简称为A，称之为移动集合。• 极性函数λA：mvsA→ {O，P}。写O=P和P=O。• 一个使能关系<$A<$mvsA×mvsA，其中m<$AmJ蕴涵m∈qstA，λA（m）=λA（mJ）<$。• 一组初始问题可以是：· λA（i）=O，对每个初始i ∈iniA.· 如果q∈qs tA且i∈in iA，则q/A<$i。定义2.8通过以下归纳法定义竞技场A上的原游戏e：e：：=ε |ema[b]（b/a∈tom s（e））回想一下，m∈qstA≠A。 为A的所有原策略的集合写一个应用程序A。每一个原型游戏都是一个序列，但不是每一个序列都是原型游戏。e的范围总是很清楚的。定义2.9称m为a[b] a（named）move;m将在命名的移动范围内变化注2.10·一个原型游戏由一系列命名的棋步组成，每一个棋步由一个棋步m、一个证明名称a和一个我们称之为m名称的共同抽象[b]组成。这个b• 新鲜度条件b/a∈toms（e）makesb在顺序这是错误的我们不能重复使用名字即使我们知道我们可以但我们为了数学上M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173177的方便而优化178M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173⊆≤• 在[19，23，14]的博弈模型中，只有问题是合理的，因此对于本文中的应用程序，我们可以放弃在原型中命名答案的共同抽象（所以：qa[b]，但只是aa）。然而，这使定义复杂化，失去了一般性，所以我们留下（虚拟的）共同抽象，取A×mvsA。在按值调用语言的游戏语义中，证明移动正确的an-swers被用来构建定义2.11假设e和eJ是序列。写eJe当eJeJJ=e对于某个eJJ;称eJ为e的前缀。 写eJe当eJJJeJeJJ=e对于某个eJJJ和eJJ;称eJ为e的一段。定义2.12定义使能（e）由e∈pplyA使能的移动：enabled（ε）=enable ed（ema[b]）=enable ed（e）{mJb|mAmJ}引理2.13使ed（e）={mb|mJa[b]e，mJAm}。定义2.14给定e ∈ pplyA，定义其基础序列|e|通过：|= ε|= ε|为|e|M|m定义2.15的直觉在备注2.16中讨论：定义2.15假设A是一个竞技场，且A是A。(i) 当eJma≤e且m/in∈iA蕴涵ma∈enableed（eJ）时，称e∈pplyA为justified(ii) 当eJia[b]≤e蕴涵eJ=ε时，称e∈p plyA是良开的.(iii) 当a[b]eJ∈e蕴涵a/f∈a（eJ）时，称e∈pplyA严格可得，对于每个EJ∈pplyA，a∈ansA，原子a。(iv) 当qa[b]e2qJb[c]e3abe蕴涵aJce3时，称e∈pplyA是严格嵌套aJ∈ansA的某个对应动作。2(v) 称e∈ppl yA交替，当mmJ|e|设λA（m）/=λA（mJ）。注释2.16直觉，定义2.15是指：• 当每一个非初始移动都响应于前一个移动时，e是正当的• 当初始移动是唯一的并且在序列中是第一个时，e是良好开放的• 当一个问题最多只能得到一个答案时，e的范围是严格的3如果我们将游戏理解为过程，这意味着回答一个问题会停止与该问题相关的过程• 当以（相反）顺序回答问题时，e是严格嵌套的这禁止从b内部启动进程b，然后启动c，然后在c之前停止b。e交替的直觉似乎很清楚，但它与名称和绑定没有直接关系，因此我们不会进一步考虑它定义2.17和2.18遵循[23，Sec. 2.1]：[2]这里重要的是原子c。[14]第14页。7]M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173179›→定义2.17给定合理的e∈应用A，定义支持者观点e浏览次数：4εema[b]eia[b]eqa[b]eJmb[c]ε=εema[b]=eqa[b]eJmb[c]=定义2.18我们说一个正当的原游戏e∈应用A满足可见性当eJqa[b]eJJqJb[c]≤e时，意味着：• 如果λA（q）=P，则qa[b]=EJqa[b]EJJ• 如果λA（q）=O，则qa[b]≠eJqa[b]eJ J。将此与[23]中更非正式的可见性定义进行比较。2.1]：一个格式良好的序列s是合法的，或者是合法的位置，如果它也满足以下可见性条件：• 如果tm ± s，其中m是P移动，则m的调整器出现在t '中。• 如果tm ± s，其中m是非初始O移动，则m的调整器出现在t '中。这里的困难是，采取的看法删除移动从发挥，因此需要一个复杂的重新索引，如果指针是正式使用整数。在视图中找到移动的合理性并不简单。可见性是微妙的，典型的纯语言或只有接地类型状态。我们已经在上面展示了如何在我们的框架中将其形式化，但是对于涉及可见性的属性的证明并不简单，因为除了名称和绑定的处理之外，其他原因，所以我们将不再进一步考虑这个属性注2.19我们现在可以计算HO博弈（[19]中的博弈）和GM博弈（[14]中的博弈）的策略。假设A是一个竞技场，e∈pplyA是一个原型游戏。然后又道：• 在HO-博弈中，当fa（e）={a}，对于某个a∈ A，e是正当的，良好的开放，交替的，严格嵌套的，满足可见性时，e是合法的博弈（见[19，定义4.2，定义4.2]）。4.4]）。• 在GM博弈中，当fa（e）={a}时，e是合法的博弈，如上所述，e是正当的，[14][15][16][17][18][19][1条件fa（e）={a}意味着e有一个自由原子a;一个“悬挂指针”。通过良好的开放性，这确保了初始问题的名称如何选择一个以上的？我们没有。这是一个不明显的设计决策，4函数e∈e不是全函数，因为它没有定义在形式为ia[b]e′的e上，其中λA（i）=P. 然而，由于ia[b]e′，其中λA（i）=P是不正当的，所以在所有正当的e上定义了λ e。180M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173在共同抽象的原子上，原剧本没有α-转换。 这就保留了组合性：如果[a] a等于[b]b，那么[a] ab等于[b] bb，这是无意义的。[5]在我们的框架中，α-转换存在于策略（原型策略集合）中，这些策略服从于等变（对称）条件，直到它们所包含的原型策略中的原子被选择为止所以α等价并不存在于元素中，它存在于元素的集合中。关于这一点，请参见备注5.3。3对戏剧3.1从一出戏中删除走法我们经常想从指针序列中删除移动，这反映但是指针进出删除的移动需要更新。定义3.1和命题3.4使我们的名义框架形式化。这一小节的最终结果是定理3.11，它使用命题3.4和其他构造来表明原剧本的性质通过删除而保持。定义3.1假设XmvsA是从竞技场A开始的一组移动，e∈pplyA.在e上归纳地定义删除e]X如下，其中我们归纳地取（f，ρ）=e]X：ε]X=（ε，id）（ema[b]）]X=（fmρ（a）[b]，ρ）（m/∈）X（ema[b]）]X=（f，ρ[b：=ρ（a）]）（m∈ X）对于π1（e]mvsA），也就是说，对于A的移动集合的删除，写e]A将是方便的。这里π1是第一个投影。注释3.2直觉]X是当我们这样做的时候，一些重新索引必须发生：例如，如果qa[b]被删除，那么任何指向b的指针都会被]X=在上图中，阴影节点（圆圈）位于X中，并被删除。e]X归纳地生成我们很容易把ρ当作一个副产品而忽略掉，但ρ可能是更重要的信息，因为f可以从ρ和X计算出来。这是命题3.4，它是定理3.11的一个很好的证明的关键。定义3.3假设e∈pplyA且X ∈mvsA。我们定义朴素删除e-X如下：[5]通过附加一个“未来置换”，可以使α-转换与原剧本相一致，如[a]π。[a]ida等于[b]（b a）b，而不是[b]idb。这里不需要这个M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173181XX·ε-X =ε（ema[b]）-X=（e-X）ma[b]（m/∈）X（ema[b]）-X=e-X（m∈ X）命题3.4假设e∈ppl yA且e]X=（EJ，ρ）. eJ=（ρ·e）-X. 6通过对e的归纳证明。 我们考虑有趣的情况（它改变ρ）：• 当 m ∈ X 时 ， ema [b] 。 设 e]X= （ eJ ， ρ ） . 利 用 归 纳 定理 （ ema[b] ） ]X=（（ρ·e）-X，ρ[b：=ρ（a）]）.N ow（ρ·e）-X=（ρ·（ema[b]））-X，因为m∈X. 由于定义2.8 b / a ∈ toms（e）（定义2.3）中的假设，因此ρ·e=（ρ[b：=ρ（a）]）·eb。七问引理3.5enable ed（ρ·e）=ρ·enable ed（e）。作为一种直接的计算方法，enabled（ρ·e）-X=（ρ·enabled（e））-X。现在我们来考察删除对定义2.15的合法性条件的影响。合法性不能通过任意删除来保持，但删除通常以一种受控的方式使用，以确保保留。例如，删除在竞技场中形成整个子树的移动，保留合法性属性。其他类型的删除可以类似地处理引理3.6假设X ∈ mvsA且e ∈ pplyA。 记e]X =（f，ρ）. 则fa（f）fa（e）和ca（f）<$p·ca（e）.引理3.7设e ∈ pplyA. 如果ma ∈ enabled（e），则a ∈ atoms（e）。证明通过使用定义2.12对原游戏e进行常规归纳。Q引理3.8若ma [b] ∈ pplyA且mJb ∈ enabled（e）则m ∈AmJ.通过对e的归纳证明。 我们考虑一种情况：• 案例e ma [b]. 假设mJb ∈ enabled（e ma [b]）。 通过定义2.8b/∈atom s（e）和by引理3.7mJb/∈enabled（e）中的假设。根据定义2.12，可以得出mAmJ。Q定义3.9当m∈X且m<$AmJ意味着MJ∈ X。引理3.10假设X mvsA在A下闭。 设e]X =（eJ，ρ）. 则如果ma∈enableed（e）且ma/∈X，则mρ（a）∈enableed（eJ）。通过引理3.5证明：如果ma∈enabled（e），则mρ（a）∈使能d（（ρ·e）-X）。我们通过对e的归纳来研究，并考虑一种情况：[6] ρ e是一个名义序列，但它可能不是一个原型序列，因为共同抽象的原子不需要是不同的。也不一定是合法的，因为单纯的删除不会更新链接.命题3.4表明，定义3.1计算了ρ和， 使得如果我们一起做这两个朴素运算，那么我们都是正确的。[7]这是证明的关键：因为b是新的，把ρ改为ρ[b：=ρ（a）]并不会改变我们迄今为止所计算的任何东西。182M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173• emaJ [a]的情况。记e]X =（eJ，ρ），假设mJa ∈ enabled（emaJ [a]），mJ/∈。X通过引理3.8mAmJ. SincemJ/∈X，它遵循X的y闭包，A表示m/∈。XSo（ρ·（emaJ[a]））-X=（（ρ·e）-X）（mρ（aJ）[ρ（a）]）. 根据定义2.12，mJρ（a）∈enabledd（ρ·e）-X）（mρ（aj）[ρ（a）]））.Q定理3.11设X =（f，ρ）.(i) 如果X mvsA在A下是闭的，那么如果e是正当的，那么f也是。(ii) 如果iniA<$X =<$，那么如果e是良开的，那么f也是。(iii) 如果e是严格限定作用域的，那么f也是(iv) 如果X mvsA在A下是闭的，那么如果e是严格嵌套的，那么f也是。证明(i) 其中e]X=（f，ρ）andm/i∈niA. 利用命题3.4FJMρ（b） =（（ρ·EJ）-X）mρ（b），对所有的som/∈，EJmb≤e.如果XSince是正当的，则由引理2.13，对于某个qa[b]e，q必须是q<$Am。由于X在下是闭的，所以Awenowq/∈。由命题3.4可以得出qρ（a）[ρ（b）]≠J，我们就完成了。(ii) 通过一个简单的论点使用命题3.4。(iii) 设aρ（a）fJ<$f。 则aaeJ∈ a，对某个eJ∈ p。 由于e是严格scop ed的，我们知道a/f∈a（EJ）。 根据引理3.6，a/f∈a（fJ）也成立。(iv) 就像前一个案例一样。Q3.2对遗传正当化子博弈的限制本小节的结构类似于第3.1小节。我们有一个比删除更复杂的操作;提取遗传公正的子指针序列。在我们的框架中，定义是绝对常规的;我们只是取一个子序列。这是定义3.12;然后命题3.14展示了如何使用名称快速计算相关的子序列，定理3.18表达了如何保持性质。定义3.12假设e∈p plyA且A∈ A。定义遗传正当的原游戏eTA，其中我们取（f，B）=eTA，a∈B，AJ/B∈：εTA=（ε，A）（ema[b]）TA=（fma[b]，B<${b}）（emaJ[b]）TA=（f，B）定义3.13假设e∈p plyA且A∈ A。 定义e@A如下，其中a∈A和aJ/A∈（来自[12]的与原子的接触关系被描述）：ε@A=ε（ema[b]）@A=（e@A）ma[b]（emaJ[b]）@A=e@A命题3.14如果eTA =（f，B）则e @ B = f。M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173183推论3.15设eTA =（f，B）。然后又道：• 如果fJma [b] ≤ f，则存在eJ使得eJma [b] ≤ e且（eJma [b]）@ B = fJma [b]。• 如果aa [b] fJ <$F，则eJ存在，使得aa [b] eJ<$e且（aa [b] eJ）@B=aa [b]fJ。• 如果qa[b]f2qJb[c]f3ab[d]<$f，则e2和e3存在，使得（qa[b]e2qJb[c]e3ab[d]）@B=qa[b]f2qJb[c]f3ab[d]。推论3.16如果eTA=（f，B）则{mb∈enable ed（e）|b∈B}=enabledd（f）.推论3.17fa（e @ B）= fa（e）<$B和ca（e @ B）= ca（e）<$B。定理3.18设eTA=（f，B）. 如果e是公正的/良好开放的/严格作用域的/严格嵌套的，那么f也是。我们依次考虑每个属性• 公正。使用推论3.15和推论3.16的第1部分。• 开得好使用推论3.15的第1部分。• 严格的范围。从推论3.15和推论3.17的第2部分。• 严格嵌套。第三部分推论3.15。Q4组合竞技场定义4.1（i）设f是集合X上的函数，g是集合X上的函数，不相交Y 写[f，g]为X上的配对函数，使得 [f，g]（x）=f（x），[f，g]（y）=g（y）.(ii)假设g是{O，P}的函数。将x映射到g（x）的函数写成g(De定义2.7）。定义4.2通过下式定义竞技场的乘积A×B和箭头A×BA×B=（qstA+qstB，ansA+ansB，[λA，λB]，<$A+<$B，iniA+iniB）A<$B=（qstA+qstB，ansA+ansB，[λA<$，λB]，<$A+<$B+iniB×iniA，iniB）• 在上面，符号+表示不相交的集合并（为了方便起见，假设不同竞技场的移动集合是不同的），并且• iB×iA={（iJ，i）|iJ∈in iB，i∈in iA}。 SoA+B+in iB×in iA是A和B的使能关系的不交并，不交并iniB×iniA.我们展示了如何从A/B中的原始戏剧中恢复A中的原始戏剧，B. 这是引理4.3和4.5。这两个重要的操作原型策略--删除和分解--保留了某些形式良好的属性，这些属性定义了HO和GM法律策略的概念。这些业务是制定战略组成的关键，因此，保持合法性对于表明总部或总经理战略的组成是明确界定的至关重要引理4.3设e∈pplyA <$B且e]mvsA=（f，ρ）.则f∈pplyB.如果e是正当的、良好开放的、严格作用域的或严格嵌套的，那么f也是184M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173对于第一部分，通过命题3.4，f只包含mvsB中的移动。第二部分遵循定理3.11，并且我们注意到，限制于运动mv s B的使能关系ΔAΔB恰好是ΔB。Q定义4.4通过unravel（e）={eT{a}定义e ∈ p ply A的unravel|a ∈fa（e）}。解开是构建指数博弈的关键[23，Sec 2.4]。直觉上，在A和B的一局棋中，我们可以通过删除A的棋步来恢复B的一局棋。移除B中的移动产生A的交错的一组打法。解开通过以下指针将这些游戏分开，如图所示：T={，}很容易看出，如果e是正当的，那么unavel（e）就抓住了“e中的线程集”的概念引理4.5如果e∈pplyA <$B则unavel（e]B）<$pplyA。如果e是公正的/开放的/strictly-scoped/strictly-nested，那么每个f ∈ unavel（e]B）都是如此。直接从引理4.3证明。Q5战略5.1策略与等方差定义5.1当e∈σ对每个置换π都蕴含π·e∈σ时，称σ∈pplyA为等式。记σ：A，当σ是pA的等变子集时，称σ为策略。(The战略的概念通常受到进一步的限制;这些限制将在下面讨论。从定义3.1中删除e]A。我们遵循[23，2.2.3节]：定义5.2假设A、B和C是不相交移动的竞技场。然后，对于策略σ：A <$B和τ：B<$C，定义它们的相互作用和组合为：||τ ={e ∈ PplyA×B×C|e]C ∈ σ <$e]A ∈ τ}σ; τ ={e]B |e ∈ σ||τ}这是策略组合的线性版本;指数博弈是使用前面介绍的解开概念（定义4.4）构建的。 使用几乎没有结构的原型游戏，简化了互动的定义（-||与通常的定义相比（cf。[23，第2.2.3节]），这需要相互作用序列的辅助概念。注5.3等变性是置换原子下的对称性。命名fulfill链接fulfill的函数，例如[19，23，14]。策略的置换对称性相当于说M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173185JJ因此，在我们的框架中，原型游戏不具有α-等价性，但原型游戏集具有α-等价性。[10]）。这样，定理5.4就变成了一个由对称性/等变性的单线论证。这避免了关于α重命名、重索引或重链接的争论，如果我们使用数字或显式链表，则需要这些争论所以我们有：定理5.4设A、B和C是竞技场，σ：A <$B和τ：B <$C是策略。 而在《易经》中，则是一种“道”，一种“道”，一种“道”。通过定义5.1证明一个策略是一个等变的原型集，所以σ和τ是等变的。我们注意到，指定σ;τ所涉及的定义在原子中都是对称的，因此通过假设，这些定义的输入是σ和τ，因此根据等方差原理，σ;τ也是对称的。（关于等方差的正式讨论在其他地方[7，4.2小节Q5.2合成的结合性我们将证明定理5.5，策略的合成是结合的：定理5.5假设A、B、C和D是不相交移动的竞技场。假设σ：A <$B、τ：B <$C和μ：C <$D是策略。 然后（σ; τ）; μ = σ;（τ; μ）。这将直接从引理5.8得出。对我们来说，在本文中，策略只是一系列的移动和名称序列，证明只是通过常规归纳和名称追踪，即：拆开定义并注意名称在等式两侧的相同位置结束（见命题5.6的证明）。命题5.6假设C是一个竞技场，X，Y是两个不相交的移动集合，e∈pplyC。设e]X=（eJ，ρ），eJ]Y =（eJJ，ρJ），e]（X <$Y）=（f，ρ）.则f = eJJ和ρJJ= ρJ <$ρ（其中<$是函数复合，记法来自定义2.5）。通过使用定义3.1对e进行归纳证明。• 案件ε…很容易.• 当 m ∈ X时，ma[b]的 情形.根据 命题3.4EJ=ρ·e-X 和 EJJ=ρJ·E-Y. e_（ JJ ）= （ ρJ<$ρ）·e-（X<$Y）。 也可由命题3.4得到f=ρJ J·e-（X<$Y）。通过归纳假设f=eJJ和ρJJ=ρJ<$ρ。根据定义3.1，我们有ema[b]]X=（eJ，ρ[b：=ρ（a）]），由此得出π1（ema[b]]X）]Y=（eJJ，ρJ<$（ρ[b：=ρ（a）]））。此外，函数的事实是ρJ<$（ρ[b：=ρ（a）]）=（ρJ<$ρ）[b：=（ρJ <$ρ）（a）]。使用定义3.1，我们有ema[b]]（X <$Y）=（f，ρJJ[b：=ρJJ（a）]），结果如下。• 当m∈Y时，e ma [b]。类似于前一种情况，但更简单。Q注5.7我们的策略概念很简单，它不依赖于合法博弈的概念因此，为了研究合成的性质，在竞技场A×B上的任何策略也是在竞技场A × B上的策略，因为两个竞技场具有相同的移动集合-移动的极性和正义结构是不同的186M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173在A×B和A×B之间，但这个信息并不用于组成的定义。同样，定义σ||策略σ：A <$B和τ：B <$C的τ。为了方便起见，一个交互作用可以被看作是（A×B）×C或A×（B×C）中的一个策略这是正确的，因为交互作用保持了等方差，并且这些领域中的移动集合是相同的。这样，我们将得到一个关于相互作用结合性的特别简单的证明，如下所示。引理5.8假设σ：A <$B、τ：B <$C和μ：C <$D是策略。 则（σ||τ）||μ =σ||（τ ||μ）。证明我们反复解压缩定义5.2：e ∈（σ||τ）||μ当且仅当e]D ∈ σ||τ和e]A×B∈ μ，当且仅当（e]D）]C ∈ σ和（e]D）]A ∈ τ和e]A×B∈ μ. 使用命题5.6，这等价于e]D×C∈σ和e]D×A∈τ和e]A×B ∈μ。通过类似的推理，eJ∈ σ||（τ ||μ）等价于EJ]D×C∈ σ和EJ]D×A∈ τ和EJ]A×B ∈μ.结果如下。Q5.3前闭和后闭正如原型剧一样，GM和HO策略也受到限制。在本节的其余部分中，我们将简要介绍（有时是详细介绍）如何表达这些内容关于策略的两个标准条件是预闭和对手闭;参见[19，第5节]（其中对手闭被称为偶然完备性）或[14，定义4]。这些都是简单的形式化：定义5.9在下列情况下，分别将σ应用A称为prefix-closed和prefix-closedema[b]∈σe∈σe∈σ λA（m）=Oema[b]∈pplyAema[b]∈σ5.4原型剧的预订购在[14]中，作者对异步并发建模感兴趣相应地，策略必须在特定的移动交换下饱和[14，Subsection 2.5]（这个想法可以追溯到[25]）。定义5.10当e≤eJ蕴涵ef≤eJf且fe≤feJ时，称序列上的关系≤相容。定义≤onp plyA为最小相容预序，使得：（b/f∈a（e），λA（m）=O）（bmX）（b/f∈a（e），λA（m）=P）（bXm）ma[b]e≤ema[b]ema[b]≤ma[b]e当e∈σ，EJ∈pplyA且EJ≤e蕴涵EJ∈σ时，称σ∈pplyA≤-饱和.注释5.11为了与定义5.10进行比较，可能值得引用[14]中的定义（定义6之前的文本）：M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173187的1B2年q1Q22的1Q 2年q1... 我们定义了一个在任意区域A上的预序≤作为最小自反传递关系，对于所有s，SJ∈ play A，满足sj ≤ s(i) sJ=s0·o·s1·s2且s=s0·s1·o·s2，或(ii)SJ=s0·s1·p·s2和s=s0·p·s1·s2，其中，o是任何O移动，p是任何P移动，s中的调整指针是从s j.名词序列有助于使这些直觉形式化。在[14，引理7]中给出了一个小步长形式≤J，并证明了等式≤J=≤.根据我们目前所知，这是一个常规的归纳论证：定义5.12给{O，P}一个偏序使得O ≤ O，O ≤ P，且P ≤ P。定义闭序列上的一个前序≤J为最小自反传递关系，使得：（λA（m1）≤λA（m2））（smm）m1a1[b1]m2a2[b2]≤Jm2a2[b2]m1a1[b1]（λA（m1）≤λA（m2））（smmJ）m1a[b1]m2a[b2] ≤Jm2a[b2]m1a[b1]下面是针对q1，q2解释的异步交换规则（smm）：引理5.13≤J=≤。a2b1a2bb1C证明我们通过对≤J的归纳证明了≤J<$≤：• 规则（s mm）。如果λA（m1）= 0，则由（bmX）生成;如果λA（m1）= P = λA（m2），则由（bXM）生成。• 规则（s mmJ）。如果λA（m1）= 0，则由（bmX）生成;如果λA（m1）= P = λA（m2），则由（bXM）生成。在两种情况下，边条件b2/f∈a（a1a1）是svalid. 通过对≤和e的长度的归纳，可以得到Nextweshowwthat≤ n ≤J：• 规则（b m X）。我们使用（smm）和（smmJ）将ma[b]与最左边的移动交换e. 条件b/fa∈（e）满足区别条件b2/∈{a1，，ab1}.• 规则（bX m）。我们使用（s mm）和（s mmJ）将ma [b]与最右边的移动交换在大肠Q5.5无罪HO博弈中的一个重要概念是无辜性[19，定义5.2]，它表征了无边约束的顺序计算。对我们来说，这是定义5.14，使用我们迄今为止构建的工具，它非常紧凑：8定义5.14假设m和mJ是指定的移动（定义2.9）。给定A中的HO-合法策略emmJ，eJm，其中|埃姆J|具有偶数长度，ca（mJ）atoms（eJ）=[8]我们使用McCusker的等价公式[23，2.2.4小节]。188M. Gabbay，D.Ghica/Electronic Notes in Theoretical Computer Science 286（2012）173和emCJ∈ca（EJ）使得em MJ' = ejm（ρ ·mj）'. Callσ：Ainnocentwhenem mJ，eJ∈σ<$eJm HO-合法的<$e m' = e j m ' =<$e j m（ρ · m j）∈ σ.在[19，定义5.2]中，Hyland和Ong必须用英语写指针的操作，并且这必须在他们的整个工作中完成（这是类似论文的典型）。我们提出名义技术作为一种快速和优雅地处理这个问题的方法。在HO游戏中，移动可以重复，这导致需要识别序列中移动的特定出现。这在我们的设置中消失了，因为每个问题或答案都由一个名称唯一标识：它引入的共同抽象名称。因此，在我们的框架中隐含的是“移动”与“发生”的分离在这篇论文中，我们已经能够隐含地将原游戏中的一步棋的出现与出现该步棋的命名步棋相识别，因为原游戏中的共同抽象原子是不同的（定义2.8）。6结论我们已经看到了指针序列是如何被建模为名义序列的。指针被分成一个对应于箭头头部的coabstraction [b]和一个对应于箭头尾部的（自由）原子b与指针不同的是，名称带有它的标识;b指向我们放置它的任何地方此外，与例如数字不同，名称是置换对称的，因此重新索引/重命名可以在高抽象级别上表达。正因为如此，名义序列很容易分解、组合和重新索引。我们已经考虑了一些非平凡的操作，如删除和遗传