事件结构与π演算：真正的并发模型中的类型化扩展抽象

理论计算机科学电子笔记158（2006）373-397www.elsevier.com/locate/entcs类型化事件结构与π演算扩展抽象Daniele Varacca，Nobuko Yoshida为英国伦敦帝国学院摘要我们提出了一个真正的并发模型的事件结构，保证了有趣的行为特性，被称为无冲突和混乱的类型系统。无冲突是冲突概念的真正冲突版本。 一个系统是混乱的自由，如果不确定性的选择是本地化的，不依赖于独立组件的调度。我们是第一个在真正的并发模型中控制行为的类型系统。 为了证明它的适用性，我们证明了类型化事件结构给出了具有内部移动性的线性类型化π演算的语义。我们提供的语义是π演算的第一个事件结构语义，并推广了Winskel保留字：事件结构，类型，线性，π演算。1介绍并发模型可以根据不同的标准进行分类。一种可能的分类区分交错模型和因果模型（也称为真正的并发模型）。在交错模型中，并发性被简化为在并发动作的所有可能的顺序交错之间的不确定性选择这些模型中的大多数是迹线和标记的过渡系统[35]。 交错模型通过互模拟在定义观测等价性方面非常成功[20]。在因果模型中，因果关系和并发性是明确表示的。这类1电邮地址：varacca@doc.ic.ac.uk，yoshida@doc.ic.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.019374D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373模型是Petri网[25]，Mazurkiewicz迹[18]和事件结构[23]。真正的并发模型可以很容易地表现出有趣的行为特性，例如不存在冲突，选择的独立性和顺序性[25]。在本文中，我们解决了一个特殊的真并发模型：事件结构模型[23，32]。事件结构已经被用来为并发过程语言提供语义最早的，也可能是最直观的，Winskel的本文的第一个贡献是提出了一个事件结构的组合类型系统，确保两个重要的行为属性：无冲突和无混乱。无并发是并发的真正版本。在无冲突系统中，唯一允许的不确定性是由于独立组件的调度。为了说明不太熟悉的无混淆概念，让我们假设一个系统由两个进程P和Q.假设系统可以达到这样一种状态，其中P可以在两个不同的动作a1和a2之间进行选择，并且Q可以独立地执行动作b。 我们说，如果b的出现改变了P可用的选择（例如通过禁用a2，或通过启用第三个动作a3），则这种状态是混乱的直觉上，过程P的选择不是该过程的局部，因为它可以被一个独立的动作所影响。我们说系统是无混淆的，如果没有它的可达状态是混乱的。混淆自由度首先在Petri网理论的背景下被确定[25]。在这种背景下，以自由选择的形式，nets [11].无混淆事件结构也被称为具体数据结构[4]，它们的域理论对应物是具体域[17]。最后，混淆自由度已被认为是概率模型[27，1]的背景下的一个我们提出的类型化系统保证了所有可类型化的事件结构都是无混淆的。一种受限制的类型保证了更强的无冲突性。本文的第二个贡献是给出了π演算的一个片段的第一个直接事件结构语义[21]。π演算存在各种因果语义[16，7，12，5，10，8]，但没有给出事件结构。将CCS语义扩展到π演算的技术难点在于α转换的处理，这是表示名称动态创建的主要成分。 我们能够用π演算的限制版本来解决这个问题，这是Sangiorgi π I演算的线性类型版本这个片段的表达能力足以对类型化的λ演算进行编码（事实上，可以对它进行完全抽象的编码[37]）。我们认为，在这个片段中，α转换不需要动态执行（在D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373375但是可以在键入期间（在“编译时”）通过预先选择将在计算期间创建的所有名称来完成这是可能的，因为类型系统保证，在某种意义上，每个进程都提前知道它将与哪些进程通信。此外，π演算的衍生语义保留了温斯克尔CCS原始语义的直观概念此外，由于我们的语义是根据类型化事件结构给出的，因此我们得到该片段的所有进程都是无混淆的。我们的类型化系统概括了Milner的早期想法，他设计了CCS（一种类型化系统）的语法限制，以保证交织语义的连贯性[20]。 作为我们工作的一个推论，我们证明了一个类似的限制适用于π演算guar-antees的性质的concilient freeness。线性π演算和编程语言语义之间的紧密对应为事件结构语义打开了大门，λ演算和其他函数式和命令式语言。本文结构第2节给出了πI-演算的线性类型版本。本节的启发[37]，但我们的片段扩展到允许非确定性的选择。第三节介绍了事件结构的基本定义，并正式定义了无混淆的概念。第4节介绍了我们的新类型系统和类型的事件结构语义。然后，我们借助于事件结构范畴的态射定义了事件结构类型化的概念。类型化的事件结构在定义上没有混淆。 本节的主要定理是类型化事件结构的并行组合再次被类型化，因此不会混淆。第5节给出了类型化πI演算的可靠事件结构语义。本节的主要结果是πI演算项的语义是类型化的事件结构，因此它是无混淆的。第6节总结了相关的和未来的工作。由于空间限制，用于将π演算转换为类型化事件结构的中间CCS类语言的材料留给完整版本[28]。详细的定义和所有证明都可以在完整版本中找到[28]。2π-演算的线性形式本节简要总结了[3]中π-演算的线性版本到非确定性的扩展[36]。读者可以参考[3，36]，了解更多376D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373|详细描述和更多的例子。2.1还原与还原我们假设读者熟悉π演算的基本定义[21]。正如预期的那样，我们考虑π演算的限制版本，其中只有绑定名称在交互中传递。由此产生的演算在文献中被称为πI演算[26]，并且具有与自由名称传递版本相同的表达能力[37]。从语法上讲，我们将输出限制为f（νy）x（y）.P（其中y表示两个不同的名称的集合），这将有助于我们写出x（y）.P。我们考虑一个比[3]中提出的微积分更一般的版本，因为输入和输出都是不确定的。非确定性输入被称为分支，它已经在[3]中出现，而非确定性线性输出，称为选择，是这项工作的新颖之处。分支类似于微积分的形式语法定义如下。P：：= xi∈Iini（y <$i）.P i |xi∈Iini（y <$i）.P i|P|Q| （νx）P|0|！x（y）.P过程xi∈Iini（y<$i）.Pi（resp. xi∈Iini（y<$i）.Pi）是一个分支输入（分别为 选择输出），其中I表示有限或可数无限索引集合。 PQ是一个伪随机数，（νx）P是一个约束，且d！x（y≠）.P是a复制输入。我们省略了空元组：例如，x代表x（）。当分支或选择索引集中的索引是单例时，我们使用符号x（y_n）.P或x（y_n）.P;当它不是二进制y时，我们使用x（（y_n1）.P1&（y_n2）.P2）或x（（y<$1）.P1<$（y<$2）.P2）。绑定/自由名称的定义与往常一样。我们使用标准α−和结构等价的α和α [21、3、37、15]。所有选择索引集都是单例的过程称为确定性的。分支索引集也是单例的确定性过程称为简单过程。约简语义如下：xi∈Iini（y<$i）.Pi|xj∈J在j（y<$j）中。Qj−→（νy<$h）（Ph|Qh）（h∈I<$J）！x（y）.P|x（y）.Q−→！x（y）.P|（vy）（P|Q）在评价上下文和结构等价下封闭。D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373377123↓↑‡−→|−→|↓↑2.2类型和打字线性类型规则如下限制进程的行为(A) 对于每个线性名称，存在唯一的输入和唯一的输出;以及(B) 对于每个复制名称，存在唯一的无状态复制输入，其具有零个或多个双重输出。在确定性进程的上下文中，类型系统保证了一致性。我们将看到，在存在非确定性的情况下，这种类型系统保证了无混淆性。作为第一个条件的例子，让我们考虑：Qd=ef a. B|a. C|aQd=ef b.a|C.B |a. （c）在|e）、那么Q1是不可类型化的，因为a作为输出出现两次，而Q2是可类型化的，因为每个通道作为输入和输出最多出现一次。简单进程的可类型性（如Q2o）仅表示确定性行为.然而，分支和选择可以提供非确定性行为，保持线性：Qd=efa. （b/c）|a. （de）Q3是可类型化的，我们要么有Q3（b d）或Q3（c）和（e）。 作为作为第二个约束的例子，让我们考虑以下两个过程：Q4d=ef！ B. 一|！ B. cQ5d=ef！ B. 一|B|！ C. BQ4是不可类型化的，因为b与两个复制子相关联：但Q5是可类型化的，因为b处的输出出现两次，而b处的复制输入只出现一次。通道类型由类型变量和操作模式归纳组成：两种输入模式，！，以及两个输出模，？. 我们让p，pJ，。。表示模式。我们定义p，p的对偶，通过：=，！你说呢？所以p=p。类型的语法如下：σ：：=i∈I（σ<$i）↓|i∈I（σ<$i）↑| （σ）！|(σ˜)?（branching）（selection）（ 选择）（请求）τ：：=σ|封闭 式（closed type）在那里，我们的生活充满了欢乐。对于τ的最外模，我们将MD（τ）表示为τ的最外模。τ的对偶，写作τ，是所有作用模式对偶化的结果，具有自对偶性。类型环境Γ是从通道到通道类型的有限映射。有时我们会写378D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373x∈Γ来表示x∈Dom（Γ）。D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373379类型限制进程的可组合性：如果P在环境Γ 1下类型化，Q在环境Γ 2下类型化，并且如果Γ 1，Γ 2“兼容”，则定义一个新的环境Γ 1 <$Γ 2，使得P|Q在Γ 1 <$Γ 2下有类型。如果环境不兼容，则不定义Γ1<$Γ2形式上，我们在类型上引入了一个部分交换运算，定义如下：(1)ττ=τ，MD（τ）=↓(2)ττ = τ，ττ = τ，其中MD（τ）=？然后，环境Γ1<$ Γ2被同态地定义直观地说，（2）中的规则说服务器应该是唯一的，但是任意数量的客户端可以请求交互。 （1）中的规则说，一旦我们组成输入输出线性通道，通道变得不可组合。其他成分不详。 定义（1）和（2）确保了两个约束(A)和（B）。定义类型判断P dΓ的规则与经典π-演算[3]相同，除了一个简单的修改来处理非确定性输出。见附录a2.3一种类型化标号转移关系类型化转换描述了类型化观察者可以对类型化进程进行的观察。类型化转移关系是非类型化转移关系的真子集，但不限制τ-作用：因此类型化转移限制可观察性，而不是计算。标签由以下语法生成：α，β：：=xini（y） |xini（y）|x（y）|x（y）（分支）（选择）（选择器）（请求）τ：：=（x，x）ini（y）|（x，x）（y） （synchronisation）有了上面的记号，我们说x是标签β的主体，表示dassu bj（β），而yj=y1， . . ，yn是对象名称，表示dasobj（β）. 对于分支/选择标签，索引i是标签的分支。符号偏运算α·β 的定义如下：xini （ yi ） ·xin i（ yi） =（x ，x）ini（yi），x（yi）·x（yi）=（x，x）（yi），以及其他的定义。标准的无类型转换关系在图1中定义。我们定义了谓词380D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373−→\12i∈I我我−→Pji∈I我JJa（y）an（y）a（y）.Pa（y）ainj（yj）a（y）.P！a（y）.P−→P|！a（y）.Pa（y）.P−→PP−β→PJP|Q − β → PJ|QP−α→PJQ−β→QJobj（α）=yP|Q−α→·β（νyθ）（PJ|QJ）P−β→PJsubj（β）xP<$PJPβQα（νx）P−β→（νx）PJPJ−β→QFig. 1. πI演算的标号转移系统服务能力y：对于所有的Γ，Γ都是τ;如果MD（Γ（x））=↓，则nΓ都是xini（y）;并且如果MD（Γ（x））=！，则x（y_n）都不为零。 当MD（r（x））=↑，？ 被定义为双重的。直观地说，标签只有在类型环境与它们一致时才允许只要Γ允许β，我们就定义一个新的环境Γβ来表示β标记的跃迁发生后剩下的东西。使用线性通道，而不使用复制通道释放了以前绑定的新通道。例如，如果r=Δ， x：i∈I（τ∈i）↓，βr|xin（yn）=Δ，yn=τn。当这种类型的过渡，写作PDΓQDrJ是我通过添加约束来定义：β β如果P−→Q且Γ允许β，则P DΓ−→QDΓ\β当过程中存在互补通道时，上述规则不允许线性输入动作和输出动作。例如，如果一个进程有x：（τ）！在其动作类型中，则排除x处的输出，因为在类型化上下文中永远无法观察到这样的动作- cf。[3]的文件。对于一个具体的例子，考虑过程a.b| b. a，在环境中输入a：b，b：c。虽然进程有一些无类型的转换，但它们都不被环境允许。通过对图1中规则的归纳，我们可以得到：β命题2.1（i）若P D Γ，P−→Q且Γ允许β，则QD Γ\β。(ii) （Subject约化）IfPDΓ且P−τ→τQ，thenQ DΓ.(iii) （教堂 Rosser 对于确定性过程）设P DΓ和P为决定论 假设P−τ→τQ，且P−τ→τQ。 陈清 Q或RexistsR使得Q−τ→τ1 2R和Q −τ→τR。1α2我−→Pj−→D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 158（2006）373381联系我们|}最后，我们定义了类型互模拟的概念设R是判断之间的对称关系，使得如果（PdΓ）R（PjdΓJ），则Γ = ΓJ.我们说R是互模拟，如果满足以下条件：• 当ver（PdΓ）R（PJdΓ），PdΓ−β→QdΓ\β时 ， 存 在 Qj使得PJd Γ−β→QJdΓ\β，且（Qd Γ\β）R（QJd Γ\β）.如果两个判 断之间存在互模拟 ，我们称它们 是互相似的（ P dΓ ）<$（PJdΓ）。请注意，这是一个全等关系[28]。3事件结构事件结构由Nielsen，Plotkin和Winskel [23，30]引入，并一直是几项研究的主题。它们以不同的形式出现。 我们在这项工作中介绍的结构有时被称为素事件结构[32]。对于事件结构与其他并发模型的关系，标准参考文献是[35]。3.1基本定义一个事件结构是一个三元组E=E，≤，×，使得• E是可数事件集;• 是偏序，称为因果序;• 对于每个e E，集合[e]：=eJeJ

下载后可阅读完整内容，剩余1页未读，立即下载