苗德成，奚建清，戴經(jīng)國

1.韶關學院 信息科學與工程學院，廣東 韶關 512005

2.華南理工大學 軟件學院，廣州 510640

程序語言中基于Fibrations理論的索引共歸納數(shù)據(jù)類型*

苗德成1+，奚建清2，戴經(jīng)國1

1.韶關學院 信息科學與工程學院，廣東 韶關 512005

2.華南理工大學 軟件學院，廣州 510640

傳統(tǒng)范疇論與共代數(shù)等方法在分析語義行為與描述共歸納規(guī)則方面存在不足，應用Fibrations理論對程序語言中索引共歸納數(shù)據(jù)類型（indexed co-inductive data type，ICDT）進行了研究。通過基變換構造索引Fibration，建立索引Fibration的等式函子與商函子等工具，應用伴隨性質與保持等式的提升深入分析ICDT的語義行為；以此為基礎，構造ICDT上參數(shù)化的共遞歸操作，在Fibrations理論框架內(nèi)抽象描述具有普適意義的共歸納規(guī)則，并以實例分析簡要介紹Fibrations理論在ICDT中的應用。與傳統(tǒng)研究方法相比，F(xiàn)ibrations理論具有簡潔的描述性與靈活的擴展性，可以精確分析ICDT的語義行為，具有高度的抽象性且不依賴特定的計算環(huán)境，描述了ICDT具有普適意義的共歸納規(guī)則。

語義行為；共歸納規(guī)則；基變換；提升；共遞歸

1　引言

作為一種語義計算能力更強的共歸納數(shù)據(jù)類型[1]，ICDT（indexed co-inductive data type）以共代數(shù)[2-3]為數(shù)學基礎，將終結性與互模擬等工具引入類型理論研究中，在程序語言動態(tài)語義行為分析等方面具有獨特的優(yōu)勢。Fibrations理論是計算機科學基礎研究的一個新興方向，特別是在范疇論方法研究領域，已成為前沿熱點。同時，在數(shù)據(jù)庫系統(tǒng)建模[4-5]、軟件規(guī)范[6]和程序設計方法[7-8]等領域也有廣泛的應用，為有效描述形式系統(tǒng)間的結構化聯(lián)系提供了一種通用的思維方法、研究手段和理論工具。

從文獻檢索的情況看，Hagino最早應用Dialgebras結構與范疇論方法分析了歸納與共歸納數(shù)據(jù)類型間的關系[9]，奠定了共歸納數(shù)據(jù)類型的研究基礎，但在繼承、多態(tài)類型系統(tǒng)與共歸納原理等方面存在一定的不足。Poll基于子類型和繼承對Hagino的工作進行了拓展，應用代數(shù)與共代數(shù)的對偶性質研究了歸納與共歸納數(shù)據(jù)類型的子類型和繼承關系[10]。Nogueira等人應用雙代數(shù)（bialgebra）方法研究了歸納與共歸納數(shù)據(jù)類型的關系及其在多態(tài)編程中的應用[11]。文獻[12]利用λ-雙代數(shù)與分配律將歸納與共歸納數(shù)據(jù)類型有機融合起來，探討語法構造與動態(tài)行為關系，而文獻[13]進一步給出了強共歸納數(shù)據(jù)類型的定義及一種帶固定參數(shù)的共遞歸操作punfold，并結合共模態(tài)共遞歸給出unfold與punfold的結構化描述，同時分析了punfold上的各種計算律。Greiner與Hinze將共歸納原理引入到程序語言中，對程序語言中的共歸納數(shù)據(jù)類型進行了深入研究[1,14]。以上研究成果在一定程度上解決了上述問題。

Hermida與Jacobs證明了有商類型的終結共代數(shù)的共歸納規(guī)則是可靠的[15]。Ghani等人在文獻[15]的基礎上，突破多項式函子的限制，進一步將其研究工作擴展為一般意義上的函子類型[7,16]。同時，文獻[16]分析了ICDT與其語義行為在程序邏輯上的對應關系。文獻[17]在Jacobs等人研究的基礎上[15]，證明了Fibrations環(huán)境下互模擬共歸納證明方法的可靠性，并通過參數(shù)變換提出弱互模擬性證明的一種新范疇論方法。文獻[18]基于自反圖（reflexive graphs）提出了依賴數(shù)據(jù)類型的一種參數(shù)化模型，該模型可被視為從族fibration到其自反圖fibration的一種轉換，支持初始代數(shù)存在性的判定與推導。

最近，Ghani與Revell等人提出λ1-fibration的概念，以限定于卡式閉范疇的基范疇描述單位消除語義，以全范疇描述關系語義，并由λ1-fibration歸納地構造參數(shù)化計量單位fibrationUoM，證明了UoM的一些基本定理，給出一些UoM實例，在范疇論的層面對Kennedy的工作[19]進行了擴展[20]。Dorel等人應用共歸納原理提出了一個4規(guī)則的邏輯演繹系統(tǒng)來證明程序的等價性，并證明了該系統(tǒng)的可靠性與弱完備性[21]。Laura針對云存儲架構中的弱存儲模型與結果一致性存儲等問題，基于共歸納原理和進程演算引入存儲狀態(tài)兼容性的概念，在云存儲行為上進行共歸納推理，支持異構多源數(shù)據(jù)類型的描述[22]。

現(xiàn)有研究成果主要集中在共歸納數(shù)據(jù)類型及其在程序語言中的應用，而ICDT的研究當前還處于起步階段，在語義計算與程序邏輯等方面存在許多尚未解決的問題，如語義行為的分析與共歸納規(guī)則的描述等，特別是共歸納規(guī)則多以自動生成為主，缺乏堅實的數(shù)學基礎和精確的形式化描述。同時，傳統(tǒng)方法在局部卡式閉范疇內(nèi)建立ICDT的類型論模型，使得ICDT與描述其語義行為的關系共存于同一個范疇內(nèi)，導致自函子與其提升是等同的，在語義行為分析與共歸納規(guī)則描述方面存在一定的局限性。

