232理论计算机科学电子笔记45（2001）网址：http://www.elsevier.nl/locate/entcs/volume45.html26页理想CSPJ. 莱尔德COGS，University ofSussex Brighton BN19QH，UK电子邮件地址：jiml@cogs.susx.ac.uk摘要一个游戏的语义描述了一个类型化的功能语言，其中包括原语的并行组合和私人渠道上的同步通信。 语义是基于一个类别，通过扩展“Hyland-Ong游戏”与表示的多线程的控制使用“并发指针”，表示一种新的因果关系之间的动作。 语义被证明是完全抽象的“通道自由”类型相对于一个可能和必须等价的有限片段，并相对于可能等价的整个语言，使用因式分解结果，以减少可定义性的顺序情况。1介绍博弈语义已被成功地应用于各种顺序程序设计语言的建模，其显著特点是许多基本概念是内涵的，结合了并发理论和传统域理论的思想。基于PCF [12]的Hyland-Ong（HO）模型，出现了一个完全抽象模型的层次结构，扩展了非功能性（但仍然是顺序的）特性，如可变状态和存储[1，4]和控制[13，1,4]，现在有一个彻底的分析顺序功能计算，在很大程度上基于并发。因此，扩展现有的游戏模型来解释并发特征是一种自然的发展，尽管它需要在视角上进行实质性的改变，因为现有的模型是基于将交互表示为令牌（移动）的交替序列其中一种结构-并发博弈[3]-已经被Abram-sky和Mellies用来建模乘加线性逻辑（其中并发是隐式的而不是其他）。并发游戏是基于一个“真正的本文描述了并发行为的一种不同表示--2000年1月，出版社dbyElsevierScienceB。 V. 在CC BY-NC-ND许可下开放访问。拉尔德233它保留了基于令牌的交互概念，但增加了多线程控制的表示，允许利用侧事件的HO游戏模型的丰富结构来建模显式并发特征，例如私有信道上的通信。多线程游戏用于给出具有算术的类型化按名称调用λ-演算的语义加上并行组合运算符和沿着具有本地声明名称的通道传递的（基础类型）消息。这种语言的语法本质上与Brookes的理想化CSP相同[7]，因此我们保留了这个名称，尽管在操作语义上有几个不同;消息传递是同步的（与[7]中的同步相反），并且在并行组合操作符的解释上有一个关键的区别;这可以概括为，它在这里被解释为进程的并行组合，而在[7]中被解释为命令的并行组合。尽管如此，游戏模型提供的语义分析可以被视为对[7]中描述的函子-范畴语义的补充。它的显着特点是，它是完全抽象的，相对于可能测试（对于完整的语言），以及相对于可能和必须测试（对于无递归片段）。完整的抽象结果仅限于Hyland-Ong博弈的基本框架给了我们一个λ-演算的算术解释。对模型并发性的扩展有两个关键特性：多线程和同步消息传递。对多线程控制的解释需要对游戏语义学中以前的工作进行最激进的扩展，这些工作（除了[3]）通过将策略的交互表示为移动序列来构建序列语言模型。 我们在这些序列中添加了一组新的“并发指针”，这样它们就可以被看作是将两个策略的交互表示为一个移动树。然而，保持移动的顺序，允许我们在树的不同分支中捕获移动之间的同步通过向后跟踪控制指针，我们可以为每次移动提取一个“控制线程”（树的一个分支）。这些是来自相关HO博弈的普通序列，允许定义与原始HO博弈和策略同构的“序列策略”子类基于控制线程的交错，在多线程设置中存在策略的并行组合的自然操作。此外，我们表明（通过因子分解），所有分支的控制线程在有限的策略可以从这样的并行组合。消息在私有通道上的传递是以“面向对象”的风格来解释的事实上，拉尔德234|||⇒⇒chan类型作为其“方法”send和recv的产物，与理想化Algol [1]的博弈模型中var类型及其方法（赋值和反引用）的解释完全相同。 因此，这两个特性的语义之间的唯一区别在于对新变量和新通道声明的解释。 两者都是在一个战略，违反了一些约束的组成部分，遵守相应的纯功能性条款，并捕捉因果关系写与读或发送与接收之间的关系。“新通道”策略的关键属性论文的其余部分基本上分为两部分;第2 - 4节定义了ICSP的合理游戏模型，第5节将其细化为完全抽象的语义。因此，第一部分完成了解释游戏中的线程和通信所需的新功能，而第二部分包含更多与原始HO模型相关的技术材料。该组织的详细情况如下：— 在第2节中，定义了ICSP的语法、操作语义和上下文— 第3节描述了“多线程游戏”的类别— 第四节给出了ICSP在这一范畴中的指称语义，并表明它在操作语义方面是合理和充分的— 第5节对语义进行了细化，并推导出了完整的抽象结果。首先，使用一个新的条件--然后，定义了顺序策略的一个子类别;也满足可见性，无辜性和良好包围约束（的多线程版本）的顺序策略被证明形成了一个与[12]中用于建模PCF最后，我们给出了两个因子分解结果，以表明模型中的每一个有限策略都可以定义为ICSP的一个项，由此可以进行完全抽象。2理想化CSP理想化CSP [7]，或ICSP，是基于按名称调用的λ演算，其类型是从基础类型（命令），nat（自然数）和chan（发送和接收自然数的通道）生成的(We我有时会用B来表示原子或基本类型nat和nat，并说一个类型是无通道的，如果它是从基本类型构建的， .）T：：=chanTT T术语根据以下语法构成：M：：= x |skip |0 |succ M |Pred M |IF0 M |λx.M |MM |YM无|M; M| MM|新陈M|发送MM|接收M拉尔德235⇒该语言将λ演算与并发原语（基于CSP [10]）结合在一起，就像理想化的Algol [19]与命令式功能（在其名称中承认的智能债务）一样;声明一个新的通道名称并在其上发送和接收类似于声明，分配和处理定位变量。并发特性的类型判断如下：ΓM：BΓN：BΓMN：BΓnil：BΓ►M:comm Γ►N:BrM;N：B中文（简体）M：BΓM：chan ΓN：nat联系人：陈先生Γ►M:chanrecvM：nat给定M：nat，N：B，我们也将（（IF 0M）N）N写成M;N。操作语义是根据ICSP配置的“小步”缩减关系给出的 配置C = N1，...， Nk是一组并行线程-相同（基本）类型的ICSP程序-包含空闲通道名称Ch（C）。（同样，可以使用结构一致性和范围挤压来减少单个程序减持规则使用求值上下文的概念为每个线程挑选一个唯一的下一个redex，它不是一个值。定义2.1求值上下文由以下语法给出：E [·]：：=[·] |E [·] M|predE [·] |succE [·] |IF0E [·]|E[·];M|发送M E[·]|发送E[·]n|小步长归约规则如下：E[λx.M N]，C−→E[M[N/x]]，C E[YM]，C−→E[MYM]，CE[pred（succM）]，C−→E[M]，CE[IF0 0]，C−→E[λxy.x]，CE[IF0（succ n）]，C−→E[λxy.y]，CE[skip;M]，C−→E[M]，CE[M<$N]，C−→E[M]，E[N]，CE[newchanM]，C−→E[M c]，C：c/∈Ch（E[newchanM]，C）E[sendan]，EJ[recva]，C−→E[skip]，E[n]，C.操作newchan允许声明本地或私有通道-newchanM提供一个新的通道名作为M：chan B的参数，并将其添加到环境中。send的求值是通过将其第二个参数减少为一个值（数字），然后将其第一个参数减少为一个通道名称，recv将其参数计算为一个通道名称，并分别并行发送一个n和recv一个reduce以跳过和n。与[7]相反，消息传递是拉尔德236ǁǁ不同步的进程nil：B可以看作是两个死锁进程newchan λc的简写。sendc 0：new或newchan λc。接收c：nat. 请注意，评估并行组合会重复评估上下文。这似乎令人惊讶，但如果我们回想起求值上下文实际上是当前延续的表示，则更有意义因此，（地面类型）进程并行组合每一个线程因此，两个值（比如skip和skip）的并行组合简化为由两个线程组成的配置，其中包含无法进一步计算的这些这与[7]中对M N的解释不同，可以称之为“命令的并行组合”; M和N同时计算，如果至少有一个计算结果为跳过，则返回单个值跳过。因此，例如，命令skip和skip的并行组合等效于skip。 使用具有同步通信的进程的并行组合，我们可以将命令M、N的并行组合表示为：纽坎λc. （（M; send c 0）（N; send c 0）（recv c; nil））.各种其他编程结构，如Algol风格的存储和非确定性选择，可以在ICSP中表达一个有用的例子;对于任何n>0，定义程序oraclen，它不规则地产生一个小于n的数。oraclen= newchan λc. （（send c 0 sendc 1. （pred n）;（nilominal recvc）对于涉及并发性的更微妙的编程问题的解决方案的例子[7]的文件。2.1收敛性测试和操作等价性观察等价是相对于一个简单的测试定义的-至少有一个收敛线程。这相当于测试恰好一个收敛线程，或者对于任何有限个n >0，至少/恰好n由于（正如人们所期望的那样）nilM在外延上等于M，我们无法观察到死锁线程的存在，因此无法测试所有线程是否收敛。定义2.2定义谓词在类型A的配置上的可收敛性（may convergence）如下：C，跳过梅CJ.C→CjC.马伊项M、N：T是可能等价的（如果对于所有程序上下文，则M可以是NC[·]：n，C [M] n可以当且仅当C [N] n可以。拉尔德237⇓不联系我们May-equivalence是使用博弈语义的模型的自然等价-正如我们将看到的，它对应于策略的迹等价然而，对于一个固有的非确定性语言，如ICSP，它是相当弱的-它导致无法区分总是收敛的程序与那些可能收敛或发散的程序[9，8]。一个更强有力的等价概念可以从可能和必须测试中推导出来。定义2.3定义配置上的谓词必须（必须收敛）C、跳过必须J.J.（C→CJ）=<$CJ<$必须Cmust项M，N：T必须等价，如果对于所有封闭上下文C[·]：N，C[M]必须当且仅当C[N]必须。我们应该写MM&MN，如果M和N是may-equivalent和must-equivalent。像序列语言的博弈（和其他）模型一样，我们的语义将β相等视为指称等价-例如。 我们有[λx.x skip]]=[[skip]。不幸的是，在无限约简序列的存在下（没有评价的公平性），β-平等对于可能和必须测试来说是不合理的。例如，λx.xskipMMskip，因为Yλy.y λx.xskip必须。这表明，要给出ICSP的指称语义，对于可以和必须测试（或互模拟等价）来说是足够的将有必要将术语的归约行为并入语义中。在这里，我们将只给出ICSP的“finitary”片段的可能和必须结果，对于该片段，求值总是终止;我们将调用没有Y -组合子命题2.4有限ICSP的构形不存在无穷级数C1，C2，. Cn，. 使得C1−→ C2−→... − → C n−→.. ......你好。证据 是由一个标准的基于“可计算性谓词”的参数。✷3多线程游戏将用于模拟ICSP的博弈结构基于Hyland和Ong [12]和Nickau [16]给出的博弈结构（并在[15，1，4，11]中开发），其中博弈状态-系统与环境之间的相互作用-表示为合理的移动序列。然而，为了对并发进行建模，我们将在移动之间增加一个因果关系，用“并发指针”来表示。这允许将多个交错的“控制线程”的树表示为单个序列。然而，这样的“多线程序列”携带关于树的不同分支中的事件的时间排序的附加信息，并且该附加信息在建模同步时将是重要的。一个游戏的结构（动作、它们的标签、它们之间的关系）是由它的竞技场所规定的。这基本上是在[12]中定义的;不需要新的结构来支持多线程。竞技场A是一个三重的A，拉尔德238∗ ►► ⊆×联系我们QAi=1±（MA）λ×MA，λA：MA→ {Q，A} λ，其中：— MA是一组称为移动的令牌，—A（MA）→MA是一个叫做使能的关系，— λA：MA Q，A是将移动标记为答案（A）的函数，或者问题（Q），这样每个答案都有一个独特的使能动作，这是一个问题。我们规定，MA中所有移动的唯一极性可以使用以下规则从使能关系推断：如果m是初始的，则m是Om），或由P-move启用，如果m由O-move启用，则它是P最简单的竞技场是空的竞技场1，没有移动，以及具有单个初始对手问题q的平坦竞技场，该初始对手问题q允许用于解释基本类型的一组玩家答案（在这里，如[12]等）;对NAT的解释是具有单个答案（“命令的执行已成功终止”）的NNAT范围[12]中的乘积和函数空间构造器也适用于多线程设置。Product对于任何集合索引的竞技场族{A i|i∈I}，形成乘积A=i∈IAias如下：• Mi∈IAi=i∈IMAi，• m，i•λi∈IAi（m，i）=λAi（m）.我们将Ak写成Ak。函数空间对于竞技场A1，A2，形成A1<$A2如下：• MA1A2=MA1+MA2，• 如果i=j且m<$n，或m∈MA2，n∈MA1 和A2 m和λ1 n，<$Q<$A<$m，i<$ifm∈MA2且d<$A2m，• λA1<$A2（m，i<$）=λAi（m）。一般来说，l，m，n... 将用于表示竞技场的移动，而a，b，c，. 以表示这些移动在序列r、s、t中的出现。 空序列记为ε，对于任意序列s，t，st表示s是t '的前缀，sa表示由移动a扩展的序列s，st表示由序列t扩展的序列s。在一个移动序列sa中，s的一个调整指针是从a到s中某个移动的指针，该移动使a成为可能。在竞技场A上的一个调整序列是MA的一个元素序列，其中每个非初始移动a都有一个调整指针。一个交替的公正序列t是这样一个序列，在这个序列中，对手的移动总是跟随着玩家的移动，反之亦然。我们把A上的交错正则序列的集合记为JA。拉尔德239n1 、、3.1多线程序列我们现在将定义我们的模型所基于的多线程序列它们是通过将“并发指针”添加到公正序列中形成的定义3.1设sa是一个移动序列。a的并发指针是从a到s中某个单一移动（a的出现）的指针，它与它的对齐指针（如果有的话）不同。 如果移动没有并发指针，则它是线程初始的。设MTA是在竞技场A上的多线程序列（具有并发指针的对齐序列）的集合没有并发指针的对齐序列（即[12]中使用的对齐序列的标准概念）被称为“单线程”。通过回溯并发指针，我们可以从每个多线程序列中提取一系列单线程并发，或定义3.2序列s中最后一步的控制线程CT（a）=a，如果a是线程初始的，CT（satb）= CT（sa）b，如果b有指向a的并发指针。多线程合法序列是具有并发和公正指针的有限序列，使得每个线程都是交替的公正序列：• 每个非线程初始化的O-move都有一个指向移动，反之亦然，• 每个非初始移动都有一个指向其控制线程中的移动的调整指针。定义3.3对于竞技场A，定义多线程合法序列的集合如下：LM A={s∈MT A|是的。CT（t）∈JA}。定义3.4一个合法的序列（多线程或单线程）是良好开放的，如果它包含最多一个初始对手移动。 假设WM A是A上的良好打开（多线程）合法序列的集合：WM A={s∈LM A|ta±sa=t = ε}例如，在Arena[nat]上的单线程序列最多只有三步，并且对于某些i∈ω，其形式为ε，q或qai。相比之下，对于任何自然数n 1 n 2的有限序列... n k有一个独特序列--o_o，，q，a，s、、、an2...安基每一个人，都有一个属于自己的归宿，一个属于自己的归宿。此序列是控制线程树的表示：，，、、、an1ıan2......安基— 我们应该看到，这是一个跟踪战略[n1n 2 n]。 . nk]]。拉尔德240ǁ ǁǁ3.2表示并发交互树作为带有指针的序列的表示可以很容易地看出是非唯一的;在上面的例子中，答案的任何排列a n1，...，a nnwillgiveveatracein[n1n2. . . nk]。 我们可以通过认为控制线程的所有这种交织是等效的来获得唯一性，但人们可能会问：首先，以顺序形式表示多个控制线程的意义是什么？答案是，为了在不同的线程之间同步事件，需要移动的顺序然而，由于理想化CSP本身只包含有限的设施，这样的同步，多线程序列仍然不给相应的策略之间的相互作用的唯一表示。因此，玩家策略将只有有限的权力来观察和控制移动的实际顺序在不同的线程。玩家可以等到一个给定的O-move发生后才给出响应（在ICSP中，可以暂停一个线程的评估，直到另一个线程中发生事件）。但是，玩家不能：• 迫使一个P-移动发生在另一个（玩家或对手）移动之前，或• 观察两个连续的O型移动发生的顺序。为了反映这些约束，我们定义了一个前序4，使得s4t，如果s可以通过向前迁移P，向后迁移O-从t获得。我们将要求策略在4下是封闭的-换句话说，如果t是策略的迹，并且s4t，则s也必须是策略的迹。定义3.5设4是多线程合法序列上的最小前序，使得对于所有sab·t，sba·t ∈ LMA，使得λ OP（a）= O或λ OP（b）= P，sab·t 4 sba·t。顺序的、确定性的玩家策略的原始表示[12]是偶数长度序列的集合，其中最后一步代表玩家对前一个序列的反应。正如在[8]中所观察到的，这种形式的表示不足以对一个简单的非确定性函数语言进行建模，直到可能和必须等价;例如，它识别出一个总是收敛于一个可能收敛或发散的策略在多线程设置中，缺少交替条件使问题进一步复杂化;不再是这样的情况，即位置空间在轮到对手移动的位置所以玩家可以不等待对手的反应而走一系列的步，或者可能需要几个竞技场A上的多线程策略σ将被表示为它（可能）停止的迹的集合，要么等待永远，要么等待一些更多的O-移动。定义3.6给定一个集合σ ∈ LM A，令T σ={s ∈ LM A|t∈ σ.s ± t}。当σ是一个策略时，Tσ表示σ的可达迹集。定义3.7A（多线程）策略σ：A是LMA主题的子集拉尔德241⇒∈/∈∈⇒±达到以下条件：• ε∈σ，• σ关于4-s4t是闭的并且t∈σ蕴涵s ∈σ，• 具有O-移动的可达位置的延伸是可达的-如果s∈Tσ且a是O-移动使得sa ∈LMA则sa ∈Tσ，• 在任何可达位置，σ必须要么走P步，要么等待另一个O步--如果s ∈ T σ，则要么s ∈ σ，要么存在某个P步a，使得sa ∈ T σ。A上的单线程策略是满足这些条件的LA的子集（4下的闭包显然是平凡的）。为了给一个完全抽象的语义，可以测试的完整的语言，我们将考虑的战略，只有等价的可达的痕迹。定义3.8如果T σ = T τ，则σ：A与τ：A（σ<$Aτ）迹等价。我们现在将定义一个领域和战略的类别。首先，将限制的概念扩展到多线程序列，以便它定义3.9给定s∈L（A1<$A2）<$A3，sT（Ai，Aj）（i j）是Ai Aj上的多线程序列，定义如下：εT（Ai，Aj）=εsaT（A i，A j）= sT（A i，A j）if aM Ai，MAjsaT（A i，A j）=（sT（A i，A j））aif aM Ai，M Aj.a在saT（Ai，Aj）中的表示符是从Ai或一个J，它在遗传上是正义的。（如果没有这样的移动，那么a是初始的。来自a的并发指针指向CT（sa）中来自A i或A j的最近玩过的移动（如果有的话）。引理3.10如果s∈LM（A1<$A2）<$A3，则CT（sT（A i，A j））= CT（s）T（Ai，A j）。与其他模型一样，规范态射是模仿策略，简单地复制对手在游戏不同部分之间的移动。（然而，并发指针和公正指针的处理之间存在差异;O-movea的副本具有指向自身的并发指针，以及公正指针。（注：指的是一个复制品的移动。身份战略就是最好的例子。定 义 3.11 说 s LM AA 是 一 个 copycat 序 列 ， 如 果 对 于 所 有 的 t偶 数 s ，tTA−=tTA+，并且在s中的任何时候P-移动都与前面的O-移动同时发生。 则idA={s ∈ LM A<$A|这是一个模仿者。策略的定义3.12给定σ：A1→A2和τ：A2→A3，令σ;τ={t∈LM A1和LMA3|<$s ∈LM（A1<$A2）<$A3.t =（sTA1，A3）<$（sTA1，A2）∈σ<$（sTA2，A3）∈τ}拉尔德242⇒⇒∈⇒⇒∈⇒⇒∈⇒ ⇒∈⇒⇒ ⇒⇒引理3.13若σ：A<$B且τ：B<$C，则σ; τ：A<$C。证据关键是如果sLM（A1A2）A3，则sTAi，Aj是a合法序列和4下的闭包。前一种情况是从单线程情况[12]出发的，使用引理3.10. 后者的证明是：给定s LM（A1A2）一个3 和tLM A1A3，使得sTA1，A34t，我们可以找到rLM（A1A2）A3，使得rTA1，A3= t，sTA1，A24rTA1，A2和sTA2，A34 rTA2，A3。 我们从s中推导出r，通过向前迁移A3中的P -移动，向后迁移A1中的O-移动，并交换连续的O-移动和连续的P-移动。复合是结合的证明遵循[12]中的标准论点，这几乎没有因为并发指针的存在和交替条件的缺失而改变。命题3.14对于所有σ：AB，τ：BC，ρ：CD σ;（τ; ρ）=（σ;τ）; ρ.定义3.15然而，为了构造一个carbohydrate闭范畴，我们需要良开策略的概念。一个良好开放的策略σ：A是WM A（定义3.4）的一个子集，满足定义3.7中关于良好开放序列而不是合法序列的条件。良好开放策略σ：A B与τ：B C的合成是通过定义3.16对于包含初始移动a的（多线程合法）序列sTa定义为s的（多线程合法）子序列通过a进行顺序调整：saTa=a，sbTa=（sTa）b，如果a平行于sb（b具有通过可见性在sTsbTa = sTa否则。对于良好开放的σ：A，定义σ†：A如下：s∈ σ<$当且仅当对于s中的所有初始移动a，sTa ∈ σ。我们现在可以定义类别GS和GM，其中arena作为对象，A和B上的多线程和单线程策略分别作为从A到B的态射组成定义为σ·τ=σ†;τ。（关于A的完全开放的同一性策略IdA是将idA限制为完全开放的序列。命题3.17 GM†是一个范畴。是的。 我们使用以下事实：对于任何一个A，IdA=IdA，对于任何一个开的σ，σt;IdB= σ。对于完全开放的策略σ：A<$B，τ：B<$C，σ<$;τ<$=（σ<$;τ）<$。此外，单线程游戏[15，4]上的CCC结构可以平滑地转移到GM;操作×是具有模仿策略πi的carnival乘积：拉尔德243⇒GM⟨► ►⟩×→►GS GMA1×A2 ×Ai我我A1×A2→Ai，其中i= 1，2：πi={s∈W−−+的|我不知道。tTA−=tTA+}。定义3.18对于完全开放的策略σ：A→B，τ：A→C，定义：τσ，τ：A → B × C ={s ∈ LM A<$B×C|（sTA，B ∈ σ <$sTC = ε）<$（sTA，C ∈τsTB = ε）}。指数是函数空间的舞台-有明显的模仿策略：应用程序：A×（A<$B）→B和Λ：（A×B）<$C→A<$（B<$C）。命题3.19 GM，1，×，是一个Carnival闭范畴。为了对递归建模，我们通过迹等价（trace-equivalence）进行商数（这必须通过复合来保持，因为每个等价类都包含在该类中的所有迹上停止的策略结果是一个cpo丰富的类别，这是ICSP的五月测试模型的基础命题3.20设GM/GM是范畴，其中态射是来自GM的策略的n-等价类（具有组合的明显定义：[σ]·[τ]=[σ·τ]）。 则GM/GM是一个cpo-富序的闭范畴，若T σ<$T τ.4ICSP的语义如[1]中所述，顺序复合的解释是通过定义[[ΓM;N]]=[[ΓM]]， ΓN]];seq，其中seq：顺序复合是一种策略，在做出响应之前依次询问它的每个参数一次因此，seq中播放的典型控制线程如下所示[[]]×[[]][[]]QaQ一一然而，在多线程设置中，我们需要能够将seq定义为在每个控制线程中以相同方式行为的策略。更一般地说，我们希望在单线程策略的范畴内将PCF的原始模型嵌入GM。定义4.1给定单线程σ：A，定义多线程策略multithread（σ）：A={s∈LM A|你好。CT（r）∈T σt。（（t4s<$s4t）=<$CT（t）∈σ）}。引理4.2操作multithread是一个函子，从到它保持了carnival封闭结构。Q拉尔德244|{1}||{\fn黑体、×C×→、证据多线程（σ）;多线程（τ）=多线程（σ; τ）的证明基于引理3.10。 ✷因此，我们可以将顺序构图的解释和连接定义为多线程下的图像与单线程下的图像。策略的并行组合是通过交错它们对初始移动的响应（保留并发指针）。如果说竞技场-如果它有一个独特的初始移动打开。定义4.3设s = ab1. b m和t = ac1. c n是LM A中的序列，其中A是完全开放的区域。s和t的尾部交织是序列ar∈LMA，其中t是f1的交织。 . bmwithc1. . . c其中，该服务器用于证明和并发内部问题-例如， 如果bj点指向s中的a，则bj点指向r中的a，或者如果bj点指向s中的b i，则nbj点指向r中的bi。 我们要写|t表示s和t的尾交织的集合。命题4.4对于任何良好开放的竞技场A和（盲指针）策略σ，τ：A σ与τ-σ τ=s t s σ t τ的- 是一个定义明确的（指针盲）策略。因此，例如，对于具有唯一初始移动的竞技场，我们有一个一般的平行合成态射，对A：A×A→A = π l|π河一个典型的游戏（与 A A[2019 - 04 - 16][2019 - 04 - 16][2019 - 04][2019 - 04 - 16][2019 - 04][2019 - 04 -04][2019 - 04][2019 - 04 -04][2019 - 04][2019 - 04 - 05][2019 - 04][2019 - 04]][2019 - 04 - 05][2019 -04][2019 - 04][2019]][2[[]]×[[]][[]]、、_、、Q、，，zq. ı、一个，_q一个，、、、，，a，_， ， a我们定义[Γ <$M <$N：B]]=[[Γ <$M]]|[[Γ N]. 我们有这样一种特性，（σ|τ）× ρ; seq =（σ × ρ; seq）|（τ × ρ; seq）-换句话说，对于所有M，N：，[[（M <$N）; L]]=[[（M; L）<$（N; L）]]。因此，仍然需要给出局部绑定通道的语义这是基于将chan类型的元素视为这是Reynolds [18]提出的对引用类型的解释，并被Brookes [7]用于给出理想化 CSP这里描述的解释特别接近于理想化Algol [1]中store的游戏语义• 我们定义[chan]]=[[]]ω[[nat]（这与[1]中给出的var类型的解释相同• 对于发送消息，有一个顺序和无辜的策略写：[[nat]] [[]]ω[[]在[1]中描述，通过询问[nat]中的问题来响应初始移动，给定答案n，它在乘积[]]ω的第n部分询问初始问题。当这个问题被回答时，它回答了最初的问题。拉尔德245c、►►×►⟨► ►⟩⊆∈····∈我们定义[ΓsendM N]] = [[ΓM]];πl，[[ΓN]] ;write，这与[1]中对赋值的解释完全相同。• 我们定义[ΓrecvM]] = [[ΓM]];πr（[1]中解分配因此，通道的语义中唯一非功能性的部分--而且也是唯一与理想化Algol中商店的游戏语义不同的部分--是对新通道生成的解释这是由一个（指针盲）策略ccell：[[nat]][[ nat]]ω的的，它类似于用于解释理想模型中的new的单元格策略Algol [1]的两个读/写或发送/接收组件之间的交互，但重要的区别是发送和接收之间的通信是并发和同步的，而不是顺序的。下面给出了一个典型的ccell（带有并发指针）（第i个“发送组件”[nat]] ω中的问题[[]]ω×[[nat]]send（i）S发送（j）.你好，， 发送、、发送recv，，.rec（j）recv，，.（i）非正式地，ccell的行为可以用以下术语描述它必须对任何既有未回答的send（i）问题又有未回答的recv问题的游戏做出响应，通过给出recv问题的答案random（i）和send（i）的答案来匹配这些问题对因为答案可以在任意一对开放的发送和接收移动之间交换，所以ccell是隐式不确定的。为了满足交替条件，发送和接收移动必须总是在不同的线程中-正如人们所期望的那样，因为同步消息传递要求发送者和接收者在不同的线程中。形式上，ccell可以定义如下。• 设ccell的平衡序列Bccellccell是LMchan]]中包含ε且闭于4的序列的最小集合，并且满足以下规则：如果s Bccell，则ssend（i）recv sent rccell（i）Bccell（其中send具有concurrency和justification指针发送（i），和rename（i）recv）。• 令ccell的Bccell使得如果s∈Sccell，则s·send（i）∈Sccell。• 令“等待接收”序列的集合Bccell使得如果s∈Rccell，则s·recv ∈Rccell。拉尔德246↓ ↓/↓/↓JJJKK我 J我 K现在让ccell ={s∈LM[[chan]]|s4t<$（t∈Sccell<$t∈Rccell）}并定义：[[Γ newchanM：B]]=（[[Γ M：chan B]] × ccell）; App.4.1语义的合理性我们可以说，如果一个策略至少能回答一次初始问题，那么它可能是收敛的;如果它总是对对手的初始行动做出某种反应（即不等待），那么它一定是收敛的定义4.5对于策略σ：[[]]，定义σ↓may，如果qa∈Tσ且σ↓必须如果q/∈ σ.解释的合理性-即在操作语义学和指称语义学中，may和must概念之间的对应关系现在可以建立。首先，并行组合的可交换性和结合性，以及新通道声明的可交换性意味着配置的表示可以没有歧义地定义。定义4.6对于构型C= M1：n，.，M n：这样，Ch（C）= c1，.，c k，定义[[C]] = [[newchanλc1.... newchanλc k.M1. [2014 - 04 - 24].假设一个配置是收敛的，如果它具有形式C，跳过，如果它不收敛，不能进一步减少，则死锁。如果C是收敛的，那么[[C]]可能和[C]]必须;如果C是死锁的，那么[C]]可能和[C]]必须。因此，关于may测试的语义的合理性归结为以下事实。命题4.7如果C−→CJ，则T[[CJ]]<$T[[C]]。证据 证明是基于一个cpo-丰富的cartesian闭范畴的标准性质以及下面的引理。引理4.8[[E[M<$N]=[[E[M]<$E[N][[（newchanλc. M）<$N]]=[[newchanλc. （M<$N）]]（c∈/FV（N）[[（newchanλc. M）;N]]=[[newchanλc. （M;N）]]，（c∈/F V（N））[[newchanλc.E [sendc v]<$EJ [recvc]<$M]]<$[[newchanλc.E [skip]<$EJ[v]<$M]]。关于必须检验的有限片断的可靠性由以下命题表示。命题4.9对于任何非收敛和非死锁配置C对于无穷个ICSP，[[C]] ↓必有，如果[[CJ]] ↓必有，对于所有CJ，使得C −→ CJ。证明是基于引理4.8中给出的等式/包含以及以下引理（通过分析策略ccell建立）。引理4.10对于M1，M2，. M n，定义Mi≤nM i=M1<$M2<$. ，假设我们有项Mi=Ei[sendai vi]：j≤mi且Ni=Di[recvai]：k≤ l i，对于i ≤ n，其中每个E i [·]和D i[·]是评估上下文。然后JKi≤n（（拉尔德247KK↓−→⇓⇓⇓−→↓⇓I≤n，J ≤mI，K ≤lJ⇓ ↓ ⇓↓我J我Ki≤n（（其中M（I，J）i=Ei[skip]，如果i=I且j=JJ JM（I，J）i=Mi否则，J J且如果i=I且k=K，则N（I，J，K）i=Ei[vI]k k JN（I，J，K）i= N i，否则。我们现在可以通过归纳法证明命题4.9的约化序列长度。给定C使得如果C CJ则[C]]必须，假设有某个约简C CJ不是通信规则的实例。[48][ 49][49]][49][49]另一方面，如果不存在不是交流的instance的reduction，那么所有线程具有E[sendc n]或E[sendc n]的形式，因此根据引理4.10，q/∈[[C]]=CJ：C−→CJ[[CJ]，如所需。命题4.11如果M：M是ICSP的一个程序，那么M可以当且仅当[[M]] ↓可以，并且如果M是有限ICSP的一个程序，那么M必须当且仅当[[M]] ↓必须。证据通过归约的归纳，Mmay蕴涵[M]]may和Mmust蕴涵[M]]must对于无限次ICSP而言，相反的结论来自于评价总是终止的事实（命题2.4）。为了证明[M]]可以，那么对于包含Y组合子的项，M可以，我们使用[[C[YM]]可以当且仅当存在某个有限k使得[C[Mk]]可以归约为无穷ICSP的结果。（其中Mk是YM的第k次逼近，即M0=λ，Mk+1=M（Mk.）✷5可定义性和完全抽象我们的ICSP模型不是完全抽象的可能或必须等价。这是因为控制指针的存在允许在与语言中的区别不对应的策略在本节中，我们将展示如何通过消除这些区别来削减模型，从而通过证明每个紧凑策略都是可定义的来实现完全抽象的结果。我们需要的约束是Player不能（直接）观察O-移动的并发指针。这对应于在ICSP中不能直接观察到计算发生在哪个位置（即哪个线程）的事实。例如，λx.x：natnat在观测上等价于newchan λc.λx。（（sendc x;nil）recvc），即使它们被解释为不同的策略（因此在[（natnat）]上有一个策略可以区分它们）。拉尔德248∼GM[[nat]][[nat]]吉欧，[[nat]][[nat]]你好，P， ，百分比（%）噢，P，.、、、 百分比（%）Oc，，P P[[λx.x]][[newchan λc.λx. （（sendc x;nil）recvc）]]。定义5.1设O为多线程上的最小等价关系在以下条件下关闭的合法sa1t1a2t2br = 0sa1t1a2t2br，如果b是一个O移动，并发指针指向第一个序列中的1，第二个序列中的2，并且序列在其他方面相同。一个策略σ是（并发）指针盲的，如果它是关于σO- 即 s ∈ σ和s ∈ Ot蕴涵t ∈ σ。直接表明，指针盲策略形成一个子类别，其中包含ICSP的所有项的表示指针盲化导致了以下策略之间的定义5.2定义&策略σ，τ：A：σ <$may τ上的等价关系<$may，<$MM，如果对所有ρ：A → [[]]，σ; ρ ↓may当且仅当τ; ρ ↓may。若&对所有ρ：A → [[π]]，σ;ρ ↓必当且仅当τ; ρ ↓必。我们将证明，（无通道）类型对象上的每个紧凑指针盲策略都可以定义为ICSP的一个项，直到等价为止，由此可以得出一个标准论点，即两个项可以（或可能和必须）等价，当且仅当它们的表示可以（可能和必须）等价。然而，首先要注意的是，我们可以直接根据迹上的关系来描述Mr.may和Mr.M，该关系是Mr.O的一个补充。定义5.3令BVP是多线程序列上的最小等价关系，使得sa1t1a2t2br BVPsa1t1a2t2br（如果b是玩家）在第一个序列中移动一个并发指针到1，在第二个序列中移动一个并发指针到2，并且序列在其他方面是相同的。定义序列集上的等价σ：σ <$τ，如果σ s
我的内容管理
展开
