Bigraph反应系统中类型表述理论的研究进展

(郑州轻工业大学 计算机与通信工程学院， 河南 郑州 450001)

类型系统源于罗素为避免朴素集合论的悖论而引入的“分类”思想[1-2]. 在计算机科学中,类型系统及其相关研究涉及到理论计算机科学,特别是程序设计理论的各个方面, 如可计算理论、数理逻辑、抽象代数等. 形式语义学的各个流派,如操作语义学的结构操作语义,指称语义学的论域,公理语义学的程序逻辑,代数语义学的范畴论等都与类型系统有密切的关系[3].对于程序设计语言而言,诸如C#、Java、Ruby以及Haskell等现代商业程序设计语言，都将类型系统作为保证数据一致性和程序无误运行的强有力工具. 类型系统在安全及网络设计等其它领域也有了越来越多的应用.总之,计算机科学的类型理论的时代到来了[4].

在CCS(Calculus of Communicating Systems)[5-6]、Pi演算[7-10]等进程演算中,用类别给通道名进行分类,其主要目的在于确保进程能够合理地使用所接收的名字；类型则留给了进程,作为进程间关系推演的机制. 值得注意的是,在研究BRS的文献中,每个应用都需要对基础Bigraph范畴的扩展,而扩展的形式通常是分类或类型[11-12]. BRS主要利用赋类(sortings)或归纳类型(inductive type)的类型表述方式来限制、约束反应系统中的Bigraphs. 并且,在此类型表述下的范畴仍需具有RPO特性,以保证其衍生的标号迁移系统满足同余关系. Bigraph理论中的赋类以及归纳类型的研究，被认为是其理论本身以及应用于实践中的关键环节. 深入探讨BRS中赋类与归纳类型将有助于完善BRS的形式化语义模型,为移动分布式系统的建模、模型检验以及编程工具，奠定坚实的理论基础.

1 Bigraph反应系统概述

如何对移动分布式系统的规约、设计及程序编制提供理论支撑,如何为现有的移动和并发理论建立统一的元模型，是理论计算机研究领域所面临的双重挑战. Bigraph反应系统模型就是响应以上挑战而提出的以范畴论为数学基础的基于图形的形式化理论,它不仅具有图形化的表现形式、严格的数学基础,而且还具备灵活的语义定义方式和良好的可扩展能力.

参照文献[13],下面分别从Bigraph反应系统的静态结构以及动态系统对其进行介绍.

1.1 Bigraphs反应系统的静态结构

一个Bigraph由基于相同节点集合上的相互正交的位置图和连接图组成，其中,位置图用来模拟位置(locality),它是由节点(node)嵌套关系构造的森林. 而连接图则是模拟连通性(connectivity),它是一个节点间连接关系组成的超图. 图1中分别描画了Bigraph G及其位置图和连接图,并且,通过对图1中的元素来说明Bigraph中的相关概念.椭圆代表节点(v0,v1,v2),且每个节点被指派了控制用法标签K中的控制标识(K,M). 基本控制用法标签则是由一个控制标识集合κ及每个控制标识与其端口数量的映射ar:κ→ù构成. 当定义一个控制用法标签的时候,例如，图1写成κ={ar(K):2,ar(M):4}的形式,通常将控制用法标签只用κ来代替. 虚线的矩形框称作为区域(regions/roots)：它们是组成位置图森林的树根节点,通常由从0开始的连续自然数表示其身份,且从左到右依次递增. 一个Bigraph图中的区域的数量定义为它的宽度. 与区域相对应,灰色虚线矩形称为地点(sites/holes):它们模拟其它Bigraphs可以被插入的位置,也是由从0开始的连续自然数表示.在Bigraph理论中,将区域、节点及地点统称为位置.

外部名(outer name)用来模拟环境需要提供的连接点,一个Bigraph的外部名写在其上方,如图1中的(y0,y1,y2). 相反的,写在Bigraph下方的称为内部名(inner name),它用来刻画一个Bigraph作为环境时提供的连接点,如图1中的(x0,x1). 内部名、外部名及边(edges)统称为连接,每个链接可以连接称之为斑点的多个端口或内部名. 链接用来表述连通性.由区域宽度和外部名集Y组成的二元组n,Y称为Bigraph的外部界面,而内部界面则是由地点数量m和内部名X构成的二元组m,X.一个Bigraph是离散的当且仅当连接图的外部名和斑点之间存在一一映射关系. 将内部界面为空,也就是既没有内部名又无地点的Bigraph称为代理或基(agent/ground),通常将基H:ε→J记为H:J的形式. 如果一个Bigraph没有内部名且外部宽度为1,其坎集的表达形式为m→Y,则称满足此种形式为初始Bigraph. 如果Bigraph没有封闭的连接并且其连接映射是双射的,则该Bigraph称为是离散的.