針對以上問題，本文應用Fibrations理論對ICDT進行了研究。突破傳統(tǒng)方法對局部卡式閉范疇的限制，描述ICDT語義行為的關系不再局限于函數(shù)或態(tài)射，而是提升為全范疇中的對象。同時，ICDT與描述其語義行為的關系不再共存于同一個范疇內(nèi)，構造索引fibration及其等式函子等工具，并應用伴隨性質與保持等式的提升在共代數(shù)范疇內(nèi)深入分析ICDT的語義行為；構造ICDT上參數(shù)化的共遞歸操作，抽象描述具有普適意義的共歸納規(guī)則。

本文組織結構如下：首先，在切片范疇（slice category）上構造索引fibration及其等式函子等工具，深入分析ICDT的語義行為；其次，以此為基礎構造索引fibration基范疇上參數(shù)化的共遞歸操作，抽象描述具有普適意義的共歸納規(guī)則；再次，輔以實例簡要介紹Fibrations理論在ICDT中的應用；最后，總結全文并給出后續(xù)研究工作。

2　預備知識

本文假定讀者具備拉回（pullback）、圖表交換（diagram commute）與終對象（terminal object）等范疇論與共代數(shù)基礎。若范疇全體對象與態(tài)射都構成集合，則該范疇是小范疇（small category）[23]，本文的研究對象均基于小范疇?？ㄊ缴洌–artesian arrow）、fibration等Fibrations理論的基礎內(nèi)容可參見文獻[3, 24-26]等。記id為單位態(tài)射，Id為單位函子，1為終對象，Obj C為范疇C的對象集，Mor C為范疇C的態(tài)射集。

定義1（纖維）設P:T→B是兩個小范疇T、B間的一個fibration，稱B為基范疇，T為全范疇。對基范疇B中的一個對象C，?X∈Obj T，k∈Mor T，若有P(X)=C與P(k)=idC，則X與k構成的子范疇TC稱為對象C上的纖維，并稱k為垂直態(tài)射。

實際上，fibration是一種確保大量卡式射存在的函子，而纖維TC是全范疇T的一個全子范疇（full subcategory）。opfibration是fibration的對偶概念，若函子P:T→B既是一個fibration，又是一個opfibration，則稱P為bifibration。

定義2（重索引函子）基范疇B中的態(tài)射 f:C→D擴展為纖維TD與TC間的函子 f*:TD→TC，稱 f*為由 f歸納的重索引函子。

定義3（對偶重索引函子）基范疇B中的態(tài)射f:C→D擴展為纖維TC與TD間的一個函子*f:TC→TD，稱*f為由 f歸納的對偶重索引函子。

3　ICDT的語義行為

基于Fibrations理論的觀點，ICDT是一種常見的帶有離散索引對象的共歸納數(shù)據(jù)類型，如流、表與樹及帶環(huán)無限循環(huán)圖等復雜的數(shù)據(jù)結構，支持協(xié)同進程演算及其控制過程等。本文通過基變換構造索引fibration及其等式函子等工具，在共代數(shù)范疇內(nèi)應用伴隨函子的伴隨性質與保持等式的提升，對ICDT的語義行為進行深入分析，增強程序語言對ICDT語義行為的處理與證明能力。

3.1真值函子與關系fibration

定義4（纖維化終對象）設P:T→B是兩個小范疇T、B間的一個fibration，取?D∈Obj B，若?1D∈ObjTD為纖維TD上的終對象，且?f:C→D∈Mor B，f*(1D)為纖維TC上的終對象，即重索引函子 f*保持終對象，則稱fibrationP有纖維化終對象。

定義5（真值函子與內(nèi)涵函子）設P:T→B是兩個小范疇T、B間的一個fibration，函子TP:B→T將?C∈Obj B映射為纖維TC上的終對象，稱TP為fibrationP的真值函子。若TP有一個右伴隨函子{-}，則稱{-}為P的內(nèi)涵函子。

記1B與1T分別為基范疇B與全范疇T的終對象，則有P(1T)=1B。對?C∈Obj B，存在唯一的態(tài)射u:C→1B，有。對 ?f:C→D∈Mor B，，真值函子TP將 f映射為全范疇T上的卡式射。

例1設Set為集合范疇，?X∈Obj Set，X上的一個謂詞是一個二元組，其中，P:X→Set。對?x∈X，P(x)構成一個集合，描述x的語義行為，并稱X為謂詞的定義域。謂詞到的態(tài)射是一個序對(f,f～):→，其中f:X→X′是相應謂詞定義域上的函數(shù)，而對?x∈X,f～:P(x)→P′(f(x))，將P(x)映射為P′(f(x))。謂詞及其態(tài)射構成謂詞范疇 P，進而得到謂詞fibration Pre:P→Set，將全范疇P的對象映射為X。對 f:X→Y∈Mor Set，有P:Y→Set∈Obj P，則 f與的卡式射為謂詞范疇 P中的一對態(tài)射。謂詞fibrationPre的真值函子TPre將X映射為謂詞范疇P的單點集謂詞<{*},P>，P:{*}→Set。謂詞fibrationPre的內(nèi)涵函子{-}將謂詞映射為語義行為集{P(x)|x∈X}。

定義6（P的關系fibration）設P:T→B為兩個小范疇T、B間的一個fibration，基范疇B有積。令Δ:B→B為B上的對角自函子，將?C∈Obj B映射為積對象C×C。P沿Δ的拉回構成fibrationRel(P): Rel(T)→ B，稱Rel(P)為P的關系fibration。

