范疇數(shù)據(jù)類型上的子類型*

蘇錦鈿 余珊珊

(1．華南理工大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院，廣東廣州510006;2．中山大學(xué)信息科學(xué)與技術(shù)學(xué)院，廣東廣州510275)

范疇數(shù)據(jù)類型(CDT)研究是指以范疇論為數(shù)學(xué)理論基礎(chǔ)研究數(shù)據(jù)類型的描述、計(jì)算語義、構(gòu)造或行為特征、數(shù)學(xué)性質(zhì)及其在計(jì)算機(jī)科學(xué)中的應(yīng)用等．CDT主要包括歸納數(shù)據(jù)類型［1］(如自然數(shù)、有限分支樹、鏈表和隊(duì)列等)和共歸納數(shù)據(jù)類型［2-3］(如無限的流、鏈表、堆棧和樹等)．歸納數(shù)據(jù)類型研究是指利用代數(shù)研究遞歸類型中有限數(shù)據(jù)類型的構(gòu)造語義及其遞歸性質(zhì)．共歸納數(shù)據(jù)類型研究是指利用共代數(shù)研究共遞歸類型中無限數(shù)據(jù)類型的行為語義及其共遞歸性質(zhì)．

作為類型理論研究的一個(gè)核心概念，代數(shù)子類型描述了兩個(gè)歸納數(shù)據(jù)類型在構(gòu)造操作下的一種結(jié)構(gòu)保持關(guān)系，而共代數(shù)子類型則描述了兩個(gè)共歸納數(shù)據(jù)類型在觀察操作下的一種行為保持關(guān)系．Poll［4］對(duì)歸納數(shù)據(jù)類型上的子類型進(jìn)行了研究，并將代數(shù)子類型引入到范疇數(shù)據(jù)類型中，給出了共歸納數(shù)據(jù)類型間的共代數(shù)子類型定義及相應(yīng)的終結(jié)共代數(shù)語義解釋．

對(duì)許多CDT來說，除了包含構(gòu)造操作外，還包含觀察操作，即同時(shí)具有歸納和共歸納數(shù)據(jù)類型的典型特征．Erwig［5］指出，每個(gè)抽象數(shù)據(jù)類型都可描述成一個(gè)雙代數(shù)，并探討了以共代數(shù)函子為參數(shù)的遞歸操作．Nogueira等［6］利用雙代數(shù)對(duì)抽象數(shù)據(jù)類型進(jìn)行描述，并探討了它們的雙代數(shù)結(jié)構(gòu)在多態(tài)編程中的應(yīng)用．筆者在前期研究中發(fā)現(xiàn):雙代數(shù)可以給出數(shù)據(jù)類型上構(gòu)造操作和觀察操作的統(tǒng)一描述，并結(jié)合分配律探討了歸納與共歸納數(shù)據(jù)類型、fold與unfold之間的關(guān)系［7-8］．上述研究均沒有分析包含構(gòu)造和觀察操作的數(shù)據(jù)類型間的子類型關(guān)系及其性質(zhì)，也沒有給出雙代數(shù)結(jié)構(gòu)中的子類型定義及語義解釋．

為此，文中分析了歸納數(shù)據(jù)類型上的代數(shù)子類型和共歸納數(shù)據(jù)類型上的共代數(shù)子類型的范疇論定義及其語義，并利用雙代數(shù)給出了CDT上構(gòu)造操作和觀察操作的一種抽象描述;然后，將代數(shù)子類型和共代數(shù)子類型擴(kuò)展到基于雙代數(shù)的CDT上，給出了它們?cè)陔p代數(shù)中的定義及其語義解釋．

1 范疇數(shù)據(jù)類型及子類型

為便于描述，文中用F、G和H表示代數(shù)函子，B、D和E表示共代數(shù)函子，α、φ和δ分別表示函子F、G和H的基調(diào)，β、φ、σ分別表示函子B、D和E的基調(diào)，αX和αY分別表示同一函子F在不同載體集X和Y上的基調(diào)．

1．1 歸納數(shù)據(jù)類型及代數(shù)子類型

