多态类型系统下的等价关系

多态类型系统下的等价关系

1多态类型系统的应用并行计算模型是计算机科学的研究领域之一。并发计算模型是对并发计算的形式刻画,传统的并发计算模型有Hoare的CSP、Milner的CCS等。由Milner、Parrow、Walker等人提出的π演算是对传统的并发计算模型CCS的扩展,增加了对移动的形式刻画,已经成为移动进程演算的典范。目前对π演算的研究主要在于代数理论和类型系统两个方面。代数理论在无类型的π演算中已经进行了非常充分的研究,主要成果包括各种行为等价关系的公理化系统,如迟、早互模拟,迟、早同余,开互模拟,测试等价等。对类型系统的研究如文献,它们分别考察了类型系统对行为等价关系、代数理论的影响,以及多态类型系统对行为等价关系的影响。在本文中,我们考察了多态类型系统对π演算代数理论的影响。类型系统在分布式系统理论中有着非常重要的作用,本质上它是一种静态分析工具,有利于保证程序的正确性。然而,一般的类型系统限制了程序设计的灵活性,并且往往不能保证完备性。多态类型系统允许某个操作可以作用到不同类型的参数上,从一定程度上克服了这样的问题。多态类型有三种方式,分别为Ad-Hoc多态、Subtyping多态和参数多态(ParametricPolymorphism)。本文主要讨论第三种多态。在对π演算增加类型系统后,人们需要考察π演算的一些新的特性,其中最重要的就是考察进程等价关系的变化。Pierece和Sangiorgi在文献中通过区分通道的读写能力首先提出了通道的能力类型(CapabilityTypes),并据此给出了类型接口同余的定义。在赋予通道能力类型后,进程的等价关系发生了变化,主要原因在于通道的通信能力受到了限制。例如,进程:Ρdef=(νc)ˉbc.a(y).(ˉy|c)Qdef=(νc)ˉbc.a(y).(ˉy.c+c.ˉy)在无类型的π演算中它们是不等价的。然而,如果我们限制通道b通信的内容只具有输入能力,也即c只能用于输入而不能用于输出,此时P和Q是行为等价的,这是由于c不能经过通道a发送到进程P和Q(ˉy的出现使得c不能实例化y)。事实上,在引入类型系统后,环境区分进程的能力受到了限制,区分能力减弱,从而使得原本不等价的进程在新的环境下又变得等价。而引入多态类型系统后,由于环境无法得知进程中通道的具体类型,只知抽象类型,此时环境的区分能力进一步削弱。文献中首次对多态π演算中进程的行为等价关系进行了研究,给出了多态类型接口等价的标号互模拟描述,但其中的标号互模拟描述并不是完备的。文献中给出了一个完备的标号互模拟描述,本文即给出了文献中标号互模拟的完备的公理系统。需要注意的是,本文讨论的是异步多态π演算,这是因为异步更接近于现实中的分布式系统,也比同步更容易实现。文献中给出了异步π演算中进程互模拟的公理系统,但他没有考虑类型系统。在类型系统的影响下,情况变得更为复杂。2多态慢流模型在本部分,我们将给出多态异步π演算的语法与操作语义以及类型系统。2.1导致开项互模拟记C是通道的无穷可数集合,V是变量的无穷可数集合,一般地,C={a,b,…},V={x,y,…}。通道、变量都为名,记N是名的无穷可数集合,N={u,v,…}。以P、Q表示进程,异步多态π演算的语法如下所示:Ρ,Q::=ˉu〈Τ;v〉|Ρ|Q|(νa:Τ)Ρ|GG::=0|u(X;x:Τ).Ρ|τ.Ρ|G+G其中,T、U、V、W表示类型,X、Y表示类型变量。注意这里没有复制操作,这是因为公理化时只能针对有穷进程进行。这里区分了通道与变量,所以在输入进程中的输入只能是变量,限制操作的对象只能是通道。我们分别用fn(P)、fv(P)、ftv(P)表示进程P中的自由通道、自由变量、自由类型变量。如果fv(P)≠∅,则称进程P为开项,否则称其为闭项。本文中公理化只针对闭项进行,这是因为在多态环境下开项互模拟的情况非常复杂,其能否公理化还不知道,这将是我们进一步的工作。替换σ为V→C的函数,替换作用的对象为进程中的自由变量,它使得一个开项在其作用下变为一个闭项。替换具有最高的运算优先级。2.2进程等价定义图1中我们使用标号转移系统给出了无类型π演算的操作语义。其中,我们总认为α换名的两个进程具有相同的行为,即Ρ′α→Ρ″,Ρ与Ρ″为α换名Ρα→Ρ″。我们不能直接使用这个操作语义给出进程行为等价的定义,这是因为在多态类型环境下进程等价需要考虑类型的影响,我们也需要考虑类型环境下进程的标号转移系统。在SUM、PAR和COM规则中省略了对称情况。2.3类型环境的生成图2中给出的类型系统是相当简单的,因为它不包含子类型、递归类型等,然而增加这些特性并不会影响本文的结果。其中,X、Y、Z表示类型变量,T、U等表示类型,当类型T形如085971[X;T]时,称T为生成的(Generative)。Γ、Δ表示类型环境,dom(Γ)表示类型环境的域,如dom(X;n:T)={X,n}。fv(Γ)、ftv(Γ)分别表示类型环境Γ的自由变量和自由类型变量,如fv(X;x:T)={x},ftv(X;n:T)={X}∪ftv(T)。若fv(Δ)=ftv(Δ)=∅,则我们称类型环境Δ是闭合的;同时,若a:T∈Δ且a:U∈Δ,则T=U。我们以Γ[σ]表示对类型环境的变量替换。这个类型系统与文献的不同之处在于它允许类型环境中存在一个名或变量有多个类型的现象。例如:X,Y;a:085971[085971[X],085971[Y]]b:085971[X],b:085971[Y]ˉa〈b,b〉而文献中不允许出现这样的现象,他们使用类型合一(TypeUnification)的设施来达到同样的目的。例如,上面这个例子中类型X和Y将被合一,这样b只有一个类型,即b:085971[X]。3生成多态类型互模拟使用无类型标号转移系统不能给出多态类型环境下进程的互模拟等价关系,为此我们需要一个综合类型环境和进程的标号转移系统。首先给出格局的定义。定义1(格局)格局具有这样的形式Γ[σ]Ρ,由三个部分组成,其中P是被观察的进程,Γ是P所在的类型环境的外部视图,σ是一个类型替换。Γ可能并不具有关于类型的完整信息,当进程P输出一个通道时,Γ只知其抽象类型,而不知其具体类型。σ把外部视图映射成内部视图,提供了P输出的类型的完整信息。图3中我们给出基于格局的标号转移系统,它有三种转换:(1)τ转换。此时进程没有输入输出,Γ、σ均未发生变化。(2)(ν→a:→Τ)c[→U;→b]转换。此时环境向进程发送数据,允许环境新建名并发送给进程,新建名记录在类型环境中。因为考虑的是异步演算,所以输入转换在一定条件下总是可以的。而进程没有发送消息到环境,因此σ不会发生变化。(3)(ν→a:→Τ)ˉc〈→X;→b:→V〉转换。此时进程向环境发送数据,环境中用来通信的进程必须具有类型085971[→X;→V],因此类型环境被扩展包含→X及→b:→V,这可能会导致环境中同一个名有多种类型的情况。同时σ也被扩展。例1设类型环境Γ::=a:085971[X,Y;085971[X],085971[Y],085971[Y],X],考虑进程:L=ν(b:085971[Τ],c:085971[Τ],d:Τ)(ˉa〈Τ,Τ;b,b,c,d〉|c(y:Τ).0)有:(ΓL)v(b,c,d)ˉa〈X,Y;b:085971[X],b:085971[Y],c:085971[Y],d:Y〉→(Γ′[σ]c(y:085971[Τ]).0)其中,Γ′为X,Y,Γ,b:085971[X],b:085971[Y],c:085971[Y],d:X,此时我们有以下转换:(Γ′[σ]c(y:085971[Τ]).0)b[d]→(Γ′[σ]c(y:085971[Τ]).0|ˉb〈d〉)ˉb〈d〉→(Γ′,d:Y[σ]c(y:085971[Τ]).0)c[d]→(Γ′d:Y[σ]c(y:085971[Τ]).0|ˉc〈d〉)τ→但我们不能直接有c[d]转换。下面根据上述标号转移系统给出基于格局的多态类型互模拟的形式化定义。基于闭合configuration的类型关系R是5元组(Γ,σ,P,ρ,Q)的集合,其中ΓσP、ΓρQ以及Γσ、Γρ均为闭合的。为简单起见,我们记(Γ,σ,P,ρ,Q)∈R为Γ[σ]PR[ρ]Q。定义2(互模拟关系)基于闭合格局的类型关系R被称为互模拟等价,如果Γ[σ]PR[ρ]Q,蕴含若(Γ[σ]Ρ)α→(Γ′[σ′]P′),则存在Γ′、ρ′、Q′使得(Γ[ρ]Q)α→(Γ′[ρ′]Q′)且Γ′[σ′]P′R[ρ′]Q′。记关系R为～。这个互模拟关系就是文献中针对多态类型接口等价完备的标号互模拟关系。下面我们将给出这个互模拟关系的一个公理系统。4公理化在本部分,我们将针对有穷进程给出多态类型互模拟的一个公理系统,这个系统的一致性和完备性将被证明。4.1[][]图4中给出了本文互模拟的公理系统。这个系统与文献的不同之处在于类型系统的加入。在有类型系统的情况下,我们用P=σ,ρΓQ表示进程P、Q在类型环境Γ下的等价关系,此时意味着Γ[σ]P、Γ[ρ]Q且Γ[σ]、Γ[ρ]、P、Q均是闭合的。若左右两个类型替换σ、ρ相同,我们就简单地用P=ΓQ表示。定义3Γc:085971[X;T],称Γ能推出ˉc〈U;b〉,若下述三种情况之一成立:(1)b∈dom(Γ),使得Γˉc〈U;b〉;(2)b∈dom(Γ),Γ/〈U;b〉,然而存在d∈dom(Γ),使得Γˉd〈V;b〉且Γd:085971[X;T];(3)类型T是生成的,b∉dom(Γ),则Γ,b:T{U/X}ˉc〈U;b〉。这个概念的提出是由于本文的类型环境允许存在一个名有多种类型的现象,关键是在情况(2),例1很好地解释了这种现象。4.2有穷进程p的转化本部分我们主要的工作就是证明此公理系统的完备性。证明方法借鉴了文献中的方法,但是由于类型的影响以及公理系统的差别,证明过程有很大的不同。首先先引入一个范式的概念,由于是异步π演算,这个范式和同步π演算中的范式是不一样的,然后证明任意一个进程均可以转化为对应的范式,最后我们对进程的结构和深度进行归纳证明得到结论。先给出一个辅助定义。定义4令Ρ≡(νc→:Τ→)∏i∈Ιa¯i〈Τi,bi〉,ΓσP,定义Fire(P)=∪n∈ωFiren(P),其中Firen(P)为P恰好运行n步后可被立即执行的动作索引,定义如下:Fire0(Ρ)={i|ai∉{c→}且Γ(ai)是生成的};Firen+1(P)={i|∃k∈Firen(P),bk=ai,Γ(ai)是生成的}/∪m≤nFirem(P)。下面我们给出范式的定义。定义5范式即为具有如下形式的进程项:(νc→:Τ→)(∏i∈Ιa¯i〈Τi,bi〉|(∑j∈Jτ.Ρj+∑k∈Κak(Xk;x:Τk).Ρk))其中,集合I、J、K互不相交,每个Pj、Pk均为范式,且满足下列条件:(1)∀c∈{c→},∃i∈Ι,bi=c;(2)Fire((νc→:Τ→)∏i∈Ιa¯i〈Τi;bi〉)=I;(3)∀k,j,若Γ能推出a¯k〈Uk;bk〉,且对任意的类型替换σ、ρ,都有:Ρk{Ukσ/Xk;bk/x}≠Γσ,ρ(a¯k〈Ukρ;bk〉|Ρj)为简单起见,我们把上述第三条简单地写为Ρk≠Γ(a¯k〈Uk;bk〉|Ρj)。下面我们将证明每个进程P均可使用公理系统A中的公式将其归约为一个范式。我们将对进程P的深度和结构归纳证明这个结论。首先给出P的深度的定义。定义6有穷进程P的深度表示为d(P),归纳定义如下:d(0)=0;d(a¯〈T;b〉)=1;d(a(X;x:T).P)=d(τ.P)=1+d(P);d(P|Q)=d(P)+d(Q);d((νa:T)P)=d(P);d(G+F)=max{d(G);d(F)}。下面的引理证明了任意一个有穷进程均可转化为其对应的范式。引理1对任意有穷进程P,存在一个范式:Ρ≡(νc→:Τ→)(∏i∈Ιa¯i〈Τi,bi〉|(∑j∈Jτ.Ρj+∑k∈Κak(Xk;x:Τk).Ρk))使得P=ΓP且d(P)≤d(P)。证明详细证明参见文献。在公理系统完备性的证明中,下列引理有着非常关键的作用。引理2设P、Q为两个范式:Ρ≡(νm→:Τ→)(∏i∈Ιa¯i〈Τi;bi〉|Ρ∑),Q≡(νn→:U→)(∏h∈Ηc¯h〈Uh;dh〉|Q∑),其中P∑≡∑j∈Jτ.Pj+∑k∈Kak(Xk;x:Tk).Pk,Q∑≡∑l∈Lτ.Ql+∑m∈Mcm(Ym;y:Um).Qm。若Γ[σ]P～[ρ]Q,|Ι|=Ν,且∀i∈I,Γai(Xi;x:Vi)及∀h∈H,Γch(Yh;y:Wh),如设Γi=Γ,b1:V1,…,bi:Vi,θi=T1/X1,…,Ti/Xi,σi=σ,θi,ρi=ρ,θi。其中i=1,…,N,那么存在名的单射