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

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

1.韶關(guān)學(xué)院 信息科學(xué)與工程學(xué)院，廣東 韶關(guān) 512005

2.華南理工大學(xué) 軟件學(xué)院，廣州 510640

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

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

1.韶關(guān)學(xué)院 信息科學(xué)與工程學(xué)院，廣東 韶關(guān) 512005

2.華南理工大學(xué) 軟件學(xué)院，廣州 510640

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

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

1　引言

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

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

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

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

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

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

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

2　預(yù)備知識(shí)

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

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

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

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

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

3　ICDT的語(yǔ)義行為

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

3.1真值函子與關(guān)系fibration

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

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

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

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

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

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

由給定的fibration通過(guò)拉回構(gòu)造一個(gè)新的fibration的過(guò)程稱為基變換，如定義6中P通過(guò)基變換構(gòu)造Rel(P)?；儞Q具有保持結(jié)構(gòu)的性質(zhì)，如保持纖維化終對(duì)象[27]，即若P有真值函子TP，則Rel(P)有真值函子TRel(P)，且TRel(P)(C)=TP(C×C)。

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

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

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

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

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

3.2索引fibration與其等式函子

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Fig.5　Construction of quotient functorQPI圖5　商函子QPI的構(gòu)造

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

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

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

3.4ICDT的語(yǔ)義行為

對(duì)?α:C→I∈Obj B/I，在自函子F作用下構(gòu)成一個(gè)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ù)為對(duì)象，以F-共代數(shù)態(tài)射為態(tài)射，構(gòu)成F-共代數(shù)范疇CoalgF。

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

令(α,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)，滿足匹配條件。

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

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

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

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

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

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

證明證明過(guò)程與定理2類(lèi)似，略?！?/p>

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

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

與Coalg(EqPI)類(lèi)似，記Coalg(QPI)為CoalgF⊥到CoalgF的函子，由伴隨函子的伴隨性質(zhì)有對(duì)任一 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)。類(lè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ù)間直觀的互推導(dǎo)關(guān)系，為ICDT的語(yǔ)義行為分析提供了一種以νF為終結(jié)共代數(shù)載體的簡(jiǎn)潔與一致的建模方法。

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

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

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

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

對(duì)任意一個(gè)F⊥-共代數(shù)(X,q:X→F⊥(X))，unfold q將q映射為(X,q)到終結(jié)F⊥-共代數(shù)(νF⊥,out⊥)的唯一F⊥-共代數(shù)態(tài)射unfold q:X→νF⊥。對(duì)?α∈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　實(shí)例分析

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

R是兩個(gè)流類(lèi)型α與 β間的互模擬關(guān)系，當(dāng)且僅當(dāng)?(α,β)∈R，head(α)=head(β)，且(tail(α),tail(β))∈R。

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

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

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

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

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

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

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

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

6　結(jié)束語(yǔ)

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

[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.

附中文參考文獻(xiàn)：

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

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

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

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

[26]屈延文.形式語(yǔ)義學(xué)基礎(chǔ)與形式說(shuō)明[M].2版.北京:科學(xué)出版社,2010:118-172.

[27]賀偉.范疇論[M].北京:科學(xué)出版社,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年于華南理工大學(xué)獲得博士學(xué)位，現(xiàn)為韶關(guān)學(xué)院副教授，主要研究領(lǐng)域?yàn)樾问秸Z(yǔ)言理論，范疇論方法等。

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—），男，江蘇無(wú)錫人，1992年于國(guó)防科技大學(xué)獲得博士學(xué)位，現(xiàn)為華南理工大學(xué)教授、博士生導(dǎo)師，主要研究領(lǐng)域?yàn)閿?shù)據(jù)庫(kù)，軟件理論等。

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)國(guó)（1962—），男，湖南雙峰人，1994年于武漢大學(xué)獲得碩士學(xué)位，現(xiàn)為韶關(guān)學(xué)院教授、碩士生導(dǎo)師，主要研究領(lǐng)域?yàn)樾问秸Z(yǔ)義學(xué)，可靠性軟件等。

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(國(guó)家自然科學(xué)基金);the Natural Science Foundation of Guangdong Province under Grant No.S2013010015944(廣東省自然科學(xué)基金);the High School Outstanding Young Teacher Training Plan Foundation of Guangdong Province under Grant No.YQ2014155(廣東省高等學(xué)校優(yōu)秀青年教師培養(yǎng)計(jì)劃).

CNKI網(wǎng)絡(luò)優(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.