Rel(P)全范疇Rel(T)的對象為關系(C,D)，對另一對象(C′,D′)，令 f:C→C′，g:D→D′，(f,g):(C,D)→(C′, D′)∈Mor Rel(T)。圖1中的關系fibrationRel(P)將關系(C,D)映射為基范疇B中的對象C，函子Π將(C,D)映射為T中的對象D，且有P(D)=Δ(C)。同時，定義6的拉回保持性質確保C上關于Rel(P)的纖維Rel(T)C與C×C上關于P的纖維TC×C是同構的，即。

由給定的fibration通過拉回構造一個新的fibration的過程稱為基變換，如定義6中P通過基變換構造Rel(P)。基變換具有保持結構的性質，如保持纖維化終對象[27]，即若P有真值函子TP，則Rel(P)有真值函子TRel(P)，且TRel(P)(C)=TP(C×C)。

設P:T→B是一個bifibration，基范疇B有拉回。若對B中任意一個拉回方形，如圖2所示，自然變換*s°t*→g*°*f是一個同構，則稱P滿足Beck-Chevalley條件。Beck-Chevalley條件（簡稱BC條件）實際上是由bifibrationP的基范疇中一個拉回方形定義了全范疇T中各相關纖維間函子保持結構的一種自然變換，進而確保重索引與對偶重索引函子滿足合適的圖表交換性質。

Fig.1　Relation fibrationRel(P)ofP圖1　P的關系fibrationRel(P)

Fig.2　Apullback square in base categoryBon bifibration圖2　bifibration基范疇B中任意一個拉回方形

定義7（等式函子）設P:T→B是一個滿足BC條件的bifibration，B有積，且TP為P的真值函子。對?C∈Obj B，自然變換δ:IdB→Δ在C的作用函數(shù)δC:C→C×C擴展為對偶重索引函子*δ，稱EqP:B→Rel(T)為P的等式函子，EqP=*δ°TP。

真值函子TP將C映射為TC上的終對象TP(C)，由定義6知Rel(P)是P沿Δ的基變換，則若P有纖維化終對象，則Rel(P)也有纖維化終對象。定義7中的*δ將TP(C)映射為*δ(TP(C))，而Rel(T)C)，且P的等式函子EqP將?f∈Mor B映射為δf與確定的 f×f上唯一態(tài)射。等式函子的直觀意義是，相同的參數(shù)得到相同的結果[15]。

3.2索引fibration與其等式函子

定理1設P:T→B是兩個小范疇T、B間的一個fibration或bifibration，TP:B→T為 P的真值函子。?I∈Obj B為基范疇B上的離散索引對象，令索引函子P/I:T/TP(I)→B/I為對?u:Y→TP(I)∈Obj T/TP(I)，有P/I(u)=P(u):P(Y)→I∈Obj B/I，則索引函子P I也是一個fibration或bifibration。

證明 取?f:C→D∈Mor B，存在 f上fibrationP的卡式射，使得P(X)=D，且存在唯一態(tài)射w:TP(I)→f*(X)，有與P(v)=f°h，如圖3所示。設α:D→I∈Obj B/I，β:C→I∈Obj B/I，則有γ:P(u)→α=P(Y)→D∈Mor B/I，δ:P(u)→β=P(Y)→C∈Mor B/I，滿足圖表交換γ=f°δ。在函子P I的全范疇T/TP(I)中，s:X→TP(I)∈Obj T/TP(I)，t:f*(X)→TP(I)∈Obj T/TP(I)，有g:u→s=Y→X∈Mor T/TP(I)，則存在唯一態(tài)射k:u→t=Y→f*(X)，滿足圖表交換，故是 f上函子P I的卡式射，即如果P是一個fibration，則索引函子P I也是一個fibration。

Fig.3　Cartesian arrowof functorP Ionf圖3　f上函子P I的卡式射

設m:Z→TP(I)∈Obj T/TP(I)，由函子P I的定義有P/I(m)=α，令為 f上P的對偶卡式射，如圖4所示。切片范疇B I中有圖表交換α=β°f，函子P I全范疇T/TP(I)中存在唯一態(tài)射n:*f(Z)→ TP(I)，滿足圖表交換，故是 f上函子P I的對偶卡式射，即如果P是一個opfibration，則索引函子P I也是一個opfibration。

Fig.4　Opposite Car tesian arrowof functorP Ionf圖4　f上函子P I的對偶卡式射

綜上，如果P是一個bifibration，則索引函子P I也是一個bifibration?！?/p>

定理1證明了索引fibrationP I與fibrationP具有相同的fibration或bifibration性質，同時也對索引fibration進行了定義。實際上，P沿定義域函子dom:B/I→B的基變換可具體構造一個索引fibration P/I:T/TP(I)→B/I，對?α:C→I∈Obj B I，P在C上的纖維TC與P I在α上的纖維(T/T(I))α是同構的[16]，且若P有真值函子，由P構造的索引fibrationP I也有真值函子。

對?α:C→I∈Obj B/I，設α沿自身的拉回分別為i與 j，則積對象α×α為α°i或α°j，即切片范疇B I的積對象由其拉回確定。與定義6類似，下面給出索引fibrationP I的關系fibration的定義。

定義8（P I的關系fibration）令P/I:T/TP(I)→B/I為一個索引fibration，基范疇 B I有積。設Δ/I:B/I→B/I為切片范疇B I上的對角自函子，將?α∈B/I映射為其積對象α×α。P I沿Δ I的拉回構成fibrationRel(P/I):Rel(T/TP(I))→B/I，稱Rel(P/I)為P I的關系fibration。