图1 Bigraph及其子图(位置图、链接图)Fig.1 Bigraph and its subgraphs (location map, link map)

Bigraph间的一种基本的组合方式为复合∘, 复合的规则要求参与复合的两个Bigrahs的节点和边的标识符互不相交,并且满足范畴论中态射间复合的条件, 如图2所示的G和F以及复合后的G∘F.复合操作也称为垂直合成,直观上是将F的区域插入到G的地点中，并将F的外部名与G相应的内部名连接在一起. 还有一种基本的组合方式称为水平合成,即张量积⊗.该操作除了要求参与合成的Bigraph的节点和边互补相交外,每个Bigraph的内部名和外部名也必须互补相同,其示例见图3.

图2 Bigraphs复合操作图例Fig.2 Legends of Bigraphs composite operation

图3 Bigraphs张量积图例Fig.3 Legends of Bigraphs tensor product

1.2 Bigraphs反应系统的动态结构

与图重写的重写规则类似[14-16], Bigraphs反应系统通过反应规则表述其动态语义.一条反应规则包括了反应物和生成物两个部分,并可带有任意多个参数,其中反应物、生成物都是Bigraph,生成物和反应物的参数具有映射关系,这使得反应物中的参数可以被复制或丢弃. 反应规则可以根据具体的应用自由的加以定义.尽管反应系统与图重写有许多相似点,但仍存在不同，文献[17-18]详细讨论了两者的区别与联系.

一个具体基反应规则(r:J,r′:J)是不带参数的反应规则. 当a:I是包含r的等价类,也即aCor,那么由反应规则(r,r′)产生的反应为a→d就是将a中出现的r用r′来替换得到dCor′,C称为反应的环境,→称为反应关系. 反应被限定在控制状态为活跃的控制中,而一个环境是活跃的当且仅当环境中所有的地点在位置图内都有活跃的祖先.一个具体的Bigraph反应系统由一个控制用法标签以及一组基反应规则构成的集合组成.抽象Bigraph反应系统是通过具体Bigraph反应系统的基、规则及反应关系支撑物的等价类得到.参数化的规则,也就是,反应物和生成物中可能都有地点的存在.具体参数化反应规则的形式为(R:m→J,R′:m′→J,η:m′→m)：由反应物R、生成物R′以及从生成物至反应物地点间的实例化映射. 对于一个给定的生成物地点,实例化映射刻画了反应物中哪个参数插入该地点.对于任何具体离散的Bigraphd=d0⊗…⊗dm-1:m,Y,每个di都是初始Bigraph.据此可以得到由参数化规则生成所有的基规则(r,r′),其中rRd、r′R′(d0‖…‖dm′-1)以及d′jdη(j).

2 Bigraph理论中的赋类研究

在Bigraph理论的类型表述中,赋类的方式是通过丰富范畴中的对象略去不符合赋类规范的态射,继而构造出一个新的赋类范畴.范畴与通过忘却函子联系在一起：

F:→.

自Leifer等[20]给出了BRS中链接赋类的概念以来,研究者们利用赋类机制将BRS作为并行演算的元模型，对移动分布式系统的建模、模拟、编程语言工具等进行了深入的研究,其主要工作如下：

Milner[13]利用泛代数中多类化代数的思想,给出了位置赋类(place sorting)的定义，对每个节点可以嵌套的控制类进行了约束,将Bigraph基本形式中的BG(κ)扩展为BG(∑),其中：

∑=(θ,κ,Φ)

表示对每个控制指派一个类(sort)θ∈,控制标签κ被类化在之上,Φ作为形成规则是类化Bigraph的属性，且范畴的单位态射和对称性满足此属性,范畴的复合运算、张量积保持不变.BG(∑)中接口宽度n的形式表示将中的每个θi指派给i∈n.与文献[21]中的同态赋类(homomorphic sorting)相同,文献[13]定义了层次位置赋类,在函数φ:θ→的对应关系下,形成规则Φ规定：

◇ 区域r:θ的所有子节点类型指派为θ;

◇ 节点v:θ的所有子节点类型指派为φ(θ).

在此赋类的场景下,Milner给出了有限CCS的Bigraph表述的转换规则,讨论了该BRS衍生的标号迁移系统的互模拟关系. 同样地,利用链接图多对一赋类(many-one sorting)的方法,利用如下形成规则Φ：

◇ 每条链接至多有一个s点;

◇ 一个链接有类s当且仅当它有一个s点;

◇ 任何封闭链接的类都是s.

对条件事件(condition-event) Petri网进行了Bigraph描述. 这种多类化赋类机制除了描述能力的局限,存在对Bigraph代数系统中的衍生操作符不协调的现象.

