Bigraph反應(yīng)系統(tǒng)中類型表述理論的研究進展

(鄭州輕工業(yè)大學 計算機與通信工程學院， 河南 鄭州 450001)

類型系統(tǒng)源于羅素為避免樸素集合論的悖論而引入的“分類”思想[1-2]. 在計算機科學中,類型系統(tǒng)及其相關(guān)研究涉及到理論計算機科學,特別是程序設(shè)計理論的各個方面, 如可計算理論、數(shù)理邏輯、抽象代數(shù)等. 形式語義學的各個流派,如操作語義學的結(jié)構(gòu)操作語義,指稱語義學的論域,公理語義學的程序邏輯,代數(shù)語義學的范疇論等都與類型系統(tǒng)有密切的關(guān)系[3].對于程序設(shè)計語言而言,諸如C#、Java、Ruby以及Haskell等現(xiàn)代商業(yè)程序設(shè)計語言，都將類型系統(tǒng)作為保證數(shù)據(jù)一致性和程序無誤運行的強有力工具. 類型系統(tǒng)在安全及網(wǎng)絡(luò)設(shè)計等其它領(lǐng)域也有了越來越多的應(yīng)用.總之,計算機科學的類型理論的時代到來了[4].

在CCS(Calculus of Communicating Systems)[5-6]、Pi演算[7-10]等進程演算中,用類別給通道名進行分類,其主要目的在于確保進程能夠合理地使用所接收的名字；類型則留給了進程,作為進程間關(guān)系推演的機制. 值得注意的是,在研究BRS的文獻中,每個應(yīng)用都需要對基礎(chǔ)Bigraph范疇的擴展,而擴展的形式通常是分類或類型[11-12]. BRS主要利用賦類(sortings)或歸納類型(inductive type)的類型表述方式來限制、約束反應(yīng)系統(tǒng)中的Bigraphs. 并且,在此類型表述下的范疇仍需具有RPO特性,以保證其衍生的標號遷移系統(tǒng)滿足同余關(guān)系. Bigraph理論中的賦類以及歸納類型的研究，被認為是其理論本身以及應(yīng)用于實踐中的關(guān)鍵環(huán)節(jié). 深入探討B(tài)RS中賦類與歸納類型將有助于完善BRS的形式化語義模型,為移動分布式系統(tǒng)的建模、模型檢驗以及編程工具，奠定堅實的理論基礎(chǔ).

1 Bigraph反應(yīng)系統(tǒng)概述

如何對移動分布式系統(tǒng)的規(guī)約、設(shè)計及程序編制提供理論支撐,如何為現(xiàn)有的移動和并發(fā)理論建立統(tǒng)一的元模型，是理論計算機研究領(lǐng)域所面臨的雙重挑戰(zhàn). Bigraph反應(yīng)系統(tǒng)模型就是響應(yīng)以上挑戰(zhàn)而提出的以范疇論為數(shù)學基礎(chǔ)的基于圖形的形式化理論,它不僅具有圖形化的表現(xiàn)形式、嚴格的數(shù)學基礎(chǔ),而且還具備靈活的語義定義方式和良好的可擴展能力.

參照文獻[13],下面分別從Bigraph反應(yīng)系統(tǒng)的靜態(tài)結(jié)構(gòu)以及動態(tài)系統(tǒng)對其進行介紹.

1.1 Bigraphs反應(yīng)系統(tǒng)的靜態(tài)結(jié)構(gòu)