對Rel(P/I)在α上對象R∈Obj Rel(T/TP(I))，P I在α×α上對象R′∈Obj T/TP(I)，P在dom(α×α)上對象R″∈ObjT，有同構表達式R?R′?R″成立[16]。α在自然變換 δ/I:IdBI→Δ/I上的作用函數(shù)為 (δ/I)α: C→dom(α×α)，則自然變換δ I的直觀意義是將切片范疇中B I的一個對象變換為另一個對象的態(tài)射。與定義7類似，下面給出索引fibrationP I的等式函子的定義。

定義9（P I的等式函子）設P:T→B是一個滿足BC條件的bifibration，P有真值函子，且基范疇B有積。令索引fibrationP I的真值函子為TPI，稱EqPI=*(δ/I)°TPI:B/I→Rel(T/TP(I))為P I的等式函子。

等式函子EqPI將切片范疇B I中的對象α:C→I映射為α×α上的唯一態(tài)射*(δ/I)α°TPI(C)→TP(I)。下面構造索引fibrationP I的商函子。

3.3商函子與保持等式的提升

以fibrationP:T→B的等式函子EqP:B→Rel(T)替代 P的真值函子TP:B→T，P的關系fibration Rel(P)替代P，應用定理1，構造一個新的fibration Rel(P)/I:Rel(T)/EqP(I)→B/I，對 ?R∈Obj Rel(T)，Rel(P)/I將α:R→EqP(I)映射為α′:QR→I，α′是α在伴隨函子下的置換。

設?R=(C,D)∈Obj Rel(T/TP(I))，則QPI(C,D)=C，如圖5所示。Π(C,D)=D，對 f:D→TP(I)∈Obj T/TP(I)，P/I(f)=P(D)→I，而對g:C→I∈Obj B/I，Δ/I(g)=g×g，即dom(g×g)=P(D)。

Fig.5　Construction of quotient functorQPI圖5　商函子QPI的構造

例2記Set為集合范疇，I為一離散索引對象，則 Set在 I上的切片范疇為Set/I。對任意集合X∈Obj Set，存在X/I∈Obj Set/I。索引fibrationP I的關系fibration為Rel(P/I)，X I關于Rel(P/I)在Set/I上的纖維Rel(T/TP(I))XI由關系R:X/I×X/I→Set/I構成，即 Rel(T/TP(I))XI={R:X/I×X/I→Set/I|X/I∈Obj Set/I}。對X I中任意兩個對象α與α′，R(α,α′)給出α與α′某種關聯(lián)性（如等價、同余、同構等）的構造證明，如構造 R的一種等價性定義:若α?α′，R(α,α′)=1；否則R(α,α′)=0，其中?為等價。索引fibrationP I的等式函子EqPI將X I映射為關聯(lián)集R(X/I,X/I)，而商函子QPI則將關聯(lián)集R(X/I,X/I)映射為X I的商集(X/I)/R，(X/I)/R由含R的最小等價關系確定。

定義12（保持等式的提升）設P:T→B為一個滿足BC條件且有真值函子TP的bifibration，基范疇B有積與拉回，P/I:T/TP(I)→B/I是P的索引fibration，構造P I的關系fibrationRel(P/I)，并有P I的等式函子EqPI與商函子QPI。F是Rel(P/I)基范疇B I上的一個自函子，F(xiàn)⊥是Rel(P/I)全范疇Rel(T/TP(I))上的一個自函子，若滿足圖表交換Rel(P/I)°F⊥=F°Rel(P/I)，且有同構表達式 EqPI°F?F⊥°EqPI與F°QPI?QPI°

F⊥成立，則稱F⊥是F關于Rel(P/I)在全范疇Rel(T/TP(I))上的一個保持等式的提升。

3.4ICDT的語義行為

對?α:C→I∈Obj B/I，在自函子F作用下構成一個F-共代數(shù)(α,r:α→F(α))，稱α為載體（carrier）。(α,r)與另一F-共代數(shù)(β,t:β→F(β))的態(tài)射是r與t載體間的態(tài)射 f:α→β，并且滿足圖表交換t°f= F(f)°r。

定理2以F-共代數(shù)為對象，以F-共代數(shù)態(tài)射為態(tài)射，構成F-共代數(shù)范疇CoalgF。

證明 設dom:Mor CoalgF→Obj CoalgF為域函數(shù)，cod:Mor CoalgF→Obj CoalgF為共域函數(shù)，下面證明CoalgF是一個范疇。

令(α,r)，(β,t)，(γ,s)∈Obj CoalgF，f:(α,r)→(β,t)，g: (β,t)→(γ,s)∈Mor CoalgF，則 g°f:(α,r)→(γ,s)∈Mor CoalgF，故dom(g°f)=dom(f)=(α,r)，cod(g°f)=cod(g)= (γ,s)，滿足匹配條件。

設h:(γ,s)→(δ,v)∈Mor CoalgF，h°g:(β,t)→(δ,v)∈Mor CoalgF，故h°(g°f)=(α,r)→(δ,v)=(h°g)°f，滿足結合律條件。

對(α,r)∈Obj CoalgF，存在一個唯一的單位態(tài)射id(α,r)，有dom(id(α,r))=cod(id(α,r))=(α,r)，且對?f∈Mor CoalgF，若dom(f)=(α,r)，則 f°id(α,r)=f；若cod(f)=(α,r)，則id(α,r)°f=f，滿足單位態(tài)射存在條件。

由范疇的定義[26]知，CoalgF是一個由F-共代數(shù)及其態(tài)射構成的F-共代數(shù)范疇?！?/p>