文献[22]中给出的绑定赋类是将控制标签中的每个控制K的端口用h→k划分成绑定h和自由k两种类型. 绑定端口规定链接到节点N上一个绑定端口的所有内部名和端口在N之内,即所谓的辖域条件. 绑定端口的定义可以模拟像同步Pi演算中x(k):P的语言项,但对于绑定Bigraphf:2,{x}→1,φ与g:0,φ→2,{x}的复合操作f∘g却不能确定x的位置. 为了纠正指派单个位置的缺陷,文献[23-24]提出的局部(local)Bigraph将接口(m,X)中的名字x∈X指定了多个位置m′⊆m,但仍然不能很好地解决位置确定的问题.

Conchúir[25]在文献[22]的基础上,定义并研究了类别(kind) Bigraph. 区别于非空类集合Φ中的成员sort,类别kind是一个控制中所能包含的控制的集合,即对于系统控制标签κ有以下关系：

进而将控制标签{κ,ar,status}扩展为{κ,ar,actv,kind}的形式. 类别Bigraph本质上是一种位置赋类,在讨论了类别BRS的RPO等静态特性、动态变迁中的反应归纳一致性后, Conchúir还论述了类别kind与同态赋类 (homomorphic sorting) 之间的关系.在其早期的研究中[26-27], Conchúir还提出利用瓦片赋类(tile sorting)的思想，将链接图中的端点分成有方向性的和无方向性两种，并研究了简单类型化lambda演算的Bigraph模型.

Bundgaard等在文献[28]中利用子赋类(sub-sorting)的概念对类型化多元Pi演算[29-30]进行了Bigraph表述,其中的赋类机制除了模拟多元Pi演算类型中的类型之外，还被用来控制反应规则的应用.文献[31-36]中提出的有向(directed Bigraph)是将连接图f:X→Y扩展为f:(X-,X+)→(Y-,Y+)的形式,X+和Y-是斑点而X-和Y+是链接. 这种方向性的分类有助于处理定位和资源通讯,但它与基本Bigraph之间的关系需要进一步的研究. 针对Bigraph中位置图是一个树形结构而不能对位置进行共享的情况,文献[37-38]提出了带有共享的有向非循环图 (directed acyclic graph) 来模拟像无线网络中信号范围重叠的系统(图4),与赋类机制相关的问题也是值得研究的问题.

图4 共享Bigraph及其位置子图[37]Fig.4 Shared Bigraph and its position subgraph [37]

Debois等在文献[39-41]中对Bigraph反应系统的赋类机制进行了系统的分析研究.鉴于Bigraph理论中的赋类机制多数是为了限制原范畴态射这一实际情况,提出了一个赋类函子的概念,利用范畴论中的纤维化(fibration)对BRS的赋类进行分析表述. 在此基础上,提供了一个赋类类似于一个谓词P的充分条件,使范畴上的BRS相当于一个谓词P并且要求谓词P是可分解的,即：如果P(g∘f)成立,则P(g)与P(f)皆成立. 文献中还提出了一个更加先进有用的赋类——封闭赋类(图5),对于给定的范畴两个态射f:a→b和g:b→c,其类化范畴中b的前像b′要求既是f的前像f′的余域又是g的前像g′的域.文献第六章的综述对现有的赋类进行了归纳,讨论了各种赋类应用是否有相关谓词对应.在Debois近期的研究文献[42]中,对Bigraph反应系统中的演算BRS进行了赋类机制的研究,通过赋类结构来阐述Bigraph反应系统中演算的重要地位.在此研究的基础上,文献[43]利用声明式赋类机制，不仅可以保证所谓封闭赋类及其导出的标号互模拟同余关系的存在，而且,提出的声明式赋类Bigraph元演算无需任何的范畴论知识,又可以用Bigraph抽象机进行模拟、执行. 声明式赋类机制通过一种语法类似于XPath[44]的Bigraph逻辑,考虑了先前所有进程演算模型描述为封闭赋类化Bigraph反应系统的赋类、绑定约束的直观性声明.

图5 封闭赋类Fig.5 Seal sorting

除了作为现有进程演算的元模型,为普适计算提供一个抽象机也是Bigraphs理论的主要目的之一.普适计算是信息空间和物理空间的融合,在这个融合的空间中人们可以随时随地、透明地获得数字化的服务[45-48]. 情景感知是普适计算中重要的支撑技术，它研究如何有效地感知物理空间、信息空间乃至设备和人行为的变化,使得系统动态调整自身的行为，以便和周围的环境进行交互[49-52]. Birkedal等在文献[53-55]中讨论了Bigraph赋类在感知情景中的应用.