歸納數(shù)據(jù)類型可以表示為代數(shù)，其中代數(shù)函子給出了數(shù)據(jù)類型上各種構(gòu)造操作的抽象描述．

定義1 給定范疇 和函子F: ，F(xiàn)-代數(shù)定義為二元組(X，αX:FX X)，其中X是 中的對(duì)象，稱為該F-代數(shù)的載體;αX是 中的射，稱為該F-代數(shù)的基調(diào)．任意兩個(gè) F-代數(shù)(X，αX)和(Y，αY)間的同態(tài)射 f:(X，αX)(Y，αY)是 中的射 f:XY，且滿足f?αX= αY?Ff．

在范疇論視角下，每個(gè)歸納數(shù)據(jù)類型恰好是某個(gè)代數(shù)函子的初始代數(shù)，且為遞歸類型等式的最小不動(dòng)點(diǎn)．

定義2 給定函子 F: ，稱(μF，inF:FμF μF)為初始F-代數(shù)，當(dāng)且僅當(dāng)對(duì)于任意一個(gè)F-代數(shù)(X，αX)，存在唯一射 foldF(αX):μF X，使得圖 1 中的圖表滿足交換條件．其中，foldF(αX)是由基調(diào)αX所確定的迭代射，在函數(shù)式程序語言中也稱為fold射［9］或 catamorphism［1］．

圖1 初始代數(shù)及唯一射Fig．1 Initial algebras and the unique morphism

例1 參數(shù)化數(shù)組AList上的初始化操作(nil:1AList)和插入操作(cons:A×AListAList)可抽象地描述為代數(shù)函子ListF(X)=1+A×X，且AList為初始 ListF-代數(shù)，記為 ListAlg=(AList，inListF=［nil，cons］)，其中 A為某個(gè)已知的數(shù)據(jù)類型，如整型、字符串或布爾類型．

對(duì)歸納數(shù)據(jù)類型來說，代數(shù)子類型是指子數(shù)據(jù)類型上的構(gòu)造操作在父數(shù)據(jù)類型中得到保持，可理解為兩個(gè)歸納數(shù)據(jù)類型間存在一個(gè)滿足合適條件的射，將每個(gè)子數(shù)據(jù)類型的元素映射為父數(shù)據(jù)類型的元素．例如，若類型A是類型A'的代數(shù)子類型，記為A≤AlgA'，則意味著A的元素同時(shí)也是A'的元素．一方面，子數(shù)據(jù)類型A上的所有構(gòu)造操作都包含在父數(shù)據(jù)類型A'中;另一方面，由A中的構(gòu)造操作所得到的元素，均可以由A'中的對(duì)應(yīng)構(gòu)造操作得到．在集合范疇中，可理解為A的元素構(gòu)成了A'的元素的子集，即看成是類型間的一個(gè)自然包含關(guān)系．

定理1［4］給定兩個(gè)函子 F，G: ，(μF，inF)和(μG，inG)分別為相應(yīng)函子的初始F-代數(shù)和初始G-代數(shù)．若存在自然轉(zhuǎn)換 η:F?G，則有唯一射foldF(inG?ημG):μF μG，使得圖 2 中的圖表滿足交換條件．

圖2 初始代數(shù)間的射Fig．2 Morphism between initial algebras

定理1給出了歸納數(shù)據(jù)類型上代數(shù)子類型的初始代數(shù)語義解釋，其中foldF(inG?ημG)就是從子數(shù)據(jù)類型到父數(shù)據(jù)類型的唯一射coerce:μF μG．在子類型研究中，射coerce通常稱為隱式抑制射［10-12］．

例2 參數(shù)化數(shù)組AZList上的初始化操作(znil:1AZList)、插入操作(zcons:A×AZListAZList)和合并操作(zip:AZList×AZListAZList)可抽象地描述為代數(shù)函子 ListG(X)=1+A×X+X×X，且AZList為初始 ListG-代數(shù)，記為 ZListAlg=(AZList，inListG=［znil，zcons，zip］)，其中 znil和 zcons與 AList上的nil和cons相同，zip表示依次將兩個(gè)鏈表中的頭元素取出并構(gòu)成一個(gè)新的鏈表．

圖3 ListAlg到ZListAlg的映射Fig．3 Mapping from ListAlg to ZListAlg

