无限迹等价问题的解决：基于博弈语义的不确定性程序识别模型

理论计算机科学电子笔记155（2006）467-496www.elsevier.com/locate/entcs无限迹等价保罗·布莱恩·利维1英国伯明翰大学摘要我们解决了一个长期存在的问题，通过提供一个指称模型的不确定性程序，识别两个程序，如果他们有相同的可能行为范围。我们讨论的困难与传统的方法，发散是底部或一个术语表示一个功能，从一组环境。我们看到，以游戏语义的方式使强制明确，使我们能够避免这些问题。我们首先对一个具有顺序I/O和无界非确定性的一阶语言进行建模（使用这种方法，建模并不比有限非确定性更难）。然后，我们扩展的语义，高阶和递归类型，适应早期的游戏模型。传统的充分性证明使用逻辑关系是不适用的，所以我们使用一种新的隐藏参数。保留字：非决定论，无限迹，博弈语义1介绍1.1问题考虑以下call-by-name2语言的可数不确定性命令：M：：=x|普兰特角M|μx.M|选择n∈N。Mn其中c的范围是某个字母A。我们定义二元非决定论M或MJ从可数的明显的方式。1电子邮件：pbl@cs.bham.ac.uk2意味着标识符被绑定到一个未求值的项。1571-0661© 2006由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.11.069468P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467一个闭项有两种表现方式：打印有限多个字符然后发散，或者打印有限多个字符。当两个封闭项具有相同的可能行为范围时，它们被称为无限迹等价正如[15]中所说，“我们[…]“欲使其有所欲”，“欲使其有所欲”。一些非确定性模型，如各种幂域[15]和发散语义[18]，识别不是无限迹等价的程序，所以它们太粗糙了。其他算法计算内部操作[2，4]或包含分支时间信息，因此它们对于这个问题来说太精细了（充其量）在本文中，我们提供了一个解决方案，并看到它不仅可以用于建模上述语言，而且还可以用于建模无界非确定性，输入（遵循请求），以及高阶，求和和递归类型。我们的模型是指针博弈语义的一种形式[8]，尽管指针博弈技术只需要用于高阶类型。这很好地说明了游戏语义学的力量和灵活性。证明包含高阶、求和和递归类型的模型的计算充分性是一个困难，因为传统的使用逻辑关系的方法不适用于它，所以我们给出了一个使用隐藏方法的证明。作为一个副产品，我们得到了一个非常简单的证明FPC [13]的博弈模型的充分性1.2为什么要明确强制？在转向我们的解决方案之前，我们考虑两种已经研究过的语义在这两种情况下，假设字母表都是单例{C}。(i) 最小发散语义是指一个项表示偏序集的元素，每个构造都是单调的，并且[μx。x]表示最小元素x。例子是Hoare，Smyth和Plotkin powermain语义[15]，[17]中的所有CSP语义，以及[6]中的游戏语义发散-最小语义不能在有限迹等价中建模，下面的论点取自[15]。(We将打印C替换为C。）放 M= 拉瓜尔角C. ⊥MJ= 拉瓜尔角拉瓜尔角C. ⊥然后 M = λ或λ或C。C. n≤MJM= 拉瓜尔角C. 拉瓜尔角C. ⊥MJ因此M=MJ，在有限迹等价中矛盾。这个论证只使用了二元非决定论。P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467469(ii) 一个明确的语义是（粗略地说）一个术语表示来自环境集合的函数。例如，3个幂次主语义[15]，[17]中的所有CSP语义，[2]中使用无限迹的语义和发散语义[18]。一般来说，良好指向的语义适合于满足上下文引理性质的等价：在每个环境中等价的术语在每个上下文中都是等价的。然而，无限迹等价并不满足这个性质，正如下面两个涉及x的项3所证明的：N =（选择n。Cn.μz。z）或xNJ=（选择n。Cn.μz。z）或C. X一方面，N和NJ在任何环境下都是无限迹等价的，因为C是唯一的字符：封闭式术语N[M/x]NJ[M/x]可以打印Cn然后发散可以打印Cω是的iM可以打印Cω是的iM可以打印Cω另一方面，它们在上下文中并不等同：封闭式术语μx.Nμx.NJ可以打印Cn然后发散可以打印Cω是的没有是的是的所以任何无限迹等价的模型都必须区分它们。（为了避免读者认为是无限的非确定性，假设我们只允许二进制非确定性，但将N索引的命令放入语言中。 然后定义选择n∈N.Mn为（μfλn. （Mn或f（n+1））0，它要么执行一些Mn，要么发散[15]。用这个代替如果n∈N，则会出现同样的问题3被A发现W. 罗斯科在1989年 [个人通信]，并独立在[10]。470P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467区分N和NJ的一种简单方法是说NJ能够打印一个滴答，然后强制（即，execute）x，而N不是：含xNNJ可以打印Cn然后发散是的是的可以打印Cω没有没有可以强制x是的没有可以打印C，然后强制x没有是的可以打印Cn+2，然后强制x没有没有这就是我们的解决方案。当一个按名称调用的程序强制其（thunk）参数时，模型应该显式地表达这种想法，这种想法在游戏语义中存在（通常是隐式的），其中（如[11]中所讨论的这就是为什么我们的解决方案适合游戏框架。然而，在文献中的游戏模型是最小的分歧，这一属性是利用充分性证明使用逻辑关系。这甚至适用于[6]的非确定性模型，其中策略集被Egli-Milner前序所约束，因此它们成为cpos。本文的新颖之处在于它避免了这种重复。例如，考虑两个（按名称呼叫）术语P= λx。（diverge orifx then（ifx then true else true）elsetrue）PJ= λx。（diverge or（ifx then diverge else true）ifx then（ifx then true elsetrue）类型为bool→bool在[6]中，这些项具有相同的外延，并且对于may和must检验，在观测上确实是等价的但是如果我们把印刷术加入到语言中，C [·] =[·]（C. （true）现在C[P]可以打印一个记号，然后发散，而C[PJ]可能不会。因此，从无限迹等价的观点来看，P和PJ必须有不同的表示。我们将看到，在我们的模型中就是这种情况1.3论文结构我们将1.1节的语言扩展为三个阶段。首先，在2.1节中，我们引入了任意元数的不稳定（也称为内部）选择算P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467471子，这迫使我们考虑有限迹和无限迹。472P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467其次，在2.2节中，我们添加了请求输入，例如打印请求，如请输入您的姓名，然后等待用户输入字符串。这种类型的I/O对于初学程序员来说很熟悉。在这个阶段，我们仍然可以给出一个非技术的指称语义-我们在第二节中这样做2.4.第三个扩展，在第三节，是提供高阶和递归类型。在建模之前，我们在第4节中介绍了指针游戏的基本结构，我们在模型中使用了这些结构。1.4相关工作：数据流网络数据流网络的无限迹模型-包括反馈，但不包括递归-在[9]中提出，并完全抽象。在[7]的术语中，它形成一个笛卡尔中心跟踪对称么半群范畴。虽然在[7]中表明，这样一个范畴，如果是中心封闭的，可以可以转换成一个递归模型-在某种意义上-这在这里是没有用的，因为Jonsson的模型不是中心封闭的（就这一点而言，它的有限追踪变体也不是。）确认我感谢马丁·埃斯卡德和盖伊·M·C·D·E·2一阶语言2.1不确定的选择和全错在这一节中，我们扩展了1.1节的语言，允许任意元数的选择算子但是空arity带来了一个问题：一个包含“选择空集的一个元素”命令的语言为了避免这个问题，我们引入了全错误的概念：如果u是编程语言的全错误，那么任何程序在任何时候都可以通过打印全错误消息u来中止。定义2.1一个不稳定的签名是一族集合{Ph}h∈H。它是无死锁的关于一个集合U的omni-errors时，要么所有的PH是非空的或U是非空的。任何这样的{Ph}h∈H-与字母表A-一起确定一种语言L（Y，A）在其中对于一个chh∈H，t是一个选择eh{Mp}p∈Ph的连续结构，P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467473随机选择p∈Ph，然后执行Mp。语法M：：=x|普兰特角M|μx.M|选择h{Mp}p∈P对于每个上下文r = x0，.，xn−1，我们定义一个可终止的LTS L（Y，A，Γ），其标签为A {τ}。它的态是项ΓM，它的终态是自由标识符。过渡是τμx.M~M[μx.M/x]选择eh{Mp}p∈Pτp<$$ >（p<$∈Ph）H ~MC普兰特角M~ M给定全误差s的集合U，对于每个封闭项M，我们都给出M~u且u∈U。通常，U是空的，在这种情况下，不会发生全方位错误但如果Ph是空的，对于某个h∈H，则程序chooseh{}除了引发全错之外没有其他行为如果U也是空的，那么程序根本无法运行（死锁）。在本文中，我们只研究无死锁的情况。这种语言的程序可以有三种行为方式：(i) 打印许多字符，然后发散(ii) 打印无限多个字符(iii) 很多人都认为，这是一个错误，一个错误，一个错误。对于一个闭项M，让我们写[M]U<$（A<$+Aω）+A<$ ×U作为可能行为的集合。我们把无限迹等价定义为[−]U的核。明确[M]U=[M]inf+[M]fin×U其中[M]inf<$A<$+Aω是类型（i）-（ii）的行为的范围，[ M ] fin<$A <$是M的有限迹的让我们把[M]写成对（[M]fin，[M]inf）。命题2.2（i）对于某些无死锁签名和字母表，无限迹等价严格比[−] inf的核更精细。(ii)对于所有无死锁的签名和字母表，无限迹等价是[−]的核心。证据 （i）考虑C. 选择h{}并选择h{}，其中Ph为空。（2）由于无死锁，每一条有限的道路都延伸到一条无限的道路或以一个全错为终点Q号提案2.2（ii）合法地将全错排除在无限迹等价的语义之外（在无死锁的情况下），只要我们包括H474P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467O无限的痕迹。2.2请求输入对于第二种扩展（见1.3节），我们定义一个I/O签名为集合族Z={Io}o∈O。每个o∈O都提供一个构造输入o{Mi}i∈I，它打印o，然后等待用户提供一些i∈Io，然后执行Mi。我们说Z是可数的，当O和每个IO都是可数的。定义一个特征性Z，我们将RZ记为Set映射X的闭函子到o∈OXIo。我们在Sett上得到了一个强单子TZ（在Sett上的自由单子RZ）A到μY的映射。（A+RZY）。 这个单子可以用，以这种方式[14]，以模拟所请求的输入。请注意，这包括[14]中指定为“交互式输入”，“交互式输出”和“异常”的monad作为特殊 因此，我们将每个输出c∈ A视为一个元素O，使得Io= 1，我们考虑printc。M作为语法糖4，用于输入c{M}i∈1。2.3双标记转换系统为了描述一个使用签名为Z的请求输入的系统的行为，LTS（即，对于某个固定的动作集A，内函子P（A× −）的余代数）并不真正合适。行动应该是什么一方面另一方面，如果我们允许输出和输入都是动作，我们需要额外的交替和接受输入的条件。另一方面，如果我们将一个动作定义为一个对（o，i），我们就不会处理输出的输入永远不会到达（或者，实际上，输入集是空的）的情况。相反，我们使用以下概念（抽象，集合上的内函子P+RZ的余代数）。定义2.3（BLTS）设Z={Io}o∈O，U是全错集。(i) Z和U上的双标记跃迁系统（BLTS）L由以下组成：• 一组状态S，对于某个请求o∈O，每个状态都被分类为静默状态或o-状态-我们分别将静默状态和o-状态的集合写为Ssil和SO• 一个关系~fromSsil toS和一个函数SO×IO：S，o∈O。4读者可能会觉得这两件事之间有很大的区别，因为印刷品c。M打印c并立即执行M，而input c{M}i∈1打印c，然后在继续执行M之前等待响应，如果没有收到响应，它永远不会执行M。然而，这种差异似乎在外延上是无关紧要的，至少在顺序设置中是如此。P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467475它是无死锁的，如果每个静默状态至少有一个后继，或者U是非空的。(ii) 一个可终止的BLTS是相同的，除了有第三种状态：终端(iii) 当U为空并且每个静默状态恰好有一个后继时，可终止的BLTS是确定性的与LTS一样，我们可以获得状态的迹集。首先，我们需要将这些迹集描述为定义2.4（策略）设Z是一个I/O签名，V是一个集合。(i) 一个游戏是一个有限的或无限的序列o0i0o1i1. 其中or∈ O且ir∈Ior。Itawai tsPlaya yeriofevenlengthgth ， anddawai tso-input ifofodlengthending in o. 在Z上以V结束的游戏是等待玩家的游戏游戏扩展了V的元素。(ii) 在Z到V上的非确定性无限迹（NIT）策略是一个元组σ=（A，B，C，D），其中有限轨迹A是输入等待策略分歧的集合B是有限轨迹中的玩家等待策略的集合C是无限策略终止轨迹D是以V如果t在A、B、C或D中，则t的每个等待输入的前缀都在A中。(iii) 当t的每个等待输入的前缀都是σ的有限迹时，等待参与者的策略t与NIT策略σ是有限一致的。(iv) NIT策略σ=（A，B，C，D）是确定性的，• 任何与σ完全一致的等待玩家的策略至多有一个直接延伸到A或D中的策略，而在B中，它没有这样的延伸• 任何等待输入的前缀在σ中的无限游戏t都在C中。(v) 让我们成为一个球员等待发挥超过Z到V。一个从s开始的从Z到V的NIT策略是一个扩展s的策略集合σ=（A，B，C，D），使得这些扩展s的策略的所有有限前缀都在A中。我们为（iv）中的策略定义决定论(vi) （改编自[17]）NIT策略σ到V是无死锁的，当U是非空的，或者对于每个与σ有限一致的玩家等待 SJ，存在从 SJ开始的确定性策略τ，使得τ<$σ。(vii) 我们将Z上所有NIT策略的集合TUZV写为V死锁-476P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467免费的WRTU。(Thus，如果U非空，则它将由Z上的所有NIT策略组成。显然，TUZ是集合上的一个强单子。这里有一些关于策略的操作定义2.5（i）对于d∈V，我们定义ηd（单子（二）（{}，{d}）给定一族策略{σi}i∈I，其中σi=（Ai，Bi，Ci，Di），我们写i∈Iσi对于策略（i∈I阿ii∈IBi， i∈ICi， i∈IDi）(iii)给定o∈O，对于每个i∈Io，一个策略σi=（Ai，Bi，Ci，Di），我们写输入o{σi}i∈I减灾战略（{o} {ois|i∈Io， s∈Ai}，{Ois|i∈Io， s∈Bi}，{Ois|i∈Io， s∈Ci}，{Ois|i∈Io， s∈Di}）命题2.6（i）确定性策略在任何集合上都是无死锁联合(ii) 输入o保持确定性，并保持任何集合的无死锁性联合(iii) 如果I或U非空，则i ∈ I保持U的无死锁性。定义2.7（BLTS到策略）设Z是I/O签名，设L是Z上可终结的BLTS。 写V为它的一组终端状态。(i) 对于每个状态d∈S，对于策略（A，B，C，D），我们写[d]L，或者只是[d]。其中等待播放的输入so（分别为发散s，无限播放s，终止迹sv）在A（分别为B，C，D）i有一个从D到某个O状态的转换序列（分别为从d开始的无限序列，从d开始的无限序列，从d到v的转换序列），其非无声动作的序列是s。(ii) 当[d] =[dJ]时，两个状态d和dJ无限迹等价命题2.8设d是可终止BLTS L/Z中的一个状态。OP.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467477hoHHoo(i) 如果L是确定性的，那么[d]也是。(ii) 如果L对于U是无死锁的，那么[d]也是。命题2.9设d是Z上可终结BLTS中的一个状态。• 如果d是一个o-sttethen[d]=inputtoo{[d：i]}i∈I，• Ifdisasilenttatethen[d]=d~dJO[dJ]• 如果d是终端状态，则[d] = ηd。2.4操作语义和指称语义现在我们可以讨论第二个延伸了（见1.3节）。 设Y={Ph}h∈H是对U无死锁的不稳定签名，Z={Io}o∈I是I/O签名.这些定义了一种语言L（Y，Z），其语法由下式给出：M：：=x |选择h { M p } p ∈ P|chooseh{Mp}p∈P |输入o{Mi}i∈I对于每个上下文r = x0，.，xn−1，我们将项的集合写成L（Y，Z，Γ），我的天此集合是Z上的可终止BLTS，无死锁wrtU，其中• 每个标识符都是终端• μx.M是沉默的，并且μx.M~M[μx.M/x]• 选择eh{Mp}p∈Pis is int，并对eachp∈Ph，选择eh{Mp}p∈P~Mpnt• 输入o{Mi}i∈I是一个状态，并且（输入o{Mi}i∈I）：对于each以下是一些琐碎的事情。引理2.10设Γ，x<$M和Γ <$N。 假设M不是x。(i) M是无声的，i <$M [N/x]是。此 外 ，如果M~MJ，则M [N/x]~MJ[N/x]。相反，如果M [N/x]~Q，则对于某个MJ，M ~ M j使得Q =MJ [N/x]。(ii) M是o-态i <$M [N/x]是，则M [N/x]：i =（M：i）[N/x]，其中i∈ Io.(iii) 对于每个y∈ Γ，我们有M = yi <$M [N/x] = y。由此我们可以推导出关键的结果：我们可以用合成的方式来刻画[−]：命题2.11在语言L（Y，Z）中，我们有(i) 若x∈Γ，则 [Γ<$x] =ηx(ii) [r]选择h{Mp}p∈Ph]=p∈Ph[rMp](iii) [Γinputoo{ΓMi}i∈Io]=inputoo{[ΓMo]}i∈Io478P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467O(iv) 如果r，x<$M，则[Γμx.M]=μ[Γ，xM]其中我们定义μ（A，B，C，D）为（{l0···ln−1lo|l0x ∈ D，. ，ln−1x ∈ D，lo ∈ A}，{l0···ln−1l|l0x ∈ D，. ，ln−1x ∈ D，l ∈ B}{l0···ln−1|l0x ∈ D，. ，ln−1x ∈ D，x ∈ D}，{l0···ln−1l|l0x ∈ D，. ，ln−1x ∈ D，l ∈ C}{l0l1 ···|l0x ∈ D，l1x ∈ D，. 且l0l1 ···是无限的}，{l0···ln−1ly|l0x ∈ D，. ，ln−1x ∈ D，ly ∈ D，y/= x}）(v) 若r，x<$M且 r<$N，则[Γ<$M [N/x]]=[Γ，x<$M]<$[Γ<$N]其中我们定义（A，B，C，D）=（AJ，BJ，CJ，DJ）为（A{llJo|lx∈D，lJo∈AJ}，B∈{llJ|lx∈D，lJ∈BJ}，C{llJ|lx∈D，lJ∈C J}，{ly|ly∈D，y=/ x} <${llJy|lx∈D，lJy∈DJ}）号提案2.11给了我们一个计算上足够的指称语义。命题2.12在命题2.11中定义的运算μ和μ保持了确定性，并保持了对任何集合U的无死锁性。2.5隐藏我们首先定义了隐藏在BLTS上的概念设Z={Io}o∈O和Z J={IJ}o∈OJ为I/O特征。定义2.13设L是Z+ZJ上的可终止BLTS。 ZJ在L中的隐藏，记为LTZ，是通过使每个o-状态（其中o∈ZJ）保持沉默，对每个i∈Io都有一个到d：i的过渡，从L获得的BLTS wrtZ。对于战略，我们必须从戏剧开始P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467479i∈Ioo∈O''O命题2.14设我们是一个关于Z + Zj的V的游戏。将策略wrt Z的sTZ写入通过抑制Z j中的所有I/O移动而获得的V。那么以下情况之一恰好成立：等待外部输入s和sTZ等待o-输入，其中o∈Z等待内部参与者s和sTZ等待参与者等待隐藏输入s等待o-输入，其中o∈ZJ，sTZ等待玩家外部饥饿的s是无限的，sTZ等待玩家。外无穷大s和sTZ是无穷大的外部终止s和s T Z是终止的（这里，“外部”指s TZ，“内部”指s）。这是证明了归纳有限播放，其中服从状态图等待o-输入（o∈O）等待o-输入（o∈O）o∈Oi∈I'v∈ V等待播放器终止这对于无限的戏剧来说是微不足道的。定义2.15给定进入VwrtZ +ZJ的策略σ=（A，B，C，D），隐藏σ，记作σTZ，是定义如下的策略wrtZ有限迹sTZ，其中s等待外部输入并且是σ发散的有限迹（1）sTZ，其中s等待内部参与者并且是σ发散的发散（2）sTZ，其中s是外部饥饿的并且是σ有限迹sTZ的无限迹，其中s是外部无限的并且是σ终止迹sTZ的无限迹，其中s是外部终止的并且是终止迹跟踪σ。命题2.16如果d是BLTS L中的一个状态，在Z+ZJ上，那么（[d]L）TZ=[d]（L<$Z）命题2.17给定签名Z和ZJ，480P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467Oηv是 ηvi∈I输入O{σ}σi是是（σiTZ）i∈I输入o{（σiTZ）}i∈I如果o∈Zi i∈Io⎩i∈Io（σiTZ）如果o∈ZJ其中每个σi都是策略wrtZ + ZJ。任何BLTS或策略都可以通过将隐藏应用于确定性来获得。命题2.18设Z为I/O签名。(i) 对于Z上的每个可终止BLTS L，存在I/O签名ZJ以及Z + Z j上的确定性可终止BLTS L J，使得L = L JT Z。(ii) 存在具有以下属性的I/O签名ZJ。对Z上的每个进入可数集V的无死锁策略σ，存在Z + Zj上进入V的确定性策略τ，使得τTZ = σ.证据（i）定义Zj以提供用于L的每个静默状态d的算子，其中，|d~dJ}。 通过将a_c_i_（ii）我们定义ZJ为具有两个运算符o和oJ的I/O签名，其中Ioisempty，并且IoJ=2max x（x=0，|Z|）的。Givenσ=（A，B，C），则x是U∈IoJF并在UA+B+C上进行了扫描。对于achi∈IoJ，定义一个确定的战略g㈠。如果i∈U，则g（i）是输入o{}。如果i∈U，则g（i）是Z+ZJ上的确定性策略：（{t|tawaitsOpponnt， t±s} {tmo|tawaitsOppon nent， t±s，tm/±s}，{s|这是一个问题，{s|（不确定）定义τ为确定性策略J输入{g（i）}i∈I（oJ）由此可知，τTZ=σ。Q在（i）中使用的操作称为unhiding。3按名称呼叫FPC再次，让Y=（{Ph}h∈H，U）是一个无死锁的不稳定签名，令Z={Io}o∈I是I/O签名。我们现在定义一种高阶语言OP.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467481hoLFPC（Y，Z）通过直接将L（Y，Z）与其类型与[13]相同，即：A：：=A + A|0 |A×A|1 |A→A|X| μ X.A这些项由下式给出（省略0和1的构造）：M：：= X|在M|INRM| πM|πJM| λx.M|MM|折叠M|展开M| pmM作为{inlx.N，inr x.NJ}|（男、女）| chooseh{Mp}p∈P|输入o{Mi}i∈I其中PM代表“模式匹配”。我们以标准的方式归纳地定义类型判断ΓM：B对于L（Y，Z），我们可以把它看作是LFPC（Y，Z）的片段，其中唯一的类型是0。我们在图1中给出CK-机器语义[5]。当我们处理一个术语时，我们保留了一堆上下文，类似于评估上下文。例如以将pmM求值为{inlx.N，inr x.NJ}，我们首先需要对M求值，因此项的其余部分-上下文pm[·]为{inlx.N，inr x.NJ}-被放置到堆栈上。稍后，当M已经被评估时，该上下文被从堆栈和使用。我们写Γ |BkK：C意味着K是在评估上下文T中的类型C的项的过程中可以伴随上下文T中的类型B的项的栈。这个判断在图2中归纳地定义。我们定义了一个由类型B、项ΓM：B和栈Γ组成的驻留在Γ C上的构形|K：C.对于Z和U上的可终止BLTS，我们写LFPC（Y，Z，Γ<$C），其状态是居住在Γ <$C中的配置，并且在图1中定义。它是无死锁的，因为Y是。注意：从形式上讲，所有术语都被认为是显式类型的。clutter，我们实际上还没有写类型。4指针游戏4.1指针游戏竞技场我们通过采用[13]的标准游戏语义来获得我们的CBN FPC模型-为了简单起见，省略了无罪，可见性和括号的约束，尽管后两者可以很容易地被简化-并以Def.2.4（ii）的方式删除非确定性约束。为了使sum类型的语义工作顺利，我们在表示中做了两个5 [1]中的按名称调用和类型的公式并不健壮，因为它只适用于482P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467初始配置以执行ΓN：CΓ NC无 C跃迁（我们省略了inr和πJ）ΓΓpmM作为{inlx.N，inrx.NJ}MBA+AJKpm[·]as{inlx.N，inrx.NJ}：：KCC沉默，~ΓΓinlPN[P/x]A+AJBpm[·]as{inlx.N，inrx.NJ}：：KKCC沉默，~ΓΓπMMBB×BJKπ[·]：：KCC沉默，~ΓΓ（N，NJ）NB×BJBπ[·]：：KKCC沉默，~ΓΓMNMBA→BK[·]N：：KCC沉默，~ΓΓλx.PP[N/x]A→BB[·]N：：KKCC沉默，~ΓΓ展开M MB[μX.B/X]μX.BK展开[·]：：KCC沉默，~ΓΓfoldNNμX.BB[μX.B/X]展开[·]：：KKCC沉默，~ΓΓ选择h{Mp} p∈PhMpBBKKCC沉默，~（p∈Ph）ΓΓ输入o{Mi}i∈IoMBBKKCCo-state，：=（∈I）终端配置（我们省略inr）Γ λx.PA→B无 A→BΓ （N，NJ）B×BJ无 B×BJΓ 在MA+AJ无 A+AJΓ 折叠MμX.B无 μX.BΓ XBK CFig. 1. 用于按名称调用FPC• 类型表示一个竞技场家族，而不是单个竞技场• 一个术语表示一系列玩家优先策略，而不是单个对手优先策略。例如，类型bool→bool将表示一个单例族，当两个玩家都需要遵循包围条件时。这里的重组避免了这个问题。P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467483Γ |C knil：CΓ |BkK：CΓ |B×BJkπ[·]：：K：Cr，x：AkN：Br，x：A<$NJ：B r |BkK：CΓ |A + AJkpm [·] as {inl x.N，inr x.N J}：：K：C中文（简体）Γ |BkK：CΓ |A→Bk[·]N：：K：CΓ |B [μX.B/X]K：CΓ |μX.B展开[·]：：K：C竞技场图二. 按名称调用FPCQ A A（true）（false）我们从竞技场开始一（true）一（false）（一）定 义4.1 （ i ） 设R 是 一个 集 合 ，它 具 有 一个 关 系式 λ （{λ}+moveset ）×movesett。 R的根是rt R={r|当s ∈ S的子环{ r}rt R∈R时，|sr}。我们认为，当所有这些子集都不相交时，R是一个前，并且对于每个r∈R，存在一个（必然唯一的）有限序列∗►r0► ··· ►rn=r(ii) 竞技场是一片可数的森林。(We在此阶段，不要求R元素上的Q/A标签，因为我们没有强加括号条件。）(iii) 我们把R和S的不交并写成RS。(iv) 如果r∈R，我们将严格从R.(v) 从arena R到arena S的标记重命名是一个函数RfS，使得如果b ∈ rtR，则fb ∈ rt S，并且f限制于一个arena同构RTb=STfb。 我们为arenas和to ken的类别编写T o k R e n重命名它有由不交并给出的有限余积（实际上也有可数余积，尽管我们不使用它们）。给定一个竞技场R，R上的指针博弈非正式地描述如下。• 游戏在玩家和对手之间交替进行，玩家首先移动。• 在每一步中，R的一个元素被播放。484P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467• 参与者移动的方式是声明根r∈rtR，或者指向前一个对手移动m并声明m中参与元素的子元素。• 对手通过指向前一个Player-movem并声明在m中播放的元素的子元素来移动。例如，竞技场上的指针游戏的一种可能的玩法Q A A（true）（false）一（true）一（false）是PQ OA（真实）PQ（2）第二章：一夜情事实上，这出戏将区分条款P和PJ节。一点二在PJ的情况下，表示法包括（2）作为发散，而在P的情况下，它不包括。这些指针游戏可能看起来很神秘。高阶程序在什么意义在[11]中给出了一个具体的解释，使用了一种语言和一种操作语义风格，它们对程序各部分之间的交互更加明确（参见[3]）。由于这一切都是正交的非决定论，这是本文的主题，我们省略它。I/O签名Z决定了这个游戏的变化• 每当轮到他的时候，玩家可以选择陈述一些o∈O而不是一个R元素• 然后对手必须使用一些i∈Io。我们称之为RwrtZ上的指针博弈。我们的第一步是正式制定这个游戏，包括移动之间的所有指针定义4.2设R是一个arena，Z是一个I/O签名。(i) RwrtZ中的一个正则序列s是从初始6段开始的函数movesetN（其元素称为moves），Σ（{x}+moveset）×R+O+o∈OIo使得对于每个移动M，• m∈Ioi <$m>0且sm−1=o∈O[6]推广这一点通常是方便的，因此moveset可以是N的任何子集。当然，它将唯一地与N的初始段序同构，通过应用这种序同构，我们恢复了一个“ 正 确 的 ” 正 义 序列 。P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467485op• 如果sm=（m，r），则r是R• 如果sm=（n，r），其中n∈moveset，则n m和sn=（k，RJ）且r是RJ子。根据sm是（k，r）或o或i∈Io，将移动描述为竞技场移动、o-输出移动或o-输入移动.如果sm是（k，r），我们说(ii) 一局棋是一个正义的序列s，对于每一步棋m，• 如果m是偶数（例如0），那么它是输出移动或指向奇数或奇数的竞技场移动的竞技场移动• 如果m是奇数，则它是输入移动或竞技场移动指向到一个公平的竞技场移动。然后我们说竞技场移动m是玩家移动或对手移动如果m是偶数（例如，0）或奇数。(iii) 一个有限的游戏等待O-输入，如果它以O-移动结束。否则，它等待玩家或等待对手根据其长度是偶数或奇数。(iv) 竞技场R的非确定性无限迹（NIT）策略σ包括• 一个等待对手和等待输入的游戏集合A（有限轨迹）• 一组分歧（分歧）• 一个无限游戏（无限轨迹）的集合C。这样，如果s在A、B或C中，则每个等待对手的前缀都在A、B或C中，A.(v) 我们定义了决定论，而无死锁则是一个集合U，用于像Def中那样的策略。2.4.(vi) 我们定义i∈Iσi输入O{σi}i∈Io 就像Def. 两千五(vii) 我们把R上的策略集写为stratUZR，无死锁的wrtU。这在R∈TokRen中显然是函子的。4.2分类结构修复I/O签名Z和一组全方位错误U本节的目的是定义• a类GUZ，有限产品• 左GUZ-模，即函子NUZ：GUZ→Set(We通常省略G和N上的下标UZ和strat）。由此，再加上一些额外的结构，我们得到了按推值调用的模型。见[12]为这一建筑的分类帐户486P.B. Levy/Electronic Notes in Theoretical Computer Science 155（2006）467UZ UZG的对象是arena，NR是stratR. 我们应该写Rσσ∈stratR。G的homsets由下式给出：G（R，S）=strat（RSTb）b∈rt S事实上，Gi（具有确定性和括号约束，并且没有I/O）在[ 1 ]中被称为为了定义R上的恒等态射，我们定义idR，b为RRTb上的决定性策略，没有分歧，其有限/无限迹都是玩家最初在b中玩的策略，并且响应于0 Winlb withn Winrb n+1 Winlb withn Winrb n +1Winrb withn Winlb则定义idR∈ G（R，R）为b∈rtR到idR，b的映射。为了完成上述范畴结构，我们需要两种组合：RfSgT和RF SG这两个都可以定义，一旦我们有了，对于竞技场R，S，T，一个地图G（R，S）×strat（ST）最大大鼠（RT）我们现在要定义它。直觉上，策略στ应该跟随τ，直到它在S的一个根b上移动，然后继续在σb上移动，直到它在S上移动另一步，然后再次跟随τ，依此类推。但是S中的移动是隐藏的-定义4.3设R、S、T为竞技场。(i) 设s是RST上的一个正则序列。 这样的s的内部线程名是innerss ={left am|a ∈ rt S，m是s中的一步棋，博弈是<$W a}<${right}s的线程名是innerss {outer}。对于每个线程名p，我们将p的竞技场定义为• RT，如果p=外部• STifp =right• RSTaifp =leftam.除外部线程之外的所有线程名称都是内部线程。(ii) s的线程指针集合将R中的每个rootmove与S中的早期rootmove关联，并将每个输出move与内部线程名称关联。