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

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

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

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

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

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

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

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

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

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

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

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

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

2 Bigraph理論中的賦類(lèi)研究

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

F:→.

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

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

∑=(θ,κ,Φ)

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

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

◇ 節(jié)點(diǎn)v:θ的所有子節(jié)點(diǎn)類(lèi)型指派為φ(θ).

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

◇ 每條鏈接至多有一個(gè)s點(diǎn);

◇ 一個(gè)鏈接有類(lèi)s當(dāng)且僅當(dāng)它有一個(gè)s點(diǎn);

◇ 任何封閉鏈接的類(lèi)都是s.

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

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

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

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

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

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

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

圖5 封閉賦類(lèi)Fig.5 Seal sorting

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

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

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

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

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

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

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

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

因?yàn)門(mén)是歸納定義的,則謂詞P也一定是可分解的,即滿(mǎn)足如下的關(guān)系：

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

4 Bigraph理論類(lèi)型表述研究存在的主要問(wèn)題

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

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

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

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

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

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

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

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