對(duì)于初始ListF-代數(shù)ListAlg和初始ListG-代數(shù)ZListAlg，存在自然轉(zhuǎn)換［in1，in2］:ListF ListG．再由定理1可得到唯一射coerce:AListAZList，使得圖3中的圖表均滿足交換條件，即ListAlg≤AlgZListAlg成立．其中，ini:XiX1+X2+… +Xn是第 i(1≤i≤n)個(gè)分量到其共積的注入射XnXi為ini的逆，用于取出共積中的第i個(gè)分量，且滿足 in-1i?ini=IdXi．由于射 coerce:AListAZList滿足coerce?nil=znil和 coerce?cons=zcons?IdA×coerce，因此有ListAlg≤AlgZListAlg．這意味著 ListAlg中所有由nil和cons所構(gòu)造出來的元素，均可由ZListAlg中的對(duì)應(yīng)znil和zcons構(gòu)造而成．

1．2 共歸納數(shù)據(jù)類型及共代數(shù)子類型

對(duì)偶地，共歸納數(shù)據(jù)類型可表示為共代數(shù)，其中共代數(shù)函子給出了數(shù)據(jù)類型上各種觀察操作的抽象描述．

定義3 給定范疇 和函子B: ，B-共代數(shù)定義為二元組(X，βX:X BX)，其中 X∈ 稱為該B-共代數(shù)的載體或狀態(tài)空間，射βX稱為該B-共代數(shù)的基調(diào)或變遷射．任意兩個(gè)B-共代數(shù)(X，βX)和(Y，βY)間的同態(tài)射f:(X，βX)(Y，βY)是 中的射f:X Y，且滿足 Bf?βX=βY?f．

在范疇論視角下，每個(gè)共歸納數(shù)據(jù)類型恰好是某個(gè)共代數(shù)函子的終結(jié)共代數(shù)，且為共遞歸類型等式的最大不動(dòng)點(diǎn)．

定義4 給定函子 B: ，稱(νB，outB:νB BνB)為終結(jié)B-共代數(shù)，當(dāng)且僅當(dāng)對(duì)任意一個(gè)B-共代數(shù)(X，βX)，存在唯一射 unfoldB(βX):X νB，使得圖4中的圖表滿足交換條件．其中，unfoldB(βX)是由基調(diào)βX所確定的共迭代射，也稱為unfold射［9］或anamorphism［1］．

圖4 終結(jié)共代數(shù)及其唯一射Fig．4 Final coalgebras and its unique morphism

例3 參數(shù)化數(shù)組CList上的觀察操作包括isnil:CList1+1(用于判斷數(shù)組是否為空)、head:CListA(用于給出數(shù)組的當(dāng)前元素)、tail:CListCList(用于給出數(shù)組的剩余部分)、reverse:CListCList(用于對(duì)數(shù)組CList進(jìn)行逆轉(zhuǎn))．這些操作可抽象地描述為共代數(shù)函子ListD(X)=1+A×X+X，且CList為終結(jié) ListD-共代數(shù)，ListCoalg=(CList，outListD=〈isnil，〈head，tail〉，reverse〉)，其中 outListD=(1+(〈head，tail〉+reverse))?isnil?．

對(duì)共歸納數(shù)據(jù)類型來說，共代數(shù)子類型是指父數(shù)據(jù)類型上的行為在子數(shù)據(jù)類型中得到保持，即可理解為兩個(gè)共歸納數(shù)據(jù)類型間存在一個(gè)滿足合適條件的抑制射．例如，若A是B的共代數(shù)子類型，記為A≤CoalgB，則父數(shù)據(jù)類型B上的可觀察行為在子數(shù)據(jù)類型A中得到保持．一方面，B上的所有觀察操作均包含在A中;另一方面，B中元素的可觀察行為均可以由A中對(duì)應(yīng)元素上的觀察操作得到．即共代數(shù)子類型體現(xiàn)了共歸納數(shù)據(jù)類型在觀察操作下的一種行為保持關(guān)系．