一個Bigraph由基于相同節(jié)點集合上的相互正交的位置圖和連接圖組成，其中,位置圖用來模擬位置(locality),它是由節(jié)點(node)嵌套關(guān)系構(gòu)造的森林. 而連接圖則是模擬連通性(connectivity),它是一個節(jié)點間連接關(guān)系組成的超圖. 圖1中分別描畫了Bigraph G及其位置圖和連接圖,并且,通過對圖1中的元素來說明Bigraph中的相關(guān)概念.橢圓代表節(jié)點(v0,v1,v2),且每個節(jié)點被指派了控制用法標簽K中的控制標識(K,M). 基本控制用法標簽則是由一個控制標識集合κ及每個控制標識與其端口數(shù)量的映射ar:κ→ù構(gòu)成. 當定義一個控制用法標簽的時候,例如，圖1寫成κ={ar(K):2,ar(M):4}的形式,通常將控制用法標簽只用κ來代替. 虛線的矩形框稱作為區(qū)域(regions/roots)：它們是組成位置圖森林的樹根節(jié)點,通常由從0開始的連續(xù)自然數(shù)表示其身份,且從左到右依次遞增. 一個Bigraph圖中的區(qū)域的數(shù)量定義為它的寬度. 與區(qū)域相對應(yīng),灰色虛線矩形稱為地點(sites/holes):它們模擬其它Bigraphs可以被插入的位置,也是由從0開始的連續(xù)自然數(shù)表示.在Bigraph理論中,將區(qū)域、節(jié)點及地點統(tǒng)稱為位置.

外部名(outer name)用來模擬環(huán)境需要提供的連接點,一個Bigraph的外部名寫在其上方,如圖1中的(y0,y1,y2). 相反的,寫在Bigraph下方的稱為內(nèi)部名(inner name),它用來刻畫一個Bigraph作為環(huán)境時提供的連接點,如圖1中的(x0,x1). 內(nèi)部名、外部名及邊(edges)統(tǒng)稱為連接,每個鏈接可以連接稱之為斑點的多個端口或內(nèi)部名. 鏈接用來表述連通性.由區(qū)域?qū)挾群屯獠棵痀組成的二元組n,Y稱為Bigraph的外部界面,而內(nèi)部界面則是由地點數(shù)量m和內(nèi)部名X構(gòu)成的二元組m,X.一個Bigraph是離散的當且僅當連接圖的外部名和斑點之間存在一一映射關(guān)系. 將內(nèi)部界面為空,也就是既沒有內(nèi)部名又無地點的Bigraph稱為代理或基(agent/ground),通常將基H:ε→J記為H:J的形式. 如果一個Bigraph沒有內(nèi)部名且外部寬度為1,其坎集的表達形式為m→Y,則稱滿足此種形式為初始Bigraph. 如果Bigraph沒有封閉的連接并且其連接映射是雙射的,則該Bigraph稱為是離散的.

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

Bigraph間的一種基本的組合方式為復(fù)合°, 復(fù)合的規(guī)則要求參與復(fù)合的兩個Bigrahs的節(jié)點和邊的標識符互不相交,并且滿足范疇論中態(tài)射間復(fù)合的條件, 如圖2所示的G和F以及復(fù)合后的G°F.復(fù)合操作也稱為垂直合成,直觀上是將F的區(qū)域插入到G的地點中，并將F的外部名與G相應(yīng)的內(nèi)部名連接在一起. 還有一種基本的組合方式稱為水平合成,即張量積?.該操作除了要求參與合成的Bigraph的節(jié)點和邊互補相交外,每個Bigraph的內(nèi)部名和外部名也必須互補相同,其示例見圖3.

圖2 Bigraphs復(fù)合操作圖例Fig.2 Legends of Bigraphs composite operation

圖3 Bigraphs張量積圖例Fig.3 Legends of Bigraphs tensor product

1.2 Bigraphs反應(yīng)系統(tǒng)的動態(tài)結(jié)構(gòu)

與圖重寫的重寫規(guī)則類似[14-16], Bigraphs反應(yīng)系統(tǒng)通過反應(yīng)規(guī)則表述其動態(tài)語義.一條反應(yīng)規(guī)則包括了反應(yīng)物和生成物兩個部分,并可帶有任意多個參數(shù),其中反應(yīng)物、生成物都是Bigraph,生成物和反應(yīng)物的參數(shù)具有映射關(guān)系,這使得反應(yīng)物中的參數(shù)可以被復(fù)制或丟棄. 反應(yīng)規(guī)則可以根據(jù)具體的應(yīng)用自由的加以定義.盡管反應(yīng)系統(tǒng)與圖重寫有許多相似點,但仍存在不同，文獻[17-18]詳細討論了兩者的區(qū)別與聯(lián)系.