值得关注的是,在对普适计算环境中的上下文感知建模方面,Birkedal利用赋类的方法将模型分成三个部分：物理世界模型(C)、物理世界感知代理模型(P)及代理自身的模型(A),即所谓的环境感知的柏拉图模型. 尽管该模型给出了RPO和衍生标号迁移系统模拟关系的证明,但该模型既不能提供一个分类给κC∪κF，使得分类规范是同态的,并且又存在反例使得柏拉图模型不能满足判定分类是否安全的条件.

文献[56-57]利用Bigraph中的控制作为索引下标,每个控制的嵌套控制状态为其纤维(fibre)来构造一个控制嵌套的切片范畴SCat(K),其中：

◇ 范畴的态射：每个Xi中元素间的偏序关系以及由其构成的K中偏序关系为态射

◇ 范畴的组合及单位态射继承自控制集合K构成的范畴.

以此扩展Bigraph的控制标签得到位置赋类的位置图范畴,讨论其RPO的构建，论证了一致性条件下的同前相关推出. 该文献还讨论了以定型BRS中加入演算BRS的方式对情景感知系统进行建模,并且通过与文献[53]中的柏拉图模型之间的比较，展示其在感知系统建模方面的能力.

3 归纳类型系统在Bigraph理论中的应用

类型理论已经超越数据结构的范围，而进入更复杂的领域[4]. 类型系统不仅对于程序设计语言的形式语义,而且对于并行和分布式计算模型的研究都有非常重要的意义. 当前,对于BRS的类型系统研究主要是作为元模型来描述其它进程演算时进行的,除了可以将元模型的研究结果应用于其他具体的演算之外,在元模型的层面上讨论类型系统有助于更加深入的理解类型系统本身.Elsborg等[58]通过在Bigraph基本项(term)和操作上归纳地定义一个I/O类型系统,并将其应用到Bigraph表述的Pi演算上. 该项研究不仅阐述了BRS理论中归纳类型的描述机制,而且论证了类型系统中诸如类型保持定理及类型可靠性命题. Elsborg[19]在其随后的博士论文中进一步讨论了Bigraph中的归纳类型和赋类的关系,提出了归纳赋类的概念,把一个BRS上的归纳类型系统T看作是Bigraph项上的一个谓词,也就是说,

因为T是归纳定义的,则谓词P也一定是可分解的,即满足如下的关系：

国内学者对Bigraph理论的研究目前主要集中在软件体系结构的架构和验证方面,对Bigraph反应系统中的赋类或归纳类型的研究较少[59-63].

4 Bigraph理论类型表述研究存在的主要问题

作为移动分布式系统的基础理论, Bigraph反应系统较之Petri网[64-66]、Pi演算、移动灰箱[67-68]等并行模型或分布式模型理论有着明显的描述表达能力，但就模型相关的类型表述方面的研究，同成熟移动并发理论模型还有很大的差距. 根据国内外研究的情况, 笔者认为主要存在以下问题：

(1)对于一个赋类函子F:→,文献[6]中的语义对应定理只是保证了函子F与谓词P的对应关系.但是,定理没有保证对于满足谓词P的范畴中的变换轨迹在中前像也是一个轨迹.例如,是范畴中的变换轨迹,对应定理仅提供了没有保证

(2)赋类理论中的谓词P要求是可分解的,即P(g∘f)p(f)p(g). 然而,有时要求谓词P是可组合的：如果P(f)和P(g)成立,则P(g∘f)成立,从技术上讲,范畴中态射上的组合谓词确定了的一个子范畴. 组合谓词的确定在描述BRS中类型系统的子类型，以及在BRS应用到计算生物学建模时非常有用.

(3)当前,BRS元模型层面的类型系统仅是简单的归纳类型系统,对于BRS上复杂类型系统的类型指派，则需要进一步的深入研究. 并且, BRS上简单类型系统研究只是给出了Bigraph链接的归纳类型,而节点(node)的类型指派问题至今尚无相关的研究成果.

(4)归纳类系统与赋类分别从语法、语义层面对BRS中的Bigraph进行限制约束. 针对文献[13]中归纳类型与赋类之间的关系,即是否存在如下的对应关系：

P(f)当且仅当存在Δ,Γ使得Δ;Γfrep

也还是一个开放性问题.对该问题进行深入的研究,可以将两者的优势结合起来,使得对于BRS中的态射约束更加易于处理.

作为BRS中的类型表述方法,赋类与归纳类型系统各自具有不同的优势和不足. 如何通过BRS元模型上高级归纳类型系统的定义及其对相应Lambda演算、Pi演算的描述深入研究BRS的归纳类型，是未来Bigraph理论研究的一个主要方向.与此同时,通过深入研究赋类与归纳类型系统的关系，进而找出两者之间的相应联系，也是值得重点关注的内容.