定理2［4］給定兩個(gè)函子 B和 D: ，(νB，outB)和(νD，outD)分別為相應(yīng)函子的終結(jié)B-共代數(shù)和D-共代數(shù)．若存在自然轉(zhuǎn)換ρ:D?B，則有唯一射unfoldB(ρνD?outD):νD νB，使得圖 5 中的圖表滿足交換條件．

圖5 終結(jié)共代數(shù)間的射Fig．5 Morphism between final coalgebras

定理2給出了共歸納數(shù)據(jù)類型上共代數(shù)子類型的終結(jié)共代數(shù)語義解釋，其中 unfoldB(ρνD?outD)就是從子數(shù)據(jù)類型到父數(shù)據(jù)類型的抑制射．

給定兩個(gè)共歸納數(shù)據(jù)類型 C1=(νB，outB)和C2=(νD，outD)，若只存在自然轉(zhuǎn)換 ρ:D?B，則稱C1是C2的基調(diào)子類型，強(qiáng)調(diào)方法的重用;若存在自然轉(zhuǎn)換ρ:D?B及抑制射coerce:νD νB，使得圖5中的圖表滿足交換條件，則稱C1是C2的行為子類型［13］，強(qiáng)調(diào)行為的保持及客戶端代碼的重用．在面向?qū)ο笤O(shè)計(jì)原則中，行為子類型構(gòu)成了Liskov替換原則的基礎(chǔ)．

例4 參數(shù)化數(shù)組CZList上的觀察操作zisnil:CZList1+1、zhead:CZListA 和 ztail:CZListCList可表示為共代數(shù)函子 ListB(X)=1+A×X，且CZList為對(duì)應(yīng)的ListB-終結(jié)共代數(shù)，記為ZListCoalg=(CZList，outListB= 〈zisnil，〈zhead，ztail〉〉)，其 中outListB=(1+〈zhead，ztail〉)?zisnil?．

顯然，對(duì)于終結(jié)ListD-共代數(shù)ListCoalg和終結(jié)ListB-共代數(shù) ZListCoalg，存在自然轉(zhuǎn)換〈1，2〉:ListD ListB．再由定理2可得到唯一射 coerce:CListCZList，使圖6中的所有圖表滿足交換條件，即滿足 zisnil?coerce=isnil，zhead ?coerce=head 和ztail?coerce=coerce ?tail，因此ListCoalg≤CoalgZListCoalg成立．即 ZListCoalg中所有由 zisnil和〈zhead，ztail〉操作所觀察得到的行為，均可以由ListCoalg中對(duì)應(yīng)元素上的觀察操作 isnil和〈head，tail〉得到．其中，i:X1×X2×…×XnXi是積到第 i個(gè)分量的投影射:XiX1×X2×… ×Xn為 i的逆，用于將第i個(gè)分量映射到積中的對(duì)應(yīng)位置，且滿足i=

圖6 ListCoalg到ZListCoalg間的映射關(guān)系Fig．6 Mapping relationship between ListCoalg and ZListCoalg

1．3 范疇數(shù)據(jù)類型的雙代數(shù)結(jié)構(gòu)

各種歸納或共歸納數(shù)據(jù)類型通常既包含了可由代數(shù)描述的構(gòu)造操作，也包含了可由共代數(shù)描述的觀察操作，因此文中利用雙代數(shù)給出一種統(tǒng)一的和抽象的描述．

定義5 給定范疇 上的兩個(gè)函子F和B: ，〈F，B〉-雙代數(shù)定義為三元組(X，αX:FX X，βX:X

BX)，其中 αX和 βX分別為同一載體集 X∈ 上的F-代數(shù)和 B-共代數(shù)．任意兩個(gè)〈F，B〉-雙代數(shù)(X，αX，βX)和(Y，αY，βY)間的同態(tài)射是范疇 中的射f:X Y，且滿足 f?αX=αY?Ff和 Bf?βX=βY?f．

