薛崗 張云春 劉笛 姚紹文



摘要:針對系統多層嵌套式結構范疇模型的動態行為描述與分析問題,提出一種基于端口自動機的行為表達方法(PAM)。該方法基于系統狀態、輸入和輸出端口來定義對象和結構上的運算。通過證明發現:PAM在運算上具有結構保持特征,是一個函子。基于PAM,還就并行、串行和反饋等行為組合,以及應用等相關問題進行了討論和分析,相關結論表明PAM可被應用于描述或分析具有嵌套式結構的系統動態行為。
關鍵詞:
系統行為表達方法;嵌套式系統結構;端口自動機;范疇論
中圖分類號: TP301.2 文獻標志碼:A
0引言
模塊間相互嵌套的結構是信息系統中最常見的結構之一。在應用系統中,為了實現復雜的功能,具有一定功能的模塊可嵌入并組合到其他模塊中;同樣,組合后的模塊還可被嵌入到更大的外部模塊中。近期,美國麻省理工學院Spivak等[1-3]使用“對稱多范疇”(symmetric multicategory)來討論自相似對象的嵌套結構以及相關計算特征。該系列研究的核心思想是:范疇對象間存在“多對一”態射,當使用集合概念替代范疇對象時,可實現表示內部結構的多個集合與一個表示外部結構的集合之間的嵌套組合關系;而且使用“函子”(functor)可基于結構特征分析出結構上的計算特征。2015年,該方法還被應用于“模塊化網絡”的靜態結構描述與動態特性表達上[4]。在該系列研究基礎上,本文基于“端口自動機”建立面向嵌套式結構的行為表達方法PAM,并就該方法相關理論基礎和應用方法等內容進行分析和討論。區別于文獻[4]所闡述方法,本文所提出的PAM方法是一個伴隨域為Sets(對象為集合的對稱多范疇)的函子,本文所提出的PAM方法是一個函子,該函子的伴隨域為:在狀態集上進行運算的動態系統,這也說明PAM運算具有結構保持特征,可將結構與集合上的運算相互聯系起來。
1相關技術基礎
“范疇”概念來源于范疇論(Category Theory)[5-6]。自20世紀80年代開始,范疇論被廣泛應用于開發邏輯系統、構建編程語言的數學語義[7]、分析自動機[8]和并發模型[9]等計算機科學領域。在國內,早在1989年,文獻[10]就范疇論應用于計算機科學的相關問題進行了討論。另外,文獻[11]利用范疇定義構件之間的關系;文獻[12]基于范疇定義構件行為組合,并將該方法應用于實現復雜的業務功能等。
范疇在定義上包含4個基本組成[5-6]:對象集、態射集、恒等態射和組合;范疇運算必須滿足兩個規則:恒等律和結合律。其中,對象是范疇的組成單元,對象由元素構成;態射(morphism,用箭頭表示)是對象間的對應關系;恒等態射(identity morphism, id)是對象與其自身的對應關系;組合(composition,運算符為“”)支持將多個態射連接形成新態射。另外,范疇論使用函子來揭示兩個范疇之間的對應關系,其定義涉及到兩個部分:對象和態射,函子所涉及運算必須滿足兩個規則:恒等保持和組合保持[5-6]。
范疇可被實例化,例如集合范疇Set就是一個實例化范疇。Set中的對象為集合,態射為集合上的函數[1]。當Set中的對象被限定為有限集合時,所形成的范疇為有限集合范疇,使用Fin表示;Fin是Set的全子范疇[1]。
1.1對稱多范疇
定義1對稱多范疇[1]。設對稱多范疇為M,其定義包含4個基本組成:a)對象,b)態射,c)恒等態射,d)態射組合。范疇中的運算必須滿足兩個規則:a)結合率,b)恒等率。
1)4個基本組成。
a)對稱多范疇中的對象集合為Ob(M)。集合中的元素是范疇中的對象。
b)態射集合使用Mn(xx-;y)表示,其中:y∈Ob(M),n∈Ob(Fin)是一個有限集合,x:n → Ob(M)是n索引對象集合。Mn(x;y)中的元素為態射。當態射φ∈Mn(x;y),則φ:x → y或φ:(x1,x2,…,xn) → y,其中:xi被稱為域對象,y被稱為伴隨域對象。
c)若x∈Ob(M),恒等態射idx∈M1(x;x)。
d)若s:m → n是Fin中的態射,對象z∈Ob(M),有限集合m,n∈Ob(Fin),x:m → Ob(M)是m索引對象集合,y:n → Ob(M)是n索引對象集合。若元素i∈n,mi是態射s對于i的原像,使用xi:=x|mi:mi → Ob(M)表示mi對應的x對象集合,則態射組合為:
:Mn(y;z)×∏i∈nMmi(xi:yi) → Mm(x;z)
2)兩個規則。
a)運算必須滿足結合率,相關形式化定義可參考文獻[1]。
b)對于態射φ:(x1,x2,…,xn) → y,恒等率表示為:
當對稱多范疇中的對象實例化為集合時,形成范疇Sets[1]。Sets中的對象是集合,態射是集合間的“多對一”函數(函數定義域為多集合,伴隨域為單集合;區別于Sets,Set中的函數沒有“多對一”的限制)。
定義2對稱多范疇上的函子[1]。設M和M′為對稱多范疇,從M到M′的函子F:M → M′定義包含兩種運算:a)對象上的運算,b)態射上的運算。所有運算必須滿足:a)恒等保持規則,b)組合保持規則。
基于對稱多范疇上的函子可定義對稱多范疇上的代數運算[1],例如:C是對稱多范疇M上的運算,則C:M → Sets。
1.2系統的嵌套式結構
當以外部觀察為依據,一個系統模塊可被視為一個黑盒。黑盒與外部通過“端口”來進行交互,端口是交互發生的位置,交互的內容是信息。基于“類型集合”[4],一個模塊黑盒可表示成為:
X=((Xin,τin),(Xout,τout))
其中:Xin為輸入端口集,Xout輸出端口集,端口集滿足Xin,Xout∈Ob(Fin);τ為端口類型函數,該函數用于獲得端口上交互信息的類型。對任意端口集P,類型函數的定義是τ:P → Ob(Set)。端口集P上可交互信息[4]表示為:
其中:p為P中的端口,τ(p)為p上的信息類型,(P,τ)為整個端口集上可交互的信息類型。
性質1[4]設f:(P,τ) → (P′,τ′)為兩個類型端口集上的態射,則 f-:(P′,τ′) → (P,τ)。
對嵌套結構,若X表示內層結構,Y表示外層結構,則d:X → Y表示X與Y之間的嵌套關系。結構d中內外層次上端口間的對應關系必修滿足:
規則1[4]若使用φ=(φin,φout)表示單層嵌套結構端口映射規則,其中,φin:Xin → Yin∪Xout,φout:Yout → Xout。
這里,φout規定外層結構的輸出端口必須與內層結構上的部分輸出接口相對應;φin規定內層結構的輸入端口必須與部分外層結構的輸入端口,以及部分內層結構的部分輸出端口相對應。
基于上述說明,設范疇NS是描述系統嵌套結構的對稱多范疇[3-4],則該范疇包含以下技術特征。
1)范疇中的對象集合為Ob(NS),設X為端口集合,則:X=((Xin,τin),(Xout,τout))∈Ob(NS);
2)范疇中的態射集合為NSn(x;y);其中,n為自然數,若d∈NSn(x;y),則d:(X1,X2,…,Xn) → y為單層嵌套結構,而且端口映射滿足規則1,態射d中(X1,X2,…,Xn)為n索引對象集x,且X1,X2,…,Xn,Y∈Ob(NS)。
3)恒等態射為NS1(x;x),即idX:(X) → X。
4)當X,Y,Z∈Ob(NS),若存在結構d:X → Y,以及d′:Y → Z,則兩層嵌套結構為:d′d:X → Z。
5)組合運算必須滿足結合率,當存在多層嵌套結構:d″d′d,則(d″d′)d=d″(d′d),即:整體嵌套結構與系統組成時的嵌套順序無關。
6)態射運算滿足恒等率。
圖1中使用矩形表示了三個對象:P、Q和C。P對象和Q對象構成內層結構X:=P∪Q;外層結構為對象C,定義Y:=C。使用d:X → Y表示圖中嵌套關系,結構中各層次所包含端口間的連線表示了不同對象上端口之間的對應關系。具體而言,Y結構的o端口對應X結構的q3端口(形成φout規則);X結構的q1端口對應于p2端口,且p1和q2端口對應Y結構的i1和i2端口(形成φin規則)。通過性質1可知:q3端口上的輸出決定o端口上的輸出;端口i1和i2上的輸入,以及p2端口的輸出決定p1、q2和q1端口的輸入。
1.3端口自動機
在NS范疇所描述的結構上,使用函子可定義相關代數運算。這樣的運算本質上是系統結構上動態特征的表現。為了揭示這樣的特征,本文使用“端口自動機”來定義系統行為。
端口自動機[13]是一種Moore機模型,可用于表達抽象系統的行為。該模型以外部觀察為基礎,把系統與外界交互端口作為行為考察的對象。定義上,端口自動機是一個七元組[13]:(P,Q,q0,X,Y,T,O);其中,P為端口集合,Q為狀態集合,q0為初始狀態,X為端口上的輸入值集合,Y為端口上的輸出值集合,T為輸入變遷函數,O為輸出狀態函數。
2嵌套式結構上的行為
基于端口自動機[13]和文獻[4]所闡述方法,本文定義NS范疇對象上的行為為:
定義3NS中對象上的行為。對于對象X∈Ob(NS),其行為表示為:
PAM(X):={(S,(fin, fout))|S∈Ob(Set), fin:Xin×S → S, fout:S → Xout}
其中:S為對象狀態集; fin為輸入函數;Xin是輸入數據集; fout為輸出函數;Xout是輸出數據集。 fin說明對象根據輸入信息更新系統狀態; fout說明對象根據當前狀態進行輸出。若f=(fin, fout),則PAM(X)可表示為:(S, f)。
當系統結構中包含兩個并行對象X和Y,表示為X∪Y,運算為PAM(X∪Y):=(SX×SY, fX×fY)。另外,根據定義3可知:PAM運算中的輸入和輸出操作為“確定的”,即任何操作的結果唯一。
定義4NS中態射上的行為。當X,Y∈Ob(NS),對于態射d:X → Y,φ=(φin,φout)是對象之間端口映射規則φin:Xin → Yin∪Xout,φout:Yout → Xout。若內層對象行為PAM(X) :=(S, f),則d上的行為定義為:
PAM(d):=(S,g)
其中S為嵌套結構上的狀態集,該集合由內層系統的狀態集決定,運行時S不允許被改變。另外,g=(gin,gout),其中,gin為d上的輸入函數,gout為d上的輸出函數。
對于結構d上映射規則φ,基于性質1可獲得:
φout:Xout → Yout,φin:Yin∪Xout → Xin
其中:Yin∪Xout使用Yin×Xout進行計算。
性質2定義4中,若s∈S,y∈Yin,則gin和gout為:
gout(s)=φout(fout(s))
gin(y,s)=fin(φin(y, fout(s)),s)
證明對于gout,從圖2(a)可獲得相關結論。根據映射規則φ,外層輸出端口Yout與內層輸出端口Xout相連,φout說明信息從X流向Y,為了實現φout,需要經過fout計算產生X的輸出。
對于gin:式子gin(y,s)=fin(φin(y, fout(s)),s)可從圖2(b)部分獲得。由于嵌套結構的狀態集合與內層系統狀態集合相同,根據φ,內層輸入端口Xin對應于:Xout和Yin。為了獲得Xout首先需要進行fout運算,而Yin為外部直接輸入。通過Xout與Yin可獲得內層系統的輸入Xin(由φin說明)。經過計算fin,系統狀態根據輸入被更新。
因此,性質2成立。
NS范疇中對象和態射可進行PAM運算:若X是一個對象,則運算為PAM(X);若態射d:X → Y,則運算為PAM(d)。由于范疇中的態射可組合,基于定義3和定義4,若PAM運算滿足組合運算,則PAM是一個函子。
作者修改了性質3
性質3PAM是對稱多范疇NS上的一個函子,該函子的計算結果是在指定狀態集上進行運算的動態系統。
性質3PAM是從對稱多范疇NS到Sets的一個函子,即PAM:NS → Sets。
證明
1)對象上的運算如本文定義3所述。
2)態射上的運算如本文定義4所述。
3)恒等保持方面,若idX:(X) → X,則:
PAM(idX):PAM(X) → PAM(X)=id(PAM(X))
4)組合保持方面,設:
5)最后,PAM運算的結果是集合,且運算f和g是“多對一”函數。所以,PAM的伴隨域是Sets。
綜上所述,PAM:NS → Sets是一個函子。
性質3說明:1)本文所構建的PAM運算是一個伴隨域為Sets的函子,運算具有結構保持特征。
綜上所述,PAM可在NS范疇的對象和態射上進行運算,而且運算具有結構保持特征,因此,PAM是一個函子,其伴隨域為指定狀態集上進行運算的動態系統。
性質3說明:1)本文所構建的PAM一個函子,可揭示結嵌套式系統結構上的輸入和輸出行為,以及相關的系統狀態變化情況。
2)區別于文獻[4]所闡述方法,PAM可直接以端口自動機方式來表達嵌套結構上的行為。
3行為的組合
使用NS范疇所建立的結構模型可從局部和整體兩個方面來進行理解。局部上,同一層次結構上可存在多個模塊,這些模塊相互交互、彼此組合形成一個工作單元,共同實現所在層次的行為。整體上,嵌套結構可涉及多個層次;外部結構的行為通過其內部結構的行為來實現,內部結構的行為再通過其更內部的結構行為來實現,以此類推,因此,層次結構上的局部行為是系統整體行為的組成部分。
同層次上模塊間的行為組合可歸納為4種類型[14-15]:重命名、并行組合、串行組合、反饋。4個類型中,當模塊的端口直接與其他端口進行連接時,即可實現所謂“重命名”。舉例來說,設某模塊具有端口p,該端口與外部端口q連接,則p上傳輸的信息實際上也是q上傳輸的信息;p和q之間的連接結構就是一種“重命名”實現。本部分后續內容將對其他3種行為的組合情況進行討論。
3.1并行組合
同一層次中,多個并行工作模塊間如果不存在信息交互時,它們的行為相互獨立。以圖4所表示的結構為例,該圖中包含3個對象:A、B和E,配置為:
內層結構由行為相互獨立的A和B組成,外層結構為E。設X:=A∪B,Y:=E,則:
Xin={q1,p1},Xout={q2,p2},Yin={i1,i2},Yout={o1,o2}
使用p:X → Y表示結構嵌套,根據定義4指定端口映射規則:
φinp:Xin → Yin,φoutp:Yout → Xout
圖4中X和Y之間的端口映射情況已通過連線進行表示,例如:E的輸入端口i1與A中的輸入端口q1相連,E的輸出端口o2與B中的輸出端口p2相連等。端口間交互情況為:
3.2串行組合
當同一層次中的模塊間存在信息交互時,它們的行為之間會產生依賴。以圖5所表示的結構為例,該圖中包含3個對象:C、D和E此處是否應該是E'?請明確。回復: 關于注釋中的問題處是E,不是E‘。謝謝您。
,配置為:
3.3反饋
對于反饋,以圖6表示的結構為例,使用F表示可反饋的模塊,使用E″作為外部環境,配置為:
4應用示例
實際應用中,首先根據需求設計模塊結構,基于NS范疇描述結構;然后基于PAM來分析模塊的工作情況。
示例1設兩個傳感器:測距模塊、電機編碼器,其中電機編碼器用于檢測電機的轉速。兩個模塊的基本狀態及狀態轉移情況總結在表1中。對于測距模塊,存在兩個狀態(s0為預備態,s1為測距態),輸出為測試結果d(d為實數,使用-1.0表示無讀數),輸入包含兩個命令(measure和reset)。對于電機編碼器,存在兩個狀態(s′0為預備態,s′1為讀數態),輸出為測試結果v(v為整數,使用0表示無讀數),輸入包含兩個命令(read和reset′)。
示例2當需要利用伺服電機來控制測距模塊的朝向時,可設計一個驅動模塊實現兩個功能:1)驅動伺服電機旋轉;2)啟動測距模塊進行測距。驅動模塊基本狀態及狀態轉移情況總結在表2中。該模塊有兩個基本狀態(b為預備態,t為轉向態),輸出包含兩個命令(measure和reset),輸入為轉向角度a(a∈{0,1,…,180},使用0表示預備)。
基于3.2節的討論,驅動模塊首先需要驅動伺服電機調整測距模塊的朝向,再啟動獲得距離,因此,輸入命令指定為:{a,0},其中,a為轉動角度。假設現在需要獲得伺服電機在90°角時測距模塊檢測的距離,輸入命令為{90,0};若系統當前狀態為(b,s0),執行命令中的第一個值(角度為90°),系統首先獲得D和U狀態輸出:(reset,-1.0); fin更新系統狀態,D模塊驅動伺服電機旋轉90°;同時,由于U模塊執行命令(reset),狀態為s0。再執行命令的第2個值(角度為0°),系統獲得當前D和U狀態輸出:(measure,-1.0), fin更新系統狀態,D模塊驅動伺服電機轉角0°;同時,U模塊執行命令(measure),系統當前可獲得輸出為實測距離d,因此可見:串聯的D和U基本可以工作。
5結語
使用“對稱多范疇”可建立系統多層嵌套式結構的模型。針對這樣的結構模型,本文基于端口自動機提出一種結構上的行為表達方法PAM,該方法在理論上是一個伴隨域為Sets的函子。在PAM支撐下,本文還對并行、串行和反饋等常見組合行為進行了分析和討論。本文首先提出一種基于端口自動機的行為表達方法:PAM,然后總結了與方法相關的理論性質,最后討論分析了PAM的應用方法。
通過本文工作可以看出:PAM方法支持以端口自動機方式揭示嵌套式結構上的動態行為,因此,該方法可被應用于描述或分析嵌套式系統結構上的行為。
未來的工作還可構建、討論和分析NS范疇上的其他行為表達方法。
參考文獻:
[1]
SPIVAK D I. The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plugandplay circuits [EB/OL]. [20151210]. http://arxiv.org/abs/1305.0297.
[2]
RUPEL D, SPIVAK D I. The operad of temporal wiring diagrams: formalizing a graphical language for discrete time processes [EB/OL]. [20151208]. http://arxiv.org/abs/1307.6894.
[3]
WISNESKY R, SPIVAK D I, SCHUITZ P, et al. Algebras of open dynamical systems on the operad of wiring diagrams [EB/OL]. [20151207]. http://arxiv.org/pdf/1408.1598.
[4]
SPIVAK D I. Nesting of dynamic systems and modedependent networks [EB/OL]. [20151205]. http://arxiv.org/abs/1502.07380.
[5]
LAWVERE F W, SCHANUEL S H. Conceptual Mathematics: A First Introduction to Categories [M]. 2nd ed. Cambridge, UK: Cambridge University Press, 2009: 13-21.
[6]
SIMMONS H. An Introduction to Category Theory [M]. Cambridge, UK: Cambridge University Press, 2011: 1-5.
[7]
SCOTT P J. Handbook of Algebra (Vol. 2) [M]. Amsterdam: Elsevier, 2000: 3-77.
[8]
LYNCH N A, STARK E W. A proof of Kahn principle for input/output automata [J]. Information and Computation, 1989, 82(1): 81-92.
[9]
SASSON V, NIELSEN M, WINSKEL. G. Models for concurrency: towards a classification [J]. Theoretical Computer Science, 1996, 170(1/2): 297-348.
[10]
徐家福,費宗銘.范疇論在計算機科學中的若干應用[J].計算機科學,1989,16,(3):11-17.(XU J F, FEI Z M. Several applications of category theory in computer science [J]. Computer Science, 1989,16(3): 11-17.)
[11]
楚旺,錢德沛.以體系結構為中心的構件模型的形式化語義[J].軟件學報,2006,17(6):1287-1297.(CHU W, QIAN D P. Formal semantic of architecturecentric component model [J]. Journal of Software, 2006, 17(6): 1287-1297.)
[12]
趙碩,陳中育,肖春水.基于范疇論的構件行為組合研究[J].計算機工程,2012,38(15):53-58.(ZHAO S, CHEN Z Y, XIAO C S. Research on component behavior combination based on category theory [J]. Computer Engineering, 2012, 38(15): 53-58.)
[13]
STEENSTRUP M, ARBIB M A, MANES E G. Port automata and the algebra of concurrent processes [J]. Journal of Computer and System Sciences, 1983, 27(1): 29-50.
[14]
STARK E W. Compositional relational semantics for indeterminate dataflow networks [C]// Proceedings of the Sixth International Conference on Category Theory and Computer Science, LNCS 389. Berlin: Springer, 1989: 52-74.
[15]
LEE E A, VINCENTELLIVINCENTELLI A. A framework for comparing models of computation [J]. IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, 1998, 17(12): 1217-1229.