（计算机软件与理论专业论文）对称π演算和lambdaπ演算的综合对称λπ演算.pdf

摘要 ， 计算机软件理论发展至今，研究焦点已从顺序计算转移到了并行计算。q 顷序计算可以很容易地理解 成函数式计算，而a 演算模型则是函数式计算的最佳形式化工具。利用它，人们很容易就解决了函数式 顺序计算中的许多理论问题，并在实践中得到了印证。并行计算则因其本身的复杂性和不确定性，从一 开始就对理论工作者提出了很高的要求。从m i h 、e r 提出c c s 以来，各种从不同侧面反映并发本质的模 。型被相继提出。在这些模型中，进程代数( 如c c s ) 因概念简洁，可用的数学工具丰富，得到了广泛的研 究。w ，演算是对c c s 的继承和发展。 从进程代数的观点来看，尽管用”演算来描述并行模型还有很多工作需要去研究，但是人们也同时 着手探讨用新的通信机制来描述并行计算，而且在试图寻找一种将并行计算和顺序计算直接统一起来的 模型，这样做可能可以对进程代数的研究带来一些有益的启示，1 本文提出了对称a 一”演算，然后针对它 进行了系统、深入的研究，给出了 演算与”演算均是它的子语言的证据，我的主要的工作包括以下几 个方面： i 将两类w 演算变体的特点综合。给出了对称a ”演算的模型； 2 将”演算翻译成对称a ”演算及给出了完全刻划定理j 3 将a 演算翻译成对称a 一演算， 。以上所作的研究工作很有价值。对称”演算无输入输出之分，l a m b d a ”演算中进程与通道没有 区分。牌这两类”演算的特点综合，可以得到一种新的”演算模型，称之为对称a ”演算。本论文定 义了这种新演算，并且给出它的操作语义，文中还将探讨如何用它来翻译”演算，针对”是对称a ” 的子语言，我们试图给出能用对称a n 演算来完全刻划w 演算的证据在各种互模拟中我们考虑接 口( b m b e d ) 互模拟，这是因为接口互模拟最能比较两种语言的表达能力和区分能力。文中最后给出了 a 演算在对称a 一”演算中的翻译，可以看到这种翻译很方便直接，这主要得益于对称a ”演算的简洁性。、 关键词：”一演算，进程，通道，完全刻划，互模拟，子语管 a b s t r a c t t ot h e s ed a y s ，t h ef o c u so fc o l l l p u t e rs o , w a r et h e o r yh a v eb e e nc h a n g e df r o ms e q u e n t i a lc o m p u t i n g t op a r r a l e lc o m p u t i n g s e q u e n t i a lc o m p u t i u gc a no b v i o u s l yb ee x p l a i n e da sf u n c t i o n a lc o m p u t a t i o n t h e a - c a l c u l u si st h eb e s tp r o t o t y p i c a lm o d e lf o ri t b a s e do ut h i s ，p e o p l ec a l le a s i l ys o l v el r l a l l yp r o b l e m sa b o u t s e q u e n t i a lc o m p u t i n gt h e o r y a n dt h e s er e s u l t sh a v eb e e np a s s e di np r a c t i c e y e tp a r r a l e lc o m p u t i n gt h e o r y r e q u i r e st i l es c i e n t i s t st ow o r k i n u c hl u o r eb e c a u s eo fi t si n t r i n s i cc o m p l e x i t ya n di n t e r o p e r a b l i t y s i n c em i l n e r p u t sf o r t hc c s j1 y i a n yc o n c u r r e n tc o m p u t a t i o nm o d e l sh a v eb e e ns t u d i e d a m o n gt h e s em o d e l s ，p r o c e s s a l g e b r a ，s u c ha sc c s ，a r ew i d e l ys t u d i e db e c a u s eo fi t s c o n s c i s ec o n c e p t sa n dr i c ha v a i l a b l em a t h e m a t i c a l t o o l s t h e - c a l c u l u si st l l ei n h e r i t a n c ea n dd e v e l o p m e n to fc c s f r o mt i l ev i e w p o i n to f p r o c e s sa l g e b r a ，i us p i t eo fd e s c r i b i n gc o n c u r r e n c yw i t h - c a l c u l u sr e m a i n sl l r u c h r e s e a r c ht od o ，p e o p l eh a v eb e g u nt ol o o kf o rn e wc o m m u n i c a t i o ne s s e u c ea b o u tc o n c u r r e c ya n dt od e v e l o p n e wm o d e lt om o d e ls e q u e n t i a lc o m p u t i n ga n dp a r a l l e lc o m p u t h l g t h en e wr e s e a r c ha b o u t p r o c e s sa l g e b r a c o a lb r i n gn e wo p i n i o n s t h i st h e s i s g i v e ss y n u n e t r l ca - c a l c u l u sa n dd o e ss o m ed e e pr e s e a r c ha b o u ti t t h ep r o o fo fa - c a l c u l u sa n d - c a l c u l u sb e i n gs u b l a n g u a g e so fi ti fp r e s e n t e d t h em a i nt a s ki n c l u d e st h e f o l l o w i n gt h r e ea s p e c t s ： 1 i n t e r g r a t i n gt h ec h a r a c t e r so ft w ov a r i a n t so fn c a l c u l u s ，an e we o m p u r i n gm o d e l s y n n n e t r l ca - fc a e u l u s ，i sg i v e n 2 e m b e d 一c a l c u l u si n t os y m m e t r i ca - wc a l c u l u sa n dt i l ef u l la b s t r a c t i o nt h e o r e l ni 8 g i v e l l 3 ad i r e c ti n t e r p r e t a t i o nf r o ma - c a l c u l u st os y m m t r i ca - c a l c u l u si s p r e s e n t e d t h ea b o v et a s ki so fs i g n i f i c a n c e t h e r ei s1 1 0d i f f e r e n c eb e t w e e n i n p u ta n do u t p u tp r e f i x si ns y x m n e t ￥i c 口c a l c u l u s l a m b d a - 丌c a l c u l u st r e a t sp r o c e s sa n dc h a n n e la sa8 a l n eo b j e c t t oi n t e g r a t et h ec l l a r a c t e r so f t h e m ，an e wc o m p u t i n gn l o d e l ，s y n l m e t r i ca - 丌c a l c u l u si si n t r o d u c e d t h i st h e s i sd e f t n e 8t l l i sn e wc a l c u l u s a u dg i v e si t so p e r a t i o n a ls e l l l a n t i c s w e “d i s c u s sh o wt ou 8 ei t t oe m b e d w c a l c u l u s c o n 8 i d e y h l zb a r b e d b i s i n f i l a r i t y ，t h ep r o o fo ff u l la b s t r a c t i o ni sp r e s e n t e dt o o b e c a u s eo fi t ss i m p l ef o n m ，ad i r e c ti n t e r p r e t a t i o i l o f 一c a l c u si so b v j o u 8 k e y w o r d s ：f c a l c u l u s ，p r o c c s s c h a n n e l ，f u l la b s t r a c t i o u ，b i s i n f i l a r i t y 。s u b - l a n g u a g e i i 第一章引言 1 1 研究背景 在计算机理论科学的领域中，用形式化的方法来研究计算是十分必要和有效的手段，形式化的方法 可以为研究工作引入大量的数学和逻辑的方法，这是理论研究中最为精确的研究手段。通常，用 演算 来描述顺序计算模型，这种方法已经非常成熟并且在几乎所有顺序计算的实践中得到了验证，反过来它 又通过形式化的数学和逻辑方法为顺序计算问题提供了验证手段。然而，并行计算以其独有的复杂性和 并发行为的不确定性给计算机理论工作者提出了巨大的挑战。o ( j 年代初，m i i n e r 提出了”演算，它是 目前被研究得最为广泛最为深入的一种并发演算模型。全世界许多学者和专家针对”演算纷纷以自己独 到的眼光提出了各种改进的形式。其中引人注目的还有一个唰题就是：如何为顺序与并发的计算模型提 供一个一致性的形式化描述模型。 傅育熙教授提出了一种对称的”演算模型。无输入输出之分的对称n 演算 1 的特点是：从通信角 度讲，它没有输入与输出之分，是在共有的通信通道上交换名字，是对称的，其中关键点是它没有抽象 名。它的改进之处在于将”演算中的输入输出两种行为用一种来表达，大大简化了”演算，为对它的更 深入的研究作了很好的铺垫。 傅育熙教授还就顺序与并发计算的一致性描述模型提出了一个l a n l b d a 一”演算的模型。通道( c h a n n e l ) 与进程( p r o c e s s ) 统一的l a r n b d a - ，r 演算【2 【3 】的特点是：通道与进程是不区分的，都被看成是同一 种名，都可以通过通信进行交换或转移。这样的处理大大增强了z 演算的描述能力，通过将”中的通道 与进程看成同一种名，很容易证明 演算是l a m b d a w 演算的子语言。 本文就是在这样的背景下，提出了将对称”演算与l a m b d a 一”演算两者综合起来，得到一种新的演算 模型，对称 - 一演算。它充分利用了这两种演算模型的长处。应当来讲它是一种较为理想的计算描述模跫。 1 2 主要研究内容与成果 。 本文提出了对称a 一”演算，然后针对它进行丁系统、深入的研究，给出了a 演算与”演算均是它的 子语言的证据，我的主要的工作包括以下几个方面： 1 将两类”演算变体的特点综合，给出了对称a ”演算的模型， 2 将一演算翻译成对称a ”演算及给出了完全刻划定理， 3 将a 演算翻译成对称a ”演算i 本文的主要成果就是提出了一种新的计算系统描述模型，对称a 一”演算，这种演算模型的特点一是 第一章引言 2 对称的，二是兼有a 演算及w 演算的特点。 回顾历史，从描述顺序计算的 演算到描述并发计算系统的模型c c s ，w 演算及它们的各种变体， 所有这些演算模型在重写系统，精确验证，形式化研究等各个方面均产生了重大意义。在本文中，我们 就是在这样的背景下研究了一种新的进程代数演算模型，对称a ”演算，该模型较之以往的各种演算模 型，它汲取了众家之长，抓住通信机制不同这个各种并发计算模型的本质区别，开创了一个新的描述模 型。在通信机制上它采用的不区分输入输出动作，而且把通道与进程看成同一个实体这样处理大大增 强了它的概括能力，简化了以往并发计算系统的行为区别，也简化丁研究实体，抽象层次更高，描述层 次更高，它把”演算作为一个子语言来处理。同时时为它简化了研究实体，它具有了 演算的简洁的特 点，它能更方便地将a 演算作为一个子语言来处理。从本质上讲，它将输入输出看成同一种动作，将通 道与进程也看成了同一种实体，自然它具有简洁的特征，因此它能用更简洁的方式来抽象研究对象和处 理问题，是一种强有力的工具。从形式上讲，对称a 一”演算没有抽象名与局部名的区别，没有输入输出的 区别，没有通道与进程的区别。如此高层次抽象的演算模型，它的撒述能力到底会有多少损失，本文用 了大量的篇幅论述和证明了它能完全刻划”演算和 演算的描述能力，同时文中也给出丁一些例子。 1 3 论文结构 本篇论文的结构基本上是按研究工作的顺序进行组织的，总共分为六章。除本章是综述性的概论之 外，其余各章组织如下： 第2 章对进程代数的发展作了一个概述，c c s ，一演算，特别着重叙述了对称”演算与l a m b d a 一” 演算。 第3 章提出了对称a 一”演算，给出了它的定义和操作语义。 第4 章讨论了将一演算翻译成对称a w 演算，并给出了一些实例j 考虑接口互模拟，证明了翻译是 完全刻划的。 第5 章研究了将a 演算翻译成对称a w 演算，由于对称a 一”演算的简洁性，因此这种翻译是很直接 的，文中还阐述了这种翻译不损失a 演算中的归约语义。 第6 章简要总结了本文的主要成果，并阐述了对后续研究工作的一些没想。 第二章进程代数简介：c c s ，丌演算，对称丌演算与l a m b d a 一丌演算 2 1 c c s 众所周知，顺序程序可以看作变换式系统。程序根据对每个输入其停机时的输出指称一个函数，程序 等价可以看作函数相等。并发系统是典型的反应式系统，进程行为表现为与环境的交互事件流。c c s 将并 发系统抽象为：独立实体执行不可分割的原子动作，通过共享通道进行同步通信；进程并发理解为动作以 不确定次序交错发生。c c $ 虽然只含有动作前缀、并发合成、非确定性选择、限制、换标号干仃递归等进程构 造算子，但描述能力很强。c c s 之所以能成功地应用于并发系统建模和程序验证，除了强大的描述能力之 外，主要得益于基于互模拟概念的行为等价语义的建立和完善，它提供了一种强有力的手段和方法，能很 好地帮助人们分析和验证用它捕述的并发系统。互模拟等价是进程代数中最常用的等价关系，并且根据是 否忽略表示内部通信的t 动作分为强互模拟等价和弱互模拟等价两种。基于弱互模拟的观察同余关系是 在实际应用中最重要的等价关系。这些基于互模拟的等价关系具有良好的数学性质，便于进行组合验证。 我们以x 来表示进程变量的集合，k 表示进程常量的集合。e 是包含x ，k 与下述表达式的 最小的集合，在下述表达式中的e ，蜀属于e ： ( 1 m e ，前缀形式( “a c t ) ( 2 ) e 。，求和形式( j 是一个索引集合) 。当= 0 ，记e 为0 ，当j = 1 2 ) 时，记 ( 2 ) ，j e 。为e 1 + e z ， ( 3 ) e 。i e 2 ，组合形式 ( 4 ) e l ，受限形式( l cc ) ，表示lu 五中的动作被禁止 ( 5 ) f f ，】重标号形式( ，是一个重标号函数) ，e l i 】的行为方式与e 相同，但其中的动作名都经过f 的替换 且是名集合，五= i 卜a ) 为相反名集。c = a u 五r 代表静态动作，动作集合a c t = cu r 重标号函数f 从c 映射到，使川) = 7 而。若定义， r ) = r ，就可将f 的定义域扩大到a c t 。 为避免过多的括号，规定算子的优先级按以下顺序递减：受限和萤标号，前缀，组合，求和。因此， r + m r i b o l 就相当于r + ( ( “p ) l ( b ( o l ) ) ) 。 转移规则列示如下： ( ee e 墨兰墅! ! 毛。 f 。与彰 3 第二章进程弋数简介：c c s ，* 演算，对称”演算与抽”b d 一演算 4 e 二e 1 i i 互面f m f 二p c ，b ，l h e l f 二斟f 。 e 上e ，f 上f ， 一_ 一e l t t rr t 3 e e r r ，行l r p n e l 。e l l e 三e 而酉丽吼7 p p ，a = p 。+ 1 。1 1 。1 。c or b a 一p ， c c s 之所以能成功地应用于并发系统建模和程序验证，主要得益子基于互模拟概念的行为等价语义 理论的建立和完善。由于互模拟关系具有清晰的物理背景和良好的数学性质，为并发系统的分析和验证 提供了一种强有力的手段和方法，故在进程代数中占有显著地位。 尽管c c s 中有许多规则，它们可被划分为有不同特性的类。这是由于c c s 算法的算子可分为两类。 第一类包含组合、受限和重标号算子，它们被成为静态算子。这些算子的动作规贝都是如下形式： e 。兰- e 。 e 兰马e ：。j c o m b ( e ，e 。) sc o m y ( e e ： 其中 i 1 ，i 。) 是 1 ，7 1 , ) 的子集。如果i f i 一一i ，j ，e ；和置一样。要点是算子c o m b 在 动作前后都被保存。而且，那些改变了的成分仅仅是那些以自己的动作参与了复合进程的动作的成分。 任何由静态算子建立起来的形如c e 一e 1 的结构在动作中保持它们的结构。这就是为什么组合、受 限和重标号可看作是在流程图上的操作：它们代表的结构不被动作所干扰，因而被成为是静态结构。这 种结构指明了成分之间是怎样被连接起来的，界面的哪些部分被隐藏或是内部的，以及端口是怎样被标 。 号的。 第二类包含被称为动态算子的前缀、求和、常量算子。在这些算子的任一条规则中，这些算子在动 作前出现，在动作后消失。 由此可将所有的规则分为三类： 静态规则，只涉及到静态算子。这些规则可被认为是流程图的一个算法。 动态规则，只涉及到动态算子。这些规则可被认为是传递图的一个算法。 第二章进程代数简介：c c s ，”演算，对称”演算与撕n b d m n 演算 5 将以上两类规则联系起来的规则，即扩展规则( e r p m t s j h l m ) 。它根据p l ，一，的动作给出 n ，r 静态组合的所有动作。 c c s 理论的一个重要的基石是瓯模拟概念及其证明技术。两个动态系统之间可以有一种固定不变的 关系，可通过构造这样一种固定不变的关系的方法来求证这两个系统等价。要区分两个进程p 和0 ， 我们直观地想到可利用一个外部进程，使它与p 和0 分别发生作用，若得到不同的结果，则表示p 和 q 有区别，反之p 和q 不能被区分。 - 我们将内部动作r 和其他动作完全一样对待，得到一个相当严格的等价关系，我们称之为强等价。 如果我们把r 当作一个不能被外部进程观察到或鉴别出的内部动作，就相应地得到一个较弱的等价关系 可观察等价。 下面分别给出强互模拟和弱置模拟的定义。 定义2 1 一个建立在进程集合p 之上的二元关系s p 十p 是强互模拟关系，意味着当( p 口j s 时， 对任意，r a c t ，满足以下两个条件： ( i ) 如果p 三p ，那么存在q ，0 三q 且( p q ) s ； ( j i ) 如果q o ，那么存在p ，p p 7 且( p 7 ，q ) s 强互模拟关系一具有良好的数学性质，即是等价关系，又是同余关系，并可用泛函数的最大不动点 来定义。 i 互模拟的另一吸引人之处，是对于有穷状态系统存在多项式时间的判定算法。该算法成为进程代数 自动验证工具的基础。 就c c s 全集来说，其计算能力和t u r i n g 机等价，其互模拟是不可判定的，也不可公理化。但对于 有穷进程和有穷状态进程，其强互模拟等价和观察同余均是可公理化的。 对于一个外部观察者而言，他不关心表示进程内部通信事件的r - 动作，而只关注外部可见的行为动 作。如果在互模拟的匹配和比较中忽略表示内部通讯的r 一动作，就可导致一类最莺要的互模拟等价关系 一弱互模拟。 定义2 2 如果t a c t ，那么剔除t 中的所有r 动作后，得到i 、l + 。 定义2 3 一个建立在进程集合p 之上的二元关系s p 十p 是弱互模拟关系，意味着当( p ，q ) s 时， 对任意n a c t ，满足以下两个条件： ( i ) 如果p 三p ，那么存在q ，o 当o 且( p ，q ) sj ( i i ) 如果q 三q ，那么存在p ，p 当p 且( p 7 0 ) s 定义2 4 如果对某个( 弱) 互模拟5 ，( 只q ) s ，p 和q 被称为可观察等价或( 弱) 互模拟，写为 。 p q 。即，= u s ：s 是一个互模拟1 。 弱互模拟关系虽然是等价关系，但不是同余关系，不能被非确定选择算子或+ 所保持。因 此，由弱互模拟关系可进一步导出一种同余关系一观察同余。在实际应用中，基于弱互模拟的观察同余 关系是最常用的行为等价标准。 第二章进程代数简介：c c s ，演算，对称”演算与l , 一m b m 一演算 定理2 1 设s ( j = 1 2 ，) 是一个互模拟，以下这些性质对每个互模拟都成立 ( 1 ) ，“ ( 2 ) s l 岛 f 3 1 s l ( 4 ) u ，z s i 证明：由互模拟的定义很容易证明。 定理2 2 满足以下性质 f i ) 是最大的互模拟 f i i ) 是一个等价关系。 证明：r b 定理2 1 很容易证明。 定义2 5p 和0 是等价的或者说是( 可观察) 同余的，写为p = q ，如果它们满足以下条件：对任意 ( i ) 如果，三p ，则存在某个q ，q 当q 且p q ? u i ) 如果0 臼”，则存在某个p ，= 多p 且p 0 定理2 3 设c ( p ) u c ( q ) c 。那么p = 口当且仅当对任意的7 ，p + 冗q + r 。 证明：( = ) 很容易证明以下关系是一个互模拟： ( p + r ，q + r ) ：p q ，r p ，p = q u ( = ) 用反证法。设p q 。那么，只要证明存在n 和p ，使p 土+ p ，但是对任意的q = 与q ， 有p 聋q 。选择r 兰1 0 ，其中j 不在p 和q 的类别中。显然，p + r 生p ：因此必须证明如果 q + 冗= 与0 ，则p 簪q 。如果“= r 则q ；q + 7 。q 有? 动作而p 没有，因此p 聋q i 否则， q + 冗= 昌q ，因而q = 与q ( 因为“f ，所以冗= 与0 是不可能的) 。因此再次得到p q 。 定理2 4 由p q 可得p = q ，由p = q 可得p q 。 证明t 由互模拟的定义可得到这样一个事实；每个强互模拟也是一个互模拟。因此马上可得如果p q ， 则p q 的结论。由强互模拟的条件和= 的定义，可得如果p q ，则一定p = 0 。 在第二部分，由定理2 3 ，p = q 意味着p + 0 0 + 0j 但是p + 0 p ，因而p + 0 p ，因 此可得p o 。 定理2 5p q 当且仅当( p = q 或p = r q 或r p + 驯。 证明：( # ) 由定理2 4 可得如果p = o ，则p q 。其他的情况可由p r p 导出。 ( = j ) 设p 0 ，考虑三种情况。首先，设对某个p ，p p 。oi 那么可容易地得出p = r q 。 第二，设对某个q 7 ，q q z p ；类似地可证明r p = q 。如果以上两种情况都不成立，那么可如 下证明p = q 。首先，设p 三_ p ，因为p q ，则0 = 与q p ，即0 占q p 。在另一方 面，如果j ) p ，则q = j ，且根据假设不可能是q 本身，由对称性可得，= 印。 第二章进程代数简介：c c s ，”演算，对称”演算与l m n b d * ”演算 7 2 2”一演算的模型描述 ”，演算是在c c s 的基础上发展起来的，最初由m i l n e r 、p a r r o w 和w a l k e r 提出。n 一演算的最大 优点是可以用来捕述结构不断变化的并发系统，这里的结构变化既包括并发系统中进程状态的变化，也 包括随着进程状态不断变化而导致的进程之间联结关系的改变。 下面先给出两个例子以便读者对”演算有一个初步的认识。 1 有一个并发系统，该系统中有两个进程p 和r 。a 是p 和r 之间的通道，p 将值5 通过a 发 送给r ，r 可以r ha 接收任何值。系统可用下面的流程图来表示： p ；i 5 p ，冗en 引r 。前缀“( a ) 将变量a - 限制于进程冗7 内。可用下面的式子描述本系统 。后缀操作的含义是通道c - i 只属于进程p 和i t 私有，对于进程p 和r 之外的其它进程a 是不可见 的。 现欲在该系统中增加一个进程q ，p 和q 之间的通道是b 。在原系统中进程p 发送值5 给进程 r ，现在我们希望转由q 发送给r 。p 与q 的初始联结为b ： 在新系统中p i5 n - 5 p ，b 发送通道a 和将由a 发送的值5 。q ；b ( ) 6 ( 2 ) 乳o q 通过b 接收一 个通道名和值，然后由这个通道将所接收的值再发送出去。细心的读者不难发现a 没有在q 中出现，也 就是说在初始状态时，q 和r 之间没有任何联结。整个系统可用下面式子表示： f 乩6 5 ，- ) 伽( ) 州z ) 融，i 】眦叫r ，) “6 在两次通讯后，系统演变为 ( ，i i 5 o m ( z ) r ) ( 1 6 如果a 不在p 中出现，我们可以认为p 的a 通道被移到丁q ，而q 变成了0 ，! i 5 0 ： 第二章进程代数简介：c c s ，”演算，对称”演算与l , 一m l t m l 一”演算 8 2 考虑如下进程 y y m ( ) i h 圳i ：u 我们可以把它简写为 爵j z ( “) 订i ，| 雨z 并称它为p i q i 冗。在通道x 上每次只能有一个通讯发生，或者是p 发送y 到q ，或者是r 发送z 到 q 。通讯后的两种结果分别是。咖l i z 和劫融i o 。这时q 已变为弘或i q 可用的下一个输出通道 是y 或z 。 如果上面进程变成如下形式： ( 引i j z ( “) 可l ，l 矾 在这种情况下，r 中的自由名x 与p 和q 中的受限名x 是不同的。所以，这时只有一种通讯情况可能 发生，得到： 0 咖f 瓢 受限操作符( x ) 由于在通讯中已完成了它的使命，所以不再出现。 在考虑下面这种情况： 可f ! z ( “) 可f ，陋 这与第一种情况又有很大区别，因为这时q 是复制形式。这时的通讯结果是 。胁l1 0 i 融 旧再与r 发生通讯，得到： o 咖l ! q 胁j o - 演算与传值c c s 的区别在于被传送的内容只能是名，这一限制使我们能够得到并发计算的一个 封闭模型。设为一名集，其中的元素用小写字母表示。所有* 一进程组成的集合c 由b n f 定义的对 象构成： p ：= 0 ln ( 。) p i 矶p ip + q fp i q l ( z ) p i ! ，i 陋= y p 它们的意义解释如下： 1 o ：表示非活动进程，它不能进行任何操作； 第二章进程代数简介：c g s ，”演算，对称”演算与l a m ! 州演算 9 2 。( 。) ，：进程的输入前缀形式，此进程接在通道“的输入端口，它必须先通过“接收，然后启 动进程，【叫，( t ( ) 【l 可简化为r t ( ) 3 万一p ：进程的输出前缀形式，此进程接在c v 的输出端口，它必须首先通过“将。传出，然后启动 进程p ，砷- 0 可简化为砷，读者应该注意n ( a 。) p 中的a 。是受限的，而万n ，中的。是自r 的； 4 p q ，q ：这是进程的不确定形式。此进程将根据一定的诱囚来激活p 或q ，若被激活的进程是p ， 则整个进程所表现出来的行为就是p 的行为，反之亦然j 5 尸i q ：进程的并行操作形式，p 和q 既可各自独立地进行，也可通过共享的通道相互进行通讯； 6 ( z ) p ：进程( z ) p 中的名a ，是一个受限名，它使得进程_ p 无法通过z 与其它进程进行通讯； 7 ! p ：表示p 的一组无限拷贝； 8 陋= p ：这是一个条件进程，如果r = y ，它将激活进程p ，否则等同于进程0 。 另外一些必要的说明如下所示： ，n ( p ) 表示所有在p 中出现的自f h 名，即既不属于输入前缀中出现的受限名，也不属于约束受限 名。我们用o n ( n ，b ) 来表示，n ( n ) u f n ( 马) u 。 如同在 演算中一样，我们不区分那些可m 转换的进程，即那些只是受限名不同的进程。我们以 p i q 表示p 和q 可n 转换。 有时，我们以来表示名矢量z 1 ，。，其中n 可从上下文中得出。 我们以尸f i 。l ，如i x 。) ，或p y i z i i s ，! 。或_ p 船卢) 表示以弘代替尸中所有自由变量q 的 动作同时发生，如果有必要，可改变受限名以防新名y ；在p 中受限。 在前缀“驰”和”( 引”中，我们称y 为主体，z 为客体或参数，那些处于主体位置的自由名决定 了一个进程当前的通讯能力。 在w 演算中，有如下四种动作： 1 静态动作r 。如同在c c s 中一样，p 0 意味着p 能够演化为q ，并且在演化中，不要求和 环境发生作用。静态动作能自然地发生于形如r p 的进程，也能在一个进程的内部通讯中发生。 2 自由输出动作动。p 二马0 的转化意味着p 能在i 端口上输出自由名y 。自由输出动作发生 于输出前缀形式的进程动p 3 输入动作m ( ) 。直观地，r = 掣0 意味着p 能在端口z 上接收任何名“，然后演化为0 m 知1 。 我们注意到这与c c s 中一个输入动作包含接收到的实际值的情况很想象。不同的是，在”演算中，( ) 指向被接收的名将被安置的位置，两旁加上括号以强调这个事实。输入动作发生于输入前缀形式的进 程。( 】p 。 4 受限输出动作面( f ) 。这种动作在c c s 中没有对应的动作。直观地，p 坠掣0 意味着p 在端口虿 上输出一个私有名( 在p 中受限的名) 。( ) 指向这个私有名的位置，如同在上面的输入动作中，y 的 两旁加上括号以强调指向位置，而并不代表值。受限输出动作发生于形如( ) 珂p 的进程中。 静态动作和自由输出动作被统称为自由动作，而输入动作和受限输出动作被统称为受限动作。自由 第二章进程代数简介：c c s ，”演算，对称”演算与l t m f l ，d a 一”演算 图2 1 ：弘演算的四种动作中的受限名和自由名 输出动作和受限输出动作被统称为输出动作，有时被称为负动作( 带负极的动作) 。类似地，输入动作被 称为正动作( 带正极的动作) 。参与一个内部通讯的两个动作必须带不同的极性。 在以上提及的输入输出动作中，刊睦主体，是客体或称为参数。客体在受限动作中是受限的， 在自由动作中是自巾的。如果“是一个自i 士动作，r r 中的受限名的集合h ( n ) 是空集；反之，它仅包含 cr 中的客体名。一个动作“中的臼由名的集合，t 。( r t ) 包含c r 的主体名和自由客体名( 如果存在) ，。( “) 是b n ( n ) 和，礼( “) 的并集。注意，n ( r ) = 0 。图21 是对这些定义的一个总结。 下面的规则定义丁一演算的操作语义。为了简单起见，我们省略了对称规则： _ = 1 a u a c t t p ：- p ；i ；_ = i i ：7 0 矿t p 矿t 一 e t “，岳，7 i ( ( z ) p ) z ( z ) p2 5 ) p w z ，n p u t a c t p ! + p i 面跗m p 三p 五面j = _ 7 m a t e h p 9 ) 三p j 4 ( ) d = e f p 丽j 5 一佃e p lp 7 b ( n ) n f n ( q ) = 瓦五i f 一肌r 第二章进程代数简介：c c s ，”演算，对称”演算与抽n b d * ”演算 p ! 匕，q 旦卫q 一c d p f q p q z ) ，掣p ，a 掣q el f ) s e p q ( ，) ( ，f 0 7 ) r 叶_ p 仨n ( r y ) r e s t 【 、p 二tu 1 p p 二二p 7 ，仨f n ( ( ，) p ) t p 掣p m 抽、 定义2 8 一个进程上的二维关系上是一个( 强) 模拟关系如果p q 意味着 1 如果_ p p 且n 是一个自由的动作，那么存在某个0 q 与q 7 且p o q ； 2 如果p ! 掣p ，且yg 札( 只q ) ，那么存在某个q ，q 型掣0 且对所有“，p i “，乃卜q 训) j 3 如果p 三掣p ，且g7 l ( 只q ) ，那么存在某个，0 三掣q ，且p i 。q ，。 如果关系。和它的逆都是模拟关系，则关系之称为互模拟关系。两个进程互模拟( p o q ) 当且仅 当存在一个互模拟关系土，使，o q 很容易证明。是一个互模拟关系，且是最大的一个互模拟关系。 定义2 7 如果对任意替换d ，有p d 之q 6 则称p 和q 强等价，即p q 有关”演算和c c s 的比较： c c s 模型主要有以下不足之处：它是建立在极小原语集上的函数式程序设计语言，因而不能够很好 地描述一个无穷扩展的并行系统。这是它最大的缺陷。 ”演算是对c c s 的扩展。它在保持了c c s 的代数性质的同时扩展丁其并行计算能力。c c s 中有 通道名和变量名之分，而在z 演算中两者被统一成名( u a m c ) 。”演算中的计算实体只有名和进程，进 程之间的通讯是通过传递名来完成的。由于可以传递通道名，所以n 演算可以用来描述结构不断变化的 并行系统。所谓结构不断变化的并行系统是指进程之间的连接关系可以随着进程状态的不断变化而发生 改变。它与c c s 的一个最大不同之处在于它是一个封闭的计算模型。 2 3 对称”演算 正如引言中所述的有关并行系统的进程代数的研究发展历史，自从w 演算提出以来，人们纷纷试图 用它解释有关的并行通信。其中人们自然而然的发现到，”中针对通信实质的部分，它是严格地将通信 第二章进程代数简介：c c s ，”演算，对称”演算与l b d a ”演算 12 的两个相对部分分为输入与输出的，其定义中就将输入输出严格区分开来。对照客观世界中的实际，的 确大多通信的两个方面，均有一个是发送方一个是接收方，如：老师向学生授课；跑步比赛中发令员向 运动员发令。但是试想如下一些情形，打电话舣方同时向对方说话，难道这样的通信非要分成两个通信 动作，我们不妨可以将这种通信抽象为没有输入输出的区别，只是在某个通道上交换信息 这样从交换 为机制的通信在现实中更为普遍几乎每个单方向的通信均可理解为俯息的变换，接收方难道没有给发 送方一个回应吗，只是单方向的通信机制将这种回应又理解为另外一个通信动作。总之，可能是鉴于这 种考虑，引入了交换的通信机制，这种处理可以在某种意义上加大了通信的能力，拓展了人们对并行系 统通信的实际的思考。在这个基础上，傅育熙教授提出了对称的”演算，无输入输出之分的对称”演算 f 9 的特点是：从通信角度讲，它没有输入与输出之分，是在共有的通信通道上交换名字，是对称的，其 中关键点是它没有抽象名。用b n f 定义它的进程如下： 注意到它与传统的”演算的定义的区别在于： 1 。它没有单独的输入输出动作，而代之以一个统一的交换名字的动作。 2 。因为有e x p a n s i o nl a w 故未考虑s u m 算子 为便于对对称w 演算的本质进行研究，该定义中省略了传统的标准”演算中的m a t c h 和m i s m a t c h 等算子，得到这种简洁的只剩下了五项定义，这主要归功于将输入输出动作不加区分。 根据以上的定义，那么对称”演算应当具有什么样的操作语义呢? 从如下给出的操作规则，我们不难看 出它与传统的标准z 演算的本质区别就在于通信中是交换名字，而且不带有抽象名： 顺序规则： 并行规则 通信规则 ygb n ( p ) 面石可甄5 些坚p i 差q 娑p ! i ! o 型p 0 三 ” p 型。p ，。”。业7 ”0 ，。 可f i 两矿一u 1 q - _ q b n ( a - ) n f n ( p ) 一= 0b p q 三p i o ， 苎竺呈! 垡兰竺生! ! ：! 塑业b p q 二一( z ) ( ) ( p i q ) p m 丛骘) ，q 川1 = 二卫”q ，：e 萑n t ( q ) 门 1 丽! 可可可西 p i 骂”p q 业7 ”q ，f n ( p ) ， 币j i 丽两而一啪 第二章进程代数简介：c c s ，”演算，对称n 演算与l b d a 一”演算 局部化规则 叠代规则 p 三p ，z 幻( n ) ，p ”1 磐p 7 z 协m ， t 万互i 万伽i 巫旷“ ! 三二! ! 兄 p p l ! p 1 3 在以上规则中，名，自由名及受限名的定义与”演算中是一致的。但是请注意到交换动作的分类，对 于交换进来没有区分，而交换出去的名是否是受限名是严格分别的，动作后的右括号是) 或) 即分别表 示交换出去的是自由名及受限名，如”型? ) 与”1 j 骘分别表示动作交换出去的是自由的x 与受限的x 。 另外，其中d - m i ( y z ) ，m i ( z ) lm ，z ，y 厂) 。 我们看顺序规则，与”演算顺序规则不同的是，这儿没有区分输入输出的不同，而是进程与外界交换一 个名。再看并行规则，没有区别，只是n 动作的取值范围中没有输入输出动作，而只有不区分输入输出 的交换名的动作。下面是通信规则，注意到与”演算的不同在于，它没有抽象名，进程交换出去的若是 受限名，则受限名的受限范围也扩展至将该受限名交换进来的进程范围中，任意一个通信r 动作均是发 生一次名的交换，而不是- 演算中的发生单方向的输入输出。关于局部化与叠代规则，实质上与”演算 是一致的。 下面再给出几个简单的应用以上规则的推导的例子以更加加深对规则的把握，可以也有助于理解其与标 准w 演算的不同之处。 第一个例子是t 两个全局名进行了交换 m l q 掣。叫。 i 面再画丽s 百i 面两巧瓦面丁p 1 ，n o mpj ( 冗j m l $ v ) _ + p 肺叫j f rj q z 】) 请注意例子中动作m o 与，n 1 只是分别表示发生交换通信的两个对应方，这两方在输入输出上是没有区 别的，与w 演算中的输入输出动作m 与芥i 有本质上的区别。 第二章进程代数简介：c c s ，。演算，s , f 8 一演算与l b d a 一”演算 1 4 第二个例子是：全局名与受限名进行了交换 ，n l 时q ”唑”q y a 1 。 r i 叭阱q ”蟛1 r i q v z 4 ， i 而亚万瓦百5 1 五而丽旷必”r i q ，