在完全偏序范疇中，初始代數(shù)和終結(jié)共代數(shù)上的載體恰好相同，且均為有限的，因此可用一個(gè)載體集同時(shí)表示有限及無限元素．即若范疇 為完全偏序范疇，則函子F: 的初始F-代數(shù)(μF，inF)和終結(jié) F-共代數(shù)(νF，outF)滿足 μF=νF，而 inF和 outF均為同構(gòu)射且互逆．例如，參數(shù)化數(shù)組 AList和CZList上的函子ListF和ListB相同，因此其載體集AList和CZList相同，且 inListF與 outListB互逆，并可構(gòu)成雙代數(shù)(AList，inListF，outListB)或(CZList，inListF，outListB)．

由 Lambek 定理［14］可知，初始代數(shù)(μF，inF)上的基調(diào)inF是同構(gòu)射，其逆in-1F:μF FμF給出了初始代數(shù)載體集上的觀察操作，并構(gòu)成一個(gè)共代數(shù)(μF，in-1F)，即(μF，inF，in-1F)為一個(gè)〈F，F(xiàn)〉-雙代數(shù)．對(duì)偶地，由文獻(xiàn)［15］中的定理9．1可知，終結(jié)共代數(shù)(νB，outB)上的基調(diào)outB是同構(gòu)射，其逆out-1B:BνB νB給出了終結(jié)共代數(shù)載體集上的構(gòu)造操作，并構(gòu)成一個(gè)代數(shù)(νB，out-1B)，即(νB，out-1B，outB)為一個(gè)〈B，B〉-雙代數(shù)．任意的歸納或共歸納數(shù)據(jù)類型均可通過上述方式擴(kuò)展為雙代數(shù)．

例5 利用共代數(shù)函子ListD和ListB可分別將AList和AZList擴(kuò)展為相應(yīng)的〈ListF，ListD〉、〈ListG，ListD〉和〈ListG，ListB〉-雙代數(shù):

類似地，利用代數(shù)函子ListF或ListG可將CList和 CZList擴(kuò)展為相應(yīng)的〈ListF，ListD〉和〈ListF，ListB〉-雙代數(shù):

定義6 范疇數(shù)據(jù)類型T1=(X，αX，βX)和T2=(Y，αY，βY)之間的共積和積合并算子分別定義為

IdF(X+Y)］:F(X+Y)FX+FY，用于分離兩個(gè)代數(shù)構(gòu)造操作中的參數(shù)．例如，對(duì)于代數(shù)函子FX=1+A×X+X ×X，Δ 定義為:Δ(*)=*+* ，Δ(a，x+y)=(a，x)+(a，y)，Δ(x1+y1，x2+y2)=(x1，x2)+(y1，y2)．操作符 :BX×BYB(X×Y)用于合并兩個(gè)觀察結(jié)果．例如，對(duì)于函子BX=1+A×X+X，定義為:(* ，*)=* ，(〈a，x〉，〈a，y〉)=〈a，(x，y)〉，(x，y)=(x，y)．

2 雙代數(shù)中的子類型

2．1 雙代數(shù)中的代數(shù)子類型

定義7 給定兩個(gè)不同的CDT，即T1=(X，φX:GXX，βX:X BX)和 T2=(Y，αY:FY Y，βY:YBY)，若存在自然轉(zhuǎn)換η:F?G和唯一射coerce:X Y，使得圖7中的圖表滿足交換條件，即coerce:X Y 是從(X，αX，βX)到(Y，φY?ηY，βY)的雙代數(shù)同態(tài)射，則稱T1是T2在雙代數(shù)中的代數(shù)子類型，記為T1≤Bia，AlgT2．

圖7 雙代數(shù)中的代數(shù)子類型Fig．7 Algebraic subtype in bialgebras

雙代數(shù)中的代數(shù)子類型是指其中的代數(shù)結(jié)構(gòu)存在子類型關(guān)系，且從子類型到父類型的抑制射為共代數(shù)同態(tài)射．換句話說，子類型中的構(gòu)造在父類型中得到保持，且這些構(gòu)造操作在共代數(shù)觀察操作下不可區(qū)分．

定理3 給定初始〈F，B〉-雙代數(shù)(μF，inF，βμF:μF BμF)和初始〈G，B〉-雙代數(shù)(μG，inG，βμG:μG BμG)，若存在自然轉(zhuǎn)換 η:F?G，則有唯一射f=foldF，B(inG?ημG，βμG):μF μG，使得圖 8 中的圖表滿足交換條件．