終結F-共代數(shù)(νF,out:νF→F(νF))若存在，則是唯一同構的。終結共代數(shù)具有終結性的泛性質，其所確定的唯一同構性是研究ICDT語義行為的主要工具。

作為終結F-共代數(shù)載體的ICDTνF是函子F的最大不動點（maximal fixed point），函子F指稱ICDT νF的語法析構（destructor），out從外部觀察νF在該語法析構過程中一種語義行為。應用索引fibration P I的等式函子EqPI，將F-共代數(shù)(α,r)映射為一個F⊥-共代數(shù) EqPI(α,r)=(EqPI(α),EqPI(r):EqPI(α)→EqPI(F(α))?F⊥(EqPI(α)))。相應地，EqPI(νF)為終結F⊥-共代數(shù)的載體，即等式函子EqPI保持終對象。

定理3以F⊥-共代數(shù)為對象，以F⊥-共代數(shù)態(tài)射為態(tài)射，構成F⊥-共代數(shù)范疇CoalgF⊥。

證明證明過程與定理2類似，略?！?/p>

記Coalg(EqPI)為CoalgF到CoalgF⊥的函子，利用等式函子EqPI將關系fibrationRel(P/I)基范疇B I中的對象與態(tài)射映射為全范疇Rel(T/TP(I))中相應的對象與態(tài)射，并通過函子Coalg(EqPI)進一步建立CoalgF到CoalgF⊥的聯(lián)系。

令(EqPI(νF),out⊥:EqPI(νF)→F⊥(EqPI(νF)))是關系fibrationRel(P/I)全范疇Rel(T/TP(I))中的一個終結F⊥-共代數(shù)，則out⊥是out在函子Coalg(EqPI)作用下的同態(tài)（homomorphism）像，即Coalg(EqPI)(out)=out⊥。終結F⊥-共代數(shù)的終結性確保out⊥是唯一同構的，唯一同構泛性質的存在為分析ICDT的語義行為提供了極大的便利性。

與Coalg(EqPI)類似，記Coalg(QPI)為CoalgF⊥到CoalgF的函子，由伴隨函子的伴隨性質有對任一 F⊥-共代數(shù) (ω,q:ω→F⊥(ω))， ω:X→TP(I)∈Obj Rel(T/TP(I))，有Coalg(QPI)(q)=QPI(ω)→QPI(F⊥(ω))?F(QPI(ω))，即 Coalg(QPI)(q)=QPI(q)，則QPI(q)是q在函子Coalg(QPI)作用下的同態(tài)像，如圖6所示。若g:ω→EqPI(α)是q到EqPI(r)的F⊥-共代數(shù)態(tài)射，則QPI(q)到r的F-共代數(shù)態(tài)射h:QPI(ω)→α是g上的F-共代數(shù)同態(tài)。類似地，g是h上的F⊥-共代數(shù)同態(tài)。

Fig.6　Coalgebra category functor Coalg(EqPI)andCoalg(QPI)圖6　共代數(shù)范疇函子Coalg(EqPI)與Coalg(QPI)

函子Coalg(EqPI)的左伴隨Coalg(QPI)建立以QPI(ω)為載體的F-共代數(shù)與以ω為載體的F⊥-共代數(shù)間直觀的互推導關系，為ICDT的語義行為分析提供了一種以νF為終結共代數(shù)載體的簡潔與一致的建模方法。

4　ICDT的共歸納規(guī)則

對定義并運用了等式函子與商函子的fibration，ICDT共歸納規(guī)則的形式化描述與語義行為分析是一致的[15]。設fibrationP:T→B與索引fibrationP/I: T/TP(I)→B/I滿足定義12。F是P I的關系fibration Rel(P/I)的基范疇B I上的一個自函子，νF為終結F-共代數(shù)的載體，且F⊥為F關于Rel(P/I)保持等式的提升，則P I有以νF為ICDT的共歸納規(guī)則。同時，若函子Coalg(EqPI)保持終對象，則F⊥生成一個可靠的共歸納規(guī)則。這為F⊥應用終結F-共代數(shù)在ICDT上生成共歸納規(guī)則的有效性（validity）判定提供了一種可靠依據(jù)，即若索引fibrationP I定義并運用等式函子與商函子分析ICDT的語義行為，則其基于終結F-共代數(shù)的共歸納規(guī)則在程序語言語義行為分析過程中是有效的。下面在Fibrations理論框架內(nèi)提出并抽象描述ICDT具有普適意義的共歸納規(guī)則。

基于范疇論的觀點，共歸納數(shù)據(jù)類型的共遞歸計算源于終結共代數(shù)語義[2]。設?α:C→I∈Obj B/I，令νF∈Obj B/I，應用F構造基范疇B I上ICDT的共遞歸操作unfold:(α→F(α))→α→νF。對任意一個F-共代數(shù)(α,r:α→F(α))，unfold r將(α,r)映射為r到終結F-共代數(shù)(νF,out)的唯一F-共代數(shù)態(tài)射unfold r:α→νF。源于終結共代數(shù)語義的unfold本質上是共歸納數(shù)據(jù)類型一個參數(shù)化（parameterized）的共遞歸操作，其共遞歸計算具有語義正確，擴展靈活與表達簡潔等良好性質。

由定義12可知，EqPI(F(α))?F⊥(EqPI(α))，EqPI(F(νF))?F⊥(EqPI(νF))，而等式函子 EqPI保持終對象，則EqPI(νF)為終結F⊥-共代數(shù)的載體，記νF⊥= EqPI(νF)，X=EqPI(α)。應用自函子F⊥構造全范疇Rel(T/TP(I))上ICDT共遞歸操作unfold:(X→F⊥(X))→X→νF⊥。