一個具體基反應(yīng)規(guī)則(r:J,r′:J)是不帶參數(shù)的反應(yīng)規(guī)則. 當a:I是包含r的等價類,也即aCor,那么由反應(yīng)規(guī)則(r,r′)產(chǎn)生的反應(yīng)為a→d就是將a中出現(xiàn)的r用r′來替換得到dCor′,C稱為反應(yīng)的環(huán)境,→稱為反應(yīng)關(guān)系. 反應(yīng)被限定在控制狀態(tài)為活躍的控制中,而一個環(huán)境是活躍的當且僅當環(huán)境中所有的地點在位置圖內(nèi)都有活躍的祖先.一個具體的Bigraph反應(yīng)系統(tǒng)由一個控制用法標簽以及一組基反應(yīng)規(guī)則構(gòu)成的集合組成.抽象Bigraph反應(yīng)系統(tǒng)是通過具體Bigraph反應(yīng)系統(tǒng)的基、規(guī)則及反應(yīng)關(guān)系支撐物的等價類得到.參數(shù)化的規(guī)則,也就是,反應(yīng)物和生成物中可能都有地點的存在.具體參數(shù)化反應(yīng)規(guī)則的形式為(R:m→J,R′:m′→J,η:m′→m)：由反應(yīng)物R、生成物R′以及從生成物至反應(yīng)物地點間的實例化映射. 對于一個給定的生成物地點,實例化映射刻畫了反應(yīng)物中哪個參數(shù)插入該地點.對于任何具體離散的Bigraphd=d0?…?dm-1:m,Y,每個di都是初始Bigraph.據(jù)此可以得到由參數(shù)化規(guī)則生成所有的基規(guī)則(r,r′),其中rRd、r′R′(d0‖…‖dm′-1)以及d′jdη(j).

2 Bigraph理論中的賦類研究

在Bigraph理論的類型表述中,賦類的方式是通過豐富范疇中的對象略去不符合賦類規(guī)范的態(tài)射,繼而構(gòu)造出一個新的賦類范疇.范疇與通過忘卻函子聯(lián)系在一起：

F:→.

自Leifer等[20]給出了BRS中鏈接賦類的概念以來,研究者們利用賦類機制將BRS作為并行演算的元模型，對移動分布式系統(tǒng)的建模、模擬、編程語言工具等進行了深入的研究,其主要工作如下：

Milner[13]利用泛代數(shù)中多類化代數(shù)的思想,給出了位置賦類(place sorting)的定義，對每個節(jié)點可以嵌套的控制類進行了約束,將Bigraph基本形式中的BG(κ)擴展為BG(∑),其中：

∑=(θ,κ,Φ)

表示對每個控制指派一個類(sort)θ∈,控制標簽κ被類化在之上,Φ作為形成規(guī)則是類化Bigraph的屬性，且范疇的單位態(tài)射和對稱性滿足此屬性,范疇的復(fù)合運算、張量積保持不變.BG(∑)中接口寬度n的形式表示將中的每個θi指派給i∈n.與文獻[21]中的同態(tài)賦類(homomorphic sorting)相同,文獻[13]定義了層次位置賦類,在函數(shù)φ:θ→的對應(yīng)關(guān)系下,形成規(guī)則Φ規(guī)定：

◇ 區(qū)域r:θ的所有子節(jié)點類型指派為θ;

◇ 節(jié)點v:θ的所有子節(jié)點類型指派為φ(θ).

在此賦類的場景下,Milner給出了有限CCS的Bigraph表述的轉(zhuǎn)換規(guī)則,討論了該BRS衍生的標號遷移系統(tǒng)的互模擬關(guān)系. 同樣地,利用鏈接圖多對一賦類(many-one sorting)的方法,利用如下形成規(guī)則Φ：