圖8 初始雙代數(shù)間的射Fig．8 Morphism between initial bialgebras

證明 由初始雙代數(shù)的初始性可得到唯一射

證畢．

定理3給出了歸納數(shù)據(jù)類型的雙代數(shù)結(jié)構(gòu)中代數(shù)子類型的初始雙代數(shù)語義解釋，其中foldF，B(inG?ημG，βμG)就是從子類型到父類型的抑制射．

例如，對(duì)于AListFDBialg和AZListGDBialg，存在自然轉(zhuǎn)換［in1，in2］:ListF ListG和唯一射 coerce:AListAZList，使得 coerce是從〈ListF，ListD〉-雙代數(shù)(List，inListF，φAList)到(AZList，inListG?［in1，in2］，φAZList)的雙代數(shù)同態(tài)射，且滿足:①isnil?nil=rznil?znil;②head ?cons(a，x)=rzhead ?zcons(a，coerce(x));③coerce ?tail?cons(a，x)=rztail?zcons(a，coerce(x));④coerce ?rev ?cons(a，x)=zrev ?zcons(a，coerce(x))．因此，AListFDBialg≤Bia，AlgAZListGDBialg 成立．

定理4 雙代數(shù)中的代數(shù)子類型≤Bia，Alg關(guān)系滿足自反性和傳遞性:

(1)T≤Bia，AlgT(自反性);

(2)T1≤Bia，AlgT2∧T2≤Bia，AlgT3?T1≤Bia，AlgT3(傳遞性)．

證明 (1)對(duì)任意的范疇數(shù)據(jù)類型T=(X，αX，βX)，均存在標(biāo)識(shí)射IdX:X X和標(biāo)識(shí)自然轉(zhuǎn)換IdF:F?F，且 IdX是從(X，αX，βX)到(X，αX?IdFX，βX)的雙代數(shù)同態(tài)射．

(2)對(duì)任意的范疇數(shù)據(jù)類型 T1=(X，αX，βX)、T2=(Y，φY，βY)和 T3=(Z，δZ，βZ)，由前提可知，存在射f:XY、g:YZ及自然轉(zhuǎn)換η:F?G和 :G?H．由射之間的組合性及自然轉(zhuǎn)換保持射組合的性質(zhì)可知:g ?f:XZ 和 ?η:F H，且 g ?f是從(X，αX，βX)到(Z，δZ?Z?ηZ，βZ)的雙代數(shù)同態(tài)射．再由定義 7可知 T1≤Bia，AlgT3成立．證畢．

定理5 對(duì)于范疇數(shù)據(jù)類型T1=(X，αX，βX)、T2=(Y，αY，βY)和 T3=(Z，φZ，βZ)，若滿足T1≤Bia，AlgT3和 T2≤Bia，AlgT3，則有 T1⊕T2≤Bia，AlgT3．

證明 由前提可知，存在射f:X Z、g:Y Z和自然轉(zhuǎn)換η:F?G．利用共積可得到唯一射［f，g］:X+Y Z．再由自然轉(zhuǎn)換保持射的性質(zhì)可知，［f，g］是從(X+Y，αX⊕Y，βX⊕Y)到(Z，φZ?ηZ，βY)的雙代數(shù)同態(tài)射．因此，由定義 7 可知 T1⊕T2≤Bia，AlgT3成立．證畢．

2．2 共代數(shù)子類型

定義8 給定兩個(gè) CDT，即 T1=(X，αX，φX)和T2=(Y，αY，βY)，若存在自然轉(zhuǎn)換 ρ:D?B 和唯一射coerce:X Y，使得圖9中的圖表滿足交換條件，即coerce:X Y 是從(X，αX，ρX?φX)到(Y，αY，βY)的雙代數(shù)同態(tài)射，則稱T1是T2在雙代數(shù)中的共代數(shù)子類型，記為 T1≤Bia，CoalgT2．

雙代數(shù)中的共代數(shù)子類型是指其中的共代數(shù)結(jié)構(gòu)存在子類型關(guān)系，并且從子類型到父類型的抑制射為代數(shù)同態(tài)射．換句話說，雙代數(shù)中的共代數(shù)子類型是指在保持?jǐn)?shù)據(jù)類型上的構(gòu)造操作不變的前提下，父類型中的行為在子類型中得到保持．

定理 6 給定終結(jié)〈F，B〉-雙代數(shù)(νB，ανB，outB)和終結(jié)〈F，D〉-雙代數(shù)(νD，ανD，outD)，若存在自然轉(zhuǎn)換 ρ:D?B，則有射 f=unfoldF，B(ανD，ρνD?outνD):νD νB，使得圖10中的圖表滿足交換條件．

圖9 雙代數(shù)中的共代數(shù)子類型Fig．9 Coalgebraic subtype in bialgebras

圖10 終結(jié)雙代數(shù)間的射Fig．10 Morphism between final bialgebras

證明 由終結(jié)雙代數(shù)的終結(jié)性可得到

證畢．

定理6給出了共歸納數(shù)據(jù)類型的雙代數(shù)結(jié)構(gòu)中共代數(shù)子類型的終結(jié)雙代數(shù)語義解釋，unfoldF，B(ανD，ρνD?outνD)就是從子數(shù)據(jù)類型到父數(shù)據(jù)類型的抑制射．

例如，對(duì)于CListFDBialg和CZListFBBialg，存在自然轉(zhuǎn)換〈1，2〉:ListD ListB和唯一射 coerce:CZListCList，使得 coerce 是從〈ListF，ListB〉-雙代數(shù)(CList，αCList，〈1，2〉?outListD)到(CZList，αCZList，outListB)的雙代數(shù)同態(tài)射，且滿足:①isnil?rnil=zisnil?rznil;②head ?rcons(a，x)=zhead ?rzcons(a，coerce(x));③coerce ?tail?rcons(a，x)=ztail?rzcons(a，coerce(x))．因此，CListFDBialg≤Bia，CoalgCZListBialg 成立．

定理7 雙代數(shù)中的共代數(shù)子類型滿足自反性和傳遞性:

(1)T≤Bia，CoalgT(自反性);

(2)T1≤Bia，CoalgT2∧T2≤Bia，CoalgT3?T1≤Bia，CoalgT3(傳遞性)．

證明 (1)由標(biāo)識(shí)射為雙代數(shù)同態(tài)射及標(biāo)識(shí)自然轉(zhuǎn)換的性質(zhì)可得T≤Bia，CoalgT．

(2)對(duì)于任意的范疇數(shù)據(jù)類型T1=(X，αX，βX)、T2=(Y，αY，φY)和 T3=(Z，αZ，σZ)，由前提可知，存在射f:XY和g:YZ，以及自然轉(zhuǎn)換 ρ:E?D和θ:D?B．由射之間的組合性及自然轉(zhuǎn)換保持射組合的性質(zhì)可知，g?f:X Z 和 θ?ρ:E?B，且 g ?f是從(X，αX，θX?ρX?βX)到(Z，αZ，βZ)的雙代數(shù)同態(tài)射．再由定義8可知 T1≤Bia，CoalgT3成立．證畢．

定理8 對(duì)于范疇數(shù)據(jù)類型T1=(X，αX，φX:X DX)、T2=(Y，αY，βY:Y BY)和 T3=(Z，αZ，βZ:Z

BZ)，若 滿 足 T1≤Bia，CoalgT2和 T1≤Bia，CoalgT3，則 有T1≤Bia，CoalgT2?T3．

證明 由前提可知，存在射f:X Y、g:X Z和自然轉(zhuǎn)換 ρ:D?B．利用積可得到唯一射〈f，g〉:X Y×Z．再由射之間的組合性及自然轉(zhuǎn)換保持射組合的性質(zhì)可知，〈f，g〉是從(X，αX，ρX?σX)到(Y ×Z，αY?Z，βY?Z)的雙代數(shù)同態(tài)射．因此，T1≤Bia，CoalgT2?T3成立．證畢．

3 結(jié)語