對任意一個F⊥-共代數(shù)(X,q:X→F⊥(X))，unfold q將q映射為(X,q)到終結F⊥-共代數(shù)(νF⊥,out⊥)的唯一F⊥-共代數(shù)態(tài)射unfold q:X→νF⊥。對?α∈Obj B/I，?X∈Obj Rel(T/TP(I))，有ICDT具有普適意義的共歸納規(guī)則:CoindUni:(X→F⊥(X))→X→EqPI(νF)。

若(X,q:X→F⊥(X))是F-共代數(shù)(α,r:α→F(α))上的F⊥-共代數(shù)，則CoindUniX q是unfold r上的F⊥-共代數(shù)同態(tài)。

5　實例分析

例3流或無窮序列的元素類型由索引I指定，如自然數(shù)類型Nat，整型Int與字符型Char等，?I∈Obj B。對任意流α:S→I∈Obj B/I，有B I上自函子F:α→I×α，其中head:α→I為流的頭函數(shù)，tail:α→α為去掉頭元素后的尾函數(shù)。應用定理1構造索引fibrationP I，并取P I的關系fibrationRel(P/I)全范疇Rel(T/TP(I))中任一流性質R∈Obj Rel(T/TP(I))，如互模擬，則對B I中另一流對象β:S′→I，有α與β在互模擬性質R上的一個共歸納成立。

R是兩個流類型α與 β間的互模擬關系，當且僅當?(α,β)∈R，head(α)=head(β)，且(tail(α),tail(β))∈R。

由定理2知F-共代數(shù)及其態(tài)射構成F-共代數(shù)范疇CoalgF，若CoalgF中終結F-共代數(shù)(νF,out: νF→F(νF))存在，令流類型Stream(I)為該終結F-共代數(shù)的載體νF。自函子F應用定義12可構造一個保持等式的提升F⊥，F(xiàn)⊥-共代數(shù)及其態(tài)射應用定理3可構成F⊥-共代數(shù)范疇CoalgF⊥。對CoalgF中任一F-共代數(shù)(α,r:α→F(α))，通過關系fibrationRel(P/I)提升為CoalgF⊥中的一個F⊥-共代數(shù)(X,q:X→F⊥(X))，滿足圖表交換F°Rel(P/I)(X)=Rel(P/I)°F⊥(X)。終結F-共代數(shù)的終結性定義Stream(I)上一個共遞歸操作unfold r，執(zhí)行Stream(I)的判定；而由終結F⊥-共代數(shù)的終結性對應得到一個共遞歸操作，描述Stream(I)的語義行為。若q位于r上，則CoindUniX q是unfold r上的F⊥-共代數(shù)同態(tài)，且遍歷關系fibrationRel(P/I)全范疇Rel(T/TP(I))中每一性質R，R∈Obj Rel(T/TP(I))，得到描述Stream(I)行為的語義集{R(X,X)|X=EqPI(α),?α∈Obj B/I}。

例3中的unfold r直觀描述了流類型α到其語義行為的映射關系。unfold r的存在性提供了共代數(shù)到其終結共代數(shù)同態(tài)射的一種有效方式，進而得到共歸納定義原則，即定義函數(shù)unfold r:α→Stream(I)，只需在α上構造相應操作r，令(α,r)成為一個F-共代數(shù)即可，F(xiàn)(α)=I×α。同時，unfold r的唯一性進一步證明兩個同態(tài)射相等，從而得到共歸納證明原則，即證明m,n:α→Stream(I)相等，只需證明m與n都是同一個共代數(shù)(α,r)到其終結F-共代數(shù)(Stream(I),out: Stream(I)→F(Stream(I)))的同態(tài)射即可，即證明m與n都等于unfold r。

相對于傳統(tǒng)的范疇論與共代數(shù)研究方法，例3具有同樣的表達能力，但在語義行為分析與共歸納規(guī)則描述方面比前者更強，如表1所示。例如，互模擬是共代數(shù)與自動機理論研究的核心內(nèi)容，例3從Fibrations理論的角度進一步拓展傳統(tǒng)共代數(shù)方法的研究內(nèi)容，在關系fibrationRel(P/I)上建立描述Stream(I)共遞歸計算的共歸納規(guī)則CoindUni，突破傳統(tǒng)方法多以自動生成共歸納規(guī)則為主的局限，提供一種精確、簡潔的形式化描述方式。特別是在函數(shù)式程序語言（如Haskell、ML等）中，CoindUni生成的代碼片段具有易讀、易寫與易理解等良好性質。

Table 1　Expression abilities between Fibrations and traditional methods表1　Fibrations理論與傳統(tǒng)方法的表達能力比較

例4確定有窮狀態(tài)自動機（deterministic finite automaton，DFA）狀態(tài)空間K的具體類型由離散索引對象I指定，如字母、數(shù)字與時間序列等，?I∈Obj B。Σ為DFA的有限輸入表，B I上自函子F:K×Σ→K為狀態(tài)轉移函數(shù)。記1為終對象，ε為空輸入。對K中的任意狀態(tài)x:K→I∈Obj B/I，a∈Σ，若F(x,a)=1，則DFA停機；F(x,a)∈K，則DFA成功運行并產(chǎn)生一個新狀態(tài)。應用定理1構造索引fibrationP I，并取P I的關系fibration全范疇中任一DFA性質U∈Obj Rel(T/TP(I))，如可達性，則對另一狀態(tài)x′:K→I，輸入a時有從狀態(tài)x到x′可達的一個共歸納成立:

若CoalgF中終結F-共代數(shù)(νF,out:νF→F(νF))存在，令DFA(I)為該終結F-共代數(shù)的載體νF。應用定義12由F可構造一個保持等式的提升F⊥。對CoalgF中任一F-共代數(shù)(τ,l:τ→F(τ))，通過關系fibrationRel(P/I)提升為CoalgF⊥中的一個F⊥-共代數(shù)(Z,m:Z→F⊥(Z))，滿足圖表交換 F°Rel(P/I)(Z)= Rel(P/I)°F⊥(Z)。由終結 F-共代數(shù)的終結性定義DFA(I)上一個共遞歸操作unfold l，執(zhí)行DFA(I)的判定；而由終結F⊥-共代數(shù)的終結性對應得到一個共遞歸操作，描述DFA(I)的語義行為。若m位于l上，則CoindUniZ m是unfold l上的F⊥-共代數(shù)同態(tài)，且遍歷全范疇Rel(T/TP(I))中每一性質U，得到描述DFA(I)行為的語義集{U(Z,Z)|Z=EqPI(τ),?τ∈Obj B/I}。

可達性是自動機理論研究的重要內(nèi)容，例4在統(tǒng)一的Fibrations理論框架內(nèi)研究自動機狀態(tài)的可達性具有較強的普適意義，脫離不相關的語法細節(jié)，直接面向特定的領域問題。傳統(tǒng)研究方法中，操作語義方法證明自動機中兩個狀態(tài)在語義行為上等價，指稱語義方法證明兩個狀態(tài)在語義模型中指稱同一個對象，而數(shù)理邏輯方法則證明程序語言的兩個狀態(tài)在所有可能的模型中映射到同一個對象。以上3種方法依賴于操作語義、指稱語義與類型論等特定的計算環(huán)境，缺乏通用的建模概念，不具有普適意義。在建模工具的普適性方面，F(xiàn)ibrations理論與傳統(tǒng)方法的比較如表2所示。

Table 2　Universality between Fibrations and traditional methods表2　Fibrations理論與傳統(tǒng)方法的普適性比較

6　結束語

本文基于切片范疇B I建模，較好地處理了以I為索引的單類ICDT的語義行為及其共歸納規(guī)則的分析與描述，但I只是針對單類特定的ICDT，難以有效處理互遞歸（mutual recursive）等更為復雜的多類ICDT。將單類索引fibration的離散索引對象I擴充為索引范疇C，構造多類索引fibration，以Obj C為索引集描述B中的多類ICDT，在索引范疇C上基于fibrationG:B→C進行多類ICDT的語義行為建模，針對不同的索引選擇不同的程序邏輯，是下一步的研究工作。同時，初步探討ICDT及其共歸納規(guī)則構成復雜形式系統(tǒng)的可靠性、完備性與一致性等元性質。另外，應用Fibrations理論將ICDT的研究成果推廣到2-范疇，深入探討程序語言語義計算與程序邏輯在高階范疇中的數(shù)學結構和范疇性質也是下一步研究工作的重點。

[1]Greiner J.Programming with inductive and co-inductive types, CMU-CS-92-109[R].Pittsburgh,USA:School of Computer Science,Carnegie Mellon University,1992.

[2]Rutten J.Universal coalgebra:a theory of systems[J].Theoretical Computer Science,2000,249(1):3-80.

[3]Zhou Xiaocong,Shu Zhongmei.A survey on the coalgebraic methods in computer science[J].Journal of Software,2003,14(10):1661-1671.

[4]Johnson M,Rosebrugh R.Fibrations and universal view updatability[J].Theoretical Computer Science,2007,388(1/3): 109-129.

[5]Johnson M,Rosebrugh R,Wood R J.Lenses,fibrations and universal translations[J].Mathematics Structure in Computer Science,2012,22(1):25-42.

[6]Tews H.Coalgebra method for object-oriented specification [D].Dresden,Germany:Institute of Theoretical Information,Technical University Dresden,2002.

[7]Ghani N,Johann P,Fumex C.Generic fibrational induction[J]. Logical Methods in Computer Science,2012,8(2):1-27.

[8]Miao Decheng,Xi Jianqing,Jia Lianyin,et al.Formal language algebraic model[J].Journal of South China University of Technology:Natural Science Edition,2011,39(10):74-78.

[9]Hagino T.A Categorical programming language[D].Edinburgh,UK:Laboratory for Foundations of Computer Science,Department of Computer Science,University of Edinburgh,1987.

[10]Poll E.Subtyping and inheritance for categorical data types[J]. Sūrikaisekikenkyūsho Kōkyūroku,1998,1023:112-125.

[11]Nogueira P,Moreno-Navarro J.Bialgebra views:a way for polytypic programming to cohabit with data abstract[C]// Proceedings of the 2008 ACM SIGPLAN Workshop on Generic Programming,Victoria,Canada,Sep 20,2008.New York:ACM,2008:61-73.

[12]Su Jindian,Yu Shanshan.Coinductive data types and their applications in programming languages[J].Computer Science,2011,38(11):114-118.

[13]Su Jindian,Yu Shanshan.Comonadic corecursions on strong coinductive data types[J].Journal of South China University ofTechnology:Natural Science Edition,2014,42(1):128-134.

[14]Hinze R.Reasoning about Codata[C]//LNCS 6299:Central European Functional Programming School,Third Summer School,Budapest,Hungary,May 21-23,2009.Berlin,Heidelberg:Springer,2010:42-93.

[15]Hermida C,Jacobs B.Structural induction and coinduction in a fibrational setting[J].Information and Computation, 1998,145(2):107-152.

[16]Ghani N,Johann P,Fumex C.Indexed induction and coinduction,fibrationally[J].Logical Methods in Computer Science,2013,9(3/6):1-31.

[17]Bonchi F.Petrisan D,Pous D,et al.Coinduction up-to in a fibrational setting[C]//Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science,Vienna,Austria,Jul 14-18,2014.New York:ACM,2014:1-18.