◇ 每條鏈接至多有一個s點;

◇ 一個鏈接有類s當且僅當它有一個s點;

◇ 任何封閉鏈接的類都是s.

對條件事件(condition-event) Petri網(wǎng)進行了Bigraph描述. 這種多類化賦類機制除了描述能力的局限,存在對Bigraph代數(shù)系統(tǒng)中的衍生操作符不協(xié)調(diào)的現(xiàn)象.

文獻[22]中給出的綁定賦類是將控制標簽中的每個控制K的端口用h→k劃分成綁定h和自由k兩種類型. 綁定端口規(guī)定鏈接到節(jié)點N上一個綁定端口的所有內(nèi)部名和端口在N之內(nèi),即所謂的轄域條件. 綁定端口的定義可以模擬像同步Pi演算中x(k):P的語言項,但對于綁定Bigraphf:2,{x}→1,φ與g:0,φ→2,{x}的復(fù)合操作f°g卻不能確定x的位置. 為了糾正指派單個位置的缺陷,文獻[23-24]提出的局部(local)Bigraph將接口(m,X)中的名字x∈X指定了多個位置m′?m,但仍然不能很好地解決位置確定的問題.

Conchúir[25]在文獻[22]的基礎(chǔ)上,定義并研究了類別(kind) Bigraph. 區(qū)別于非空類集合Φ中的成員sort,類別kind是一個控制中所能包含的控制的集合,即對于系統(tǒng)控制標簽κ有以下關(guān)系：

進而將控制標簽{κ,ar,status}擴展為{κ,ar,actv,kind}的形式. 類別Bigraph本質(zhì)上是一種位置賦類,在討論了類別BRS的RPO等靜態(tài)特性、動態(tài)變遷中的反應(yīng)歸納一致性后, Conchúir還論述了類別kind與同態(tài)賦類 (homomorphic sorting) 之間的關(guān)系.在其早期的研究中[26-27], Conchúir還提出利用瓦片賦類(tile sorting)的思想，將鏈接圖中的端點分成有方向性的和無方向性兩種，并研究了簡單類型化lambda演算的Bigraph模型.

Bundgaard等在文獻[28]中利用子賦類(sub-sorting)的概念對類型化多元Pi演算[29-30]進行了Bigraph表述,其中的賦類機制除了模擬多元Pi演算類型中的類型之外，還被用來控制反應(yīng)規(guī)則的應(yīng)用.文獻[31-36]中提出的有向(directed Bigraph)是將連接圖f:X→Y擴展為f:(X-,X+)→(Y-,Y+)的形式,X+和Y-是斑點而X-和Y+是鏈接. 這種方向性的分類有助于處理定位和資源通訊,但它與基本Bigraph之間的關(guān)系需要進一步的研究. 針對Bigraph中位置圖是一個樹形結(jié)構(gòu)而不能對位置進行共享的情況,文獻[37-38]提出了帶有共享的有向非循環(huán)圖 (directed acyclic graph) 來模擬像無線網(wǎng)絡(luò)中信號范圍重疊的系統(tǒng)(圖4),與賦類機制相關(guān)的問題也是值得研究的問題.

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