將子類型引入到基于雙代數(shù)的CDT中，一方面可以為研究歸納數(shù)據(jù)類型間的代數(shù)子類型和共歸納數(shù)據(jù)類型間的共代數(shù)子類型提供一個(gè)統(tǒng)一的數(shù)學(xué)理論框架，更好地探討包含構(gòu)造操作和觀察操作的數(shù)據(jù)類型之間的關(guān)系及性質(zhì)，從而促進(jìn)CDT在函數(shù)式程序語言和泛化編程等領(lǐng)域中的應(yīng)用;另一方面可以從范疇論的角度給出子類型的數(shù)學(xué)定義和語義解釋．今后將研究如何將子類型擴(kuò)展到其他各種CDT(如嵌套或依賴數(shù)據(jù)類型)上，并探討子類型與繼承之間的關(guān)系及性質(zhì)．

［1］Meijer E，F(xiàn)okkinga M，Paterson R．Functional programming with bananas，lenses，envelopes and barbed wire［C］∥Hughes J．Functional Programming Languages and Computer Architecture．New York:Springer-Verlag，1991:124-144．

［2］蘇錦鈿，余珊珊．程序語言中的共歸納數(shù)據(jù)類型及其應(yīng)用 ［J］．計(jì)算機(jī)科學(xué)，2011，38(11):114-118．Su Jin-dian，Yu Shan-shan．Coinductive data types and their applications in programming languages［J］．Computer Science，2011，38(11):114-118．

［3］蘇錦鈿，余珊珊．共歸納數(shù)據(jù)類型上的共遞歸操作及其計(jì)算定律［J］．華南理工大學(xué)學(xué)報(bào):自然科學(xué)版，2011，39(10):90-95．Su Jin-dian，Yu Shan-shan．Corecursion operations and its calculation laws on coinductive data types［J］．Journal of South China University of Technology:Natural Science Edition，2011，39(10):90-95．

［4］Poll E．Subtyping and inheritance for inductive types［C］∥Proceedings of TYPES＇97 Workshop on Subtyping，Inheritance and Modular Development of Proofs．Durham:University of Durham，1997:1-10．

［5］Erwig M．Metamorphic programming:structured recursion for abstract data types［R］．Hagen:Computer Science Department，F(xiàn)ern University，1998:20-30．

［6］Nogueira P，Moreno-Navarro J J．Bialgebra views:a way for polytypic programming to cohabit with data abstraction［C］∥Proceedings of the ACM SIGPLAN Workshop on Generic Programming．New York:ACM，2008:61-73．

［7］蘇錦鈿，余珊珊．抽象數(shù)據(jù)類型的雙代數(shù)結(jié)構(gòu)［J］．華南理工大學(xué)學(xué)報(bào):自然科學(xué)版，2011，39(12):1-7．Su Jin-dian，Yu Shan-shan．Bialgebraic structure of abstract data types［J］．Journal of South China University of Technology:Natural Science Edition，2011，39(12):1-7．

［8］蘇錦鈿，余珊珊．抽象數(shù)據(jù)類型的雙代數(shù)結(jié)構(gòu)及其計(jì)算定律［J］．計(jì)算機(jī)研究與發(fā)展，2012，49(8):1787-1803．Su Jin-dian，Yu Shan-shan．Bialgebraic structures for abstract data types and their computations［J］．Journal of Computer Research and Development，2012，49(8):1787-1803．

［9］Gibbons J，Hutton G，Altenkirch T．When is a function a fold or an unfold?［J］．Electronic Notes in Theoretical Computer Science，2001，44(1):146-160．

［10］Luo Z．Coercive subtyping ［J］．Journal of Logic and Computation，1999，9(1):105-130．

［11］Luo Z．Coercive subtyping in type theory［C］∥Proceedings of the 1996 Annual Conference of the European Association for Computer Science Logic．London:Springer-Verlag，1996:276-296．

［12］Xue T．Theory and implementation of coercive subtyping［D］．Royal Holloway:Department of Computer Science，University of London，2013．

［13］Poll E．A coalgebraic semantics of subtyping［J］．Theoretical Informatics and Applications，2001，35(11):61-81．

［14］Lambek J．A fixpoint theorem for complete categories［J］．Mathematische Zeitschrift，1968，103:151-161．

［15］Rutten J J M M．Universal coalgebra:a theory of systems［J］．Theoretical Computer Science，2000，249(1):56-58．