[18]Atkey R,Ghani N,Johann P.A relationally parametric model of dependent type theory[J].ACM SIGPLAN Notices,2014, 49(1):503-515.

[19]Kennedy A J.Relational parametricity and units of measure [C]//Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,Paris, France,Jan 1997.New York:ACM,1997:442-455.

[20]Ghani N,Revell T,Atkey R,et al.Fibrational units of measure[EB/OL].[2015-03-21].https://personal.cis.strath.ac.uk/ neil.ghani/pub.html.

[21]Dorel L,Vlad R.Program equivalence by circular reasoning[J]. FormalAspects of Computing,2015,27(4):701-726.

[22]Laura B,Hernán M.On the behavior of general purpose applications on cloud storages[J].Service Oriented Computing andApplications,2015,9(3):213-227.

[23]Barr M,Wells C.Category theory for computing science[M]. New York:Prentice-Hall,1990:252-270.

[24]Pavlovic D.Predicates and fibrations[D].Utrecht,Nederland:University of Utrecht,1990.

[25]Jacobs B.Categorical logic and type theory[M].Amsterdam,Nederland:Elsevier Science,2001:20-107.

[26]Qu Yanwen.Formal semantics foundation and formal description[M].2nd ed.Beijing:Science Press,2010:118-172.

[27]He Wei.Category theory[M].Beijing:Science Press,2006: 23-44.

附中文參考文獻：

[3]周曉聰,舒忠梅.計算機科學中的共代數(shù)方法的研究綜述[J].軟件學報,2003,14(10):1661-1671.

[8]苗德成,奚建清,賈連印,等.一種形式語言代數(shù)模型[J].華南理工大學學報:自然科學版,2011,39(10):74-78.

[12]蘇錦鈿,余珊珊.程序語言中的共歸納數(shù)據(jù)類型及其應用[J].計算機科學,2011,38(11):114-118.

[13]蘇錦鈿,余珊珊.強共歸納數(shù)據(jù)類型上的Comonadic共遞歸[J].華南理工大學學報:自然科學版,2014,42(1):128-134.

[26]屈延文.形式語義學基礎與形式說明[M].2版.北京:科學出版社,2010:118-172.

[27]賀偉.范疇論[M].北京:科學出版社,2006:23-44.

MIAO Decheng was born in 1979.He received the Ph.D.degree in computer application technology from South China University of Technology in 2012.Now he is an associate professor at Shaoguan University.His research interests include formal languages theory and category theoretical methods,etc.

苗德成（1979—），男，黑龍江伊春人，2012年于華南理工大學獲得博士學位，現(xiàn)為韶關學院副教授，主要研究領域為形式語言理論，范疇論方法等。

XI Jianqing was born in 1962.He received the Ph.D.degree in computer architecture from National University of Defense Technology in 1992.Now he is a professor and Ph.D.supervisor at South China University of Technology. His research interests include database and software theory,etc.

奚建清（1962—），男，江蘇無錫人，1992年于國防科技大學獲得博士學位，現(xiàn)為華南理工大學教授、博士生導師，主要研究領域為數(shù)據(jù)庫，軟件理論等。

DAI Jingguo was born in 1962.He received the M.S.degree in software engineering from Wuhan University in 1994.Now he is a professor and M.S.supervisor at Shaoguan University.His research interests include formal semantics and sound software,etc.

戴經(jīng)國（1962—），男，湖南雙峰人，1994年于武漢大學獲得碩士學位，現(xiàn)為韶關學院教授、碩士生導師，主要研究領域為形式語義學，可靠性軟件等。

Indexed Co-inductive Data Type Based on Fibrations Theory in Programming?

MIAO Decheng1+,XI Jianqing2,DAI Jingguo1
1.School of Information Science and Engineering,Shaoguan University,Shaoguan,Guangdong 512005,China
2.School of Software,South China University of Technology,Guangzhou 510640,China

E-mail:tony10860@126.com

Traditional methods including category theory and coalgebra have some drawbacks to analyze semantic behavior and describe co-inductive rule,this paper explores indexed co-inductive data type(ICDT)in programming by Fibrations theory.Firstly,this paper constructs indexed Fibration by change of base,presents some tools such as equation functor and quotient functor of indexed Fibration,and then analyzes deeply semantic behavior of ICDT by adjunction property and lifting equation-preserving.Based on this,this paper proposes a parameterized co-recursive operation on ICDT to describe abstractly co-inductive rule with universality in the framework of Fibrations theory, also briefly introduces applications of Fibrations theory for ICDT by example.Compared with traditional methods, brief descriptions and flexible expansibility of Fibrations theory can analyze semantic behavior of ICDT accurately, its superior abstractness doesn?t rely on particular computing environments to describe co-inductive rule with universality of ICDT.

semantic behavior;co-induction rule;change of base;lifting;co-recursion

2015-08,Accepted 2015-10.

10.3778/j.issn.1673-9418.1508047

A

TP301.2

*The National Natural Science Foundation of China under Grant No.61103038(國家自然科學基金);the Natural Science Foundation of Guangdong Province under Grant No.S2013010015944(廣東省自然科學基金);the High School Outstanding Young Teacher Training Plan Foundation of Guangdong Province under Grant No.YQ2014155(廣東省高等學校優(yōu)秀青年教師培養(yǎng)計劃).

CNKI網(wǎng)絡優(yōu)先出版:2015-11-11,http://www.cnki.net/kcms/detail/11.5602.TP.20151111.1644.002.html

MIAO Decheng,XI Jianqing,DAI Jingguo.Indexed co-inductive data type based on Fibrations theory in programming.Journal of Frontiers of Computer Science and Technology,2016,10(10)：1482-1492.