Debois等在文獻[39-41]中對Bigraph反應(yīng)系統(tǒng)的賦類機制進行了系統(tǒng)的分析研究.鑒于Bigraph理論中的賦類機制多數(shù)是為了限制原范疇態(tài)射這一實際情況,提出了一個賦類函子的概念,利用范疇論中的纖維化(fibration)對BRS的賦類進行分析表述. 在此基礎(chǔ)上,提供了一個賦類類似于一個謂詞P的充分條件,使范疇上的BRS相當于一個謂詞P并且要求謂詞P是可分解的,即：如果P(g°f)成立,則P(g)與P(f)皆成立. 文獻中還提出了一個更加先進有用的賦類——封閉賦類(圖5),對于給定的范疇兩個態(tài)射f:a→b和g:b→c,其類化范疇中b的前像b′要求既是f的前像f′的余域又是g的前像g′的域.文獻第六章的綜述對現(xiàn)有的賦類進行了歸納,討論了各種賦類應(yīng)用是否有相關(guān)謂詞對應(yīng).在Debois近期的研究文獻[42]中,對Bigraph反應(yīng)系統(tǒng)中的演算BRS進行了賦類機制的研究,通過賦類結(jié)構(gòu)來闡述Bigraph反應(yīng)系統(tǒng)中演算的重要地位.在此研究的基礎(chǔ)上,文獻[43]利用聲明式賦類機制，不僅可以保證所謂封閉賦類及其導(dǎo)出的標號互模擬同余關(guān)系的存在，而且,提出的聲明式賦類Bigraph元演算無需任何的范疇論知識,又可以用Bigraph抽象機進行模擬、執(zhí)行. 聲明式賦類機制通過一種語法類似于XPath[44]的Bigraph邏輯,考慮了先前所有進程演算模型描述為封閉賦類化Bigraph反應(yīng)系統(tǒng)的賦類、綁定約束的直觀性聲明.

圖5 封閉賦類Fig.5 Seal sorting

除了作為現(xiàn)有進程演算的元模型,為普適計算提供一個抽象機也是Bigraphs理論的主要目的之一.普適計算是信息空間和物理空間的融合,在這個融合的空間中人們可以隨時隨地、透明地獲得數(shù)字化的服務(wù)[45-48]. 情景感知是普適計算中重要的支撐技術(shù)，它研究如何有效地感知物理空間、信息空間乃至設(shè)備和人行為的變化,使得系統(tǒng)動態(tài)調(diào)整自身的行為，以便和周圍的環(huán)境進行交互[49-52]. Birkedal等在文獻[53-55]中討論了Bigraph賦類在感知情景中的應(yīng)用.

值得關(guān)注的是,在對普適計算環(huán)境中的上下文感知建模方面,Birkedal利用賦類的方法將模型分成三個部分：物理世界模型(C)、物理世界感知代理模型(P)及代理自身的模型(A),即所謂的環(huán)境感知的柏拉圖模型. 盡管該模型給出了RPO和衍生標號遷移系統(tǒng)模擬關(guān)系的證明,但該模型既不能提供一個分類給κC∪κF，使得分類規(guī)范是同態(tài)的,并且又存在反例使得柏拉圖模型不能滿足判定分類是否安全的條件.

文獻[56-57]利用Bigraph中的控制作為索引下標,每個控制的嵌套控制狀態(tài)為其纖維(fibre)來構(gòu)造一個控制嵌套的切片范疇SCat(K),其中：

◇ 范疇的態(tài)射：每個Xi中元素間的偏序關(guān)系以及由其構(gòu)成的K中偏序關(guān)系為態(tài)射

◇ 范疇的組合及單位態(tài)射繼承自控制集合K構(gòu)成的范疇.

以此擴展Bigraph的控制標簽得到位置賦類的位置圖范疇,討論其RPO的構(gòu)建，論證了一致性條件下的同前相關(guān)推出. 該文獻還討論了以定型BRS中加入演算BRS的方式對情景感知系統(tǒng)進行建模,并且通過與文獻[53]中的柏拉圖模型之間的比較，展示其在感知系統(tǒng)建模方面的能力.

3 歸納類型系統(tǒng)在Bigraph理論中的應(yīng)用

類型理論已經(jīng)超越數(shù)據(jù)結(jié)構(gòu)的范圍，而進入更復(fù)雜的領(lǐng)域[4]. 類型系統(tǒng)不僅對于程序設(shè)計語言的形式語義,而且對于并行和分布式計算模型的研究都有非常重要的意義. 當前,對于BRS的類型系統(tǒng)研究主要是作為元模型來描述其它進程演算時進行的,除了可以將元模型的研究結(jié)果應(yīng)用于其他具體的演算之外,在元模型的層面上討論類型系統(tǒng)有助于更加深入的理解類型系統(tǒng)本身.Elsborg等[58]通過在Bigraph基本項(term)和操作上歸納地定義一個I/O類型系統(tǒng),并將其應(yīng)用到Bigraph表述的Pi演算上. 該項研究不僅闡述了BRS理論中歸納類型的描述機制,而且論證了類型系統(tǒng)中諸如類型保持定理及類型可靠性命題. Elsborg[19]在其隨后的博士論文中進一步討論了Bigraph中的歸納類型和賦類的關(guān)系,提出了歸納賦類的概念,把一個BRS上的歸納類型系統(tǒng)T看作是Bigraph項上的一個謂詞,也就是說,

因為T是歸納定義的,則謂詞P也一定是可分解的,即滿足如下的關(guān)系：

國內(nèi)學者對Bigraph理論的研究目前主要集中在軟件體系結(jié)構(gòu)的架構(gòu)和驗證方面,對Bigraph反應(yīng)系統(tǒng)中的賦類或歸納類型的研究較少[59-63].

4 Bigraph理論類型表述研究存在的主要問題

作為移動分布式系統(tǒng)的基礎(chǔ)理論, Bigraph反應(yīng)系統(tǒng)較之Petri網(wǎng)[64-66]、Pi演算、移動灰箱[67-68]等并行模型或分布式模型理論有著明顯的描述表達能力，但就模型相關(guān)的類型表述方面的研究，同成熟移動并發(fā)理論模型還有很大的差距. 根據(jù)國內(nèi)外研究的情況, 筆者認為主要存在以下問題：

(1)對于一個賦類函子F:→,文獻[6]中的語義對應(yīng)定理只是保證了函子F與謂詞P的對應(yīng)關(guān)系.但是,定理沒有保證對于滿足謂詞P的范疇中的變換軌跡在中前像也是一個軌跡.例如,是范疇中的變換軌跡,對應(yīng)定理僅提供了沒有保證

(2)賦類理論中的謂詞P要求是可分解的,即P(g°f)p(f)p(g). 然而,有時要求謂詞P是可組合的：如果P(f)和P(g)成立,則P(g°f)成立,從技術(shù)上講,范疇中態(tài)射上的組合謂詞確定了的一個子范疇. 組合謂詞的確定在描述BRS中類型系統(tǒng)的子類型，以及在BRS應(yīng)用到計算生物學建模時非常有用.

(3)當前,BRS元模型層面的類型系統(tǒng)僅是簡單的歸納類型系統(tǒng),對于BRS上復(fù)雜類型系統(tǒng)的類型指派，則需要進一步的深入研究. 并且, BRS上簡單類型系統(tǒng)研究只是給出了Bigraph鏈接的歸納類型,而節(jié)點(node)的類型指派問題至今尚無相關(guān)的研究成果.

(4)歸納類系統(tǒng)與賦類分別從語法、語義層面對BRS中的Bigraph進行限制約束. 針對文獻[13]中歸納類型與賦類之間的關(guān)系,即是否存在如下的對應(yīng)關(guān)系：

P(f)當且僅當存在Δ,Γ使得Δ;Γfrep

也還是一個開放性問題.對該問題進行深入的研究,可以將兩者的優(yōu)勢結(jié)合起來,使得對于BRS中的態(tài)射約束更加易于處理.

作為BRS中的類型表述方法,賦類與歸納類型系統(tǒng)各自具有不同的優(yōu)勢和不足. 如何通過BRS元模型上高級歸納類型系統(tǒng)的定義及其對相應(yīng)Lambda演算、Pi演算的描述深入研究BRS的歸納類型，是未來Bigraph理論研究的一個主要方向.與此同時,通過深入研究賦類與歸納類型系統(tǒng)的關(guān)系，進而找出兩者之間的相應(yīng)聯(lián)系，也是值得重點關(guān)注的內(nèi)容.