抽象數(shù)據(jù)類型的雙代數(shù)結構*

蘇錦鈿 余珊珊

(1.華南理工大學計算機科學與工程學院，廣東廣州510006;2.中山大學信息科學與技術學院，廣東廣州510275)

傳統(tǒng)的抽象數(shù)據(jù)類型(ADT)以歸納數(shù)據(jù)類型為主，側重于數(shù)據(jù)類型的有限語法構造，一般包含一些稱為“構造子”的操作，有限分支樹、數(shù)組、隊列、堆棧、自然數(shù)等都是典型的歸納數(shù)據(jù)類型.在范疇論的視角下，每個歸納數(shù)據(jù)類型都可以抽象地描述為某個代數(shù)函子下的初始代數(shù)，其中代數(shù)函子對應該數(shù)據(jù)類型的構造操作，因此，歸納數(shù)據(jù)類型也常被稱為代數(shù)數(shù)據(jù)類型［1-2］.由初始代數(shù)的初始性可得到歸納數(shù)據(jù)類型上的一個遞歸操作，稱為Fold射［3］.該操作滿足一系列的代數(shù)計算定律，在程序的計算及轉換研究中具有重要的作用.

共歸納數(shù)據(jù)類型［4］也稱為共代數(shù)數(shù)據(jù)類型［5］或共數(shù)據(jù)類型［6］，可看作是歸納數(shù)據(jù)類型的范疇對偶概念，無限分支樹、無限鏈表和流等都是典型的共歸納數(shù)據(jù)類型.與歸納數(shù)據(jù)類型不同，共歸納數(shù)據(jù)類型側重于數(shù)據(jù)類型在計算過程中所展現(xiàn)出來的動態(tài)行為.在范疇論的視角下，這一類數(shù)據(jù)類型可進一步抽象為某個共代數(shù)函子下的終結共代數(shù)，其中共代數(shù)函子對應該數(shù)據(jù)類型上的觀察操作.由終結共代數(shù)的終結性可得到共歸納數(shù)據(jù)類型上的一個共遞歸操作，稱為Unfold射［7］.該操作滿足一系列的共代數(shù)計算定律，在基于行為特征的函數(shù)定義和程序推理及轉換過程中具有重要的作用［6，8］.

對許多ADT(例如流、鏈表、堆棧和樹等)來說，除了本身包含可由代數(shù)進行描述的語法構造特征外，同時還包含可由共代數(shù)進行描述的動態(tài)行為特征，即同時具有歸納和共歸納數(shù)據(jù)類型的特點.因此，單純利用代數(shù)或共代數(shù)只能刻畫其中某一方面的特征.

代數(shù)和共代數(shù)本質上都可看成是集合及其上滿足一定性質的操作.從范疇論的角度看，兩者之間存在共同點，可以通過某種合適的關系融合在一起.基于上述考慮，Rutten等［9］提出了雙代數(shù)作為代數(shù)與共代數(shù)的一種融合，其中代數(shù)函子給出基集元素的構造方法，刻畫了系統(tǒng)的語法構造特征，而共代數(shù)函子給出基集元素的行為變遷結構，刻畫了系統(tǒng)的動態(tài)行為語義.目前，雙代數(shù)主要應用于程序語言的操作語義與指稱語義研究中［10-11］，被證明是研究狀態(tài)系統(tǒng)靜態(tài)結構與動態(tài)行為的性質及兩者間關系的一種可行途徑.

許多ADT都可以看成是一個典型的雙代數(shù)結構:ADT上的語法構造操作可以表示成某個代數(shù)函子下的基調，這是典型的代數(shù)結構;而ADT在計算過程中所展現(xiàn)出來的動態(tài)行為可以表示為某個共代數(shù)函子下的行為變遷結構，這是典型的共代數(shù)結構.代數(shù)和共代數(shù)函子間通過稱為分配律的自然轉換有機地聯(lián)系起來.這種分配律一方面給出構造操作與產生合適行為之間的關系，另一方面可通過函子化提升分別研究遞歸函數(shù)與共代數(shù)結構、共遞歸函數(shù)與代數(shù)結構的性質及兩者間的關系，從而擴展了代數(shù)中的歸納原理和共代數(shù)中的共歸納原理.

Erwig［12-13］指出ADT可以表示成雙代數(shù)結構，并探討了以共代數(shù)函子為參數(shù)的遞歸操作，從而提出一種 Metamorphic編程風格.Nogueira等［14］也指出ADT可以表示成雙代數(shù)結構，并探討了ADT的雙代數(shù)結構在多態(tài)編程中的應用.但 Erwig和Nogueira等均沒指出如何分析ADT上的語法構造和動態(tài)行為的性質及兩者間的關系，也沒有說明如何利用函子化提升研究遞歸和共遞歸函數(shù).

相對于上述研究，文中利用雙代數(shù)研究ADT上的語法構造和動態(tài)行為之間的關系，給出了ADT的一種雙代數(shù)結構，并說明了如何通過分配律對共代數(shù)和代數(shù)函子進行提升，從而將共代數(shù)結構(或代數(shù)結構)融入到遞歸(或共遞歸)函數(shù)的定義及計算中，進一步擴展了代數(shù)中的歸納原理和共代數(shù)中的共歸納原理，提高了程序語言對ADT中各種性質的描述與證明能力.

1 抽象數(shù)據(jù)類型的雙代數(shù)結構

雙代數(shù)是同一載體集上的代數(shù)和共代數(shù)對，其定義如下.

定義1 給定范疇C上的兩個自函子F和B，一個〈F，B〉-雙代數(shù)為一個三元組(X，αX，βX)，其中X為載體集，αX:FX→X和βX:X→BX分別為同一載體集X上的F-代數(shù)結構和B-共代數(shù)結構:

兩個〈F，B〉-雙代數(shù)(X，αX，βX)和(Y，αY，βY)之間的同態(tài)射是一個射f:X→Y，且滿足圖1中的圖表交換.

圖1 雙代數(shù)同態(tài)射Fig.1 Homomorphism between bialgebras

因此，雙代數(shù)同態(tài)射可以看成同時為對應的F-代數(shù)和B-共代數(shù)之間的同態(tài)射.范疇C上所有的〈F，B〉-雙代數(shù)及其同態(tài)射可構成一個范疇，記為C(F，B).

〈F，B〉-雙代數(shù)給出了同一個基集上的代數(shù)操作和共代數(shù)行為變遷結構，但沒有說明兩者間的變換關系，因此無法直接用于描述ADT.下面進一步給出λ-雙代數(shù)的定義.

定義2 設F和B分別為代數(shù)函子和共代數(shù)函子.則F對B的一個分配律為一個自然轉換λ:FB?BF.雙代數(shù)上的分配律λ簡稱為λ-雙代數(shù)，是一個〈F，B〉-雙代數(shù)(X，αX，βX)，且滿足圖 2 中的圖表交換.

圖2 λ-雙代數(shù)Fig.2 λ-bialgebras

包含所有λ-雙代數(shù)的范疇構成了范疇C(F，B)的一個完全子范疇，記為Cλ(F，B).Cλ(F，B)具有一些重要的性質，例如在合適的條件下每一個λ-雙代數(shù)上的互相似是同余關系，因此其初始語義與終結語義是一致的［9］.

根據(jù)圖2中的圖表交換，λ-雙代數(shù)通過分配律將雙代數(shù)結構中的代數(shù)運算和共代數(shù)行為變遷有機地融合在一起.即一方面代數(shù)上的構造操作是具有良行為的操作，另一方面共代數(shù)上的行為變遷在這些構造操作下被保持.

下面給出一些典型的ADT的雙代數(shù)結構.

例1 實數(shù)流 R∞上的前綴操作 scons:R×X→X表示將一個實數(shù)作為前綴添加到一個流中，加法操作⊕:X×X→X和乘法操作?:X×X→X分別表示將兩個流中對應位置的元素相加或相乘后構成一個新的流.上述構造操作可表示為一個代數(shù)結構:(X，αX=［scons，⊕，?］:R ×X+X×X+X×X→X).

對實數(shù)流中的元素進行觀察的操作包括:value:X→R用于得到流當前狀態(tài)上的實數(shù)，next:X→X用于讓流進行下一個狀態(tài).上述觀察操作可表示為一個共代數(shù)結構(X，βX=〈value，next〉:X→R ×X).

因此，實數(shù)流R∞可描述成一個雙代數(shù)結構:(X，αX:R×X+X×X+X×X→X，βX:X→R×X).

例2 參數(shù)化鏈表List［A］(A是某個已知數(shù)據(jù)類型)上的空鏈表nil:1→X和插入操作cons:A×X→X為構造子，用于構造所有的有限鏈表，合并操作zip:X×X→X用于依次將兩個鏈表中的頭元素取出后合并成一個新的鏈表.上述構造操作可表示為一個代數(shù)結構:(X，αX=［nil，cons，zip］:1+A×X+X×X→X).

觀察操作head:X→A+1和tail:X→X+1分別給出了鏈表中的頭元素及除頭元素外的剩余部分;若鏈表為空，則返回*∈1.上述觀察操作可表示為一個共代數(shù)結構(X，βX=〈head，tail〉:X→A×X+1).

因此，鏈表List［A］可描述成一個雙代數(shù)結構:(X，αX:1+A×X+X×X→X，βX:X→A×X+1).

雙代數(shù)同態(tài)射f:A→E用于將鏈表List［A］中的元素類型由A轉換為E，并且在轉換的過程中保持代數(shù)及共代數(shù)操作.

類似地，對于樹、堆棧、隊列或集合等其它ADT，也可以建立相應的雙代數(shù)結構.事實上，程序語言中任意的歸納或共歸納數(shù)據(jù)類型都可以通過適當?shù)臄U展構成一個雙代數(shù)結構.

例如，由集合范疇Set上的類型構造子FX=1+X的初始代數(shù)可以得到歸納數(shù)據(jù)類型N(表示自然數(shù))，基調inF=［zero，succ］包括了初始化操作zero:1→N和后繼操作 succ:N→N.逆=〈iszero，pred〉給出了自然數(shù)上的觀察操作，其中iszero:N→1表示自然數(shù)為0，而pred:N→N給出了某個非零自然數(shù)的前驅.因此，(N，inF=［zero，succ］，=〈iszero，pred〉)就是自然數(shù)N上的一個雙代數(shù)結構.由集合范疇Set上的自函子BX=R×X的終結共代數(shù)可以得到共歸納數(shù)據(jù)類型中的實數(shù)流R∞的定義，基調outB=〈value，next〉分別給出實數(shù)流的當前值及后繼狀態(tài).逆=［scons］為實數(shù)流上的一個構造操作.因此，(R∞=［scons］，outB=〈value，next〉)就是實數(shù)流上的一個雙代數(shù)結構.

給定 ADT 的一個λ-雙代數(shù)結構(X，αX，βX)，可以進一步利用分配律λ:FB?BF刻畫X上的語法構造和動態(tài)行為之間的轉換關系.

例3 分配律λ:FB?BF自然地描述了鏈表List［A］(記為A*)上的語法構造與動態(tài)行為之間的關系.例如，對cons操作來說，下面的交換圖(圖3)給出了鏈表變量［2，1，0］上的構造和觀察之間的變換關系，其中Id為標識函子.

圖3 鏈表上的λ分配律例子Fig.3 An example ofλ-distributive law on lists

假設σ不為空，且σ=a'·σ'(σ，σ'∈A*;a，a'∈A)，則鏈表上的 cons與〈head，tail〉之間的轉換關系為

式(1)和(2)的結果是相同的，即當利用cons操作在鏈表σ中插入一個元素a后，可以采用以下兩種方式:

(1)先利用cons將一個元素a插入到現(xiàn)有的鏈表σ中，然后再通過head和tail對其進行觀察并得到結果a×σ;

(2)在保持cons操作的代數(shù)結構的前提下利用head和tail對σ進行觀察得到(a，a'×σ')，接著通過λ分配律將(a，a'×σ')轉換成〈head，tail〉((a，σ))，最后在保持共代數(shù)行為變遷結構的前提下利用cons得到a×σ.

這兩種方式所得到的結果都是一樣的，即先構造后觀察與先觀察后轉換再構造的結果是相同的，并且這兩種方式與鏈表中所包含的元素的實際類型無關，即體現(xiàn)了λ的自然性特點.

2 分配律與函子化提升

2.1 共代數(shù)函子提升

給定一個 ADT 的λ-雙代數(shù)結構(X，αX，βX)，利用分配律λ:FB?BF可對共代數(shù)函子B進行函子化提升.

定義3 由分配律λ:FB?BF可定義一個共代數(shù)函子Bλ，將B:C→C提升為Bλ:CF→CF，使得對任意一個F-代數(shù)(X，αX)有Bλ(X，αX)=(BX，BαX?λ X:FBX→BX)，對任意一個代數(shù)同態(tài)射h:(X，αX)→(Y，αY)有Bλh=Bh.

由文獻［15］中的定理15.3 可知Bλ是(BX，BαX?λX)和(BY，BαY?λY)間的代數(shù)同態(tài)射，因此這種提升是函子化的.Bλ相當于把文獻［16］中的λ提升作用于共代數(shù)函子B:將X提升為BλX=BX，將αX提升為BλαX=BαX?λX.載體集BX是以X中的元素為參數(shù)變量、以B中的基調為觀察操作所得到的行為變遷結構，而分配律λ則說明了如何在給定變量X的F-代數(shù)結構的前提下為其行為結構BX中的元素添加相應的F-代數(shù)結構.

每一個提升后的代數(shù)Bλ(X，αX)給出了變量X的共代數(shù)行為變遷結構上的F-代數(shù)結構，且存在從初始代數(shù)(μF，inF)到Bλ(X，αX)的唯一射其中μF是初始代數(shù)的載體，且為基調inF上的最小不動點.使得等式?inF=BλαX?F成立，即滿足圖4所示的圖表交換.

圖4 初始代數(shù)到BλαX的Fold射Fig.4 Fold morphisms from initial algebras to BλαX

定理1 上述的λ-Fold射滿足

證明 由Fold射及函子化提升的性質可知圖4中的各個圖表均滿足交換，因此和均為從初始代數(shù)(μF，inF)到Bλ(X，αX)的Fold射.再由Fold射的唯一性可知有

例4 函數(shù)double:A*→A*將鏈表中的每個元素分別乘以2后構成一個新的鏈表，即對于σ，r∈A*和a∈A，double定義如下:

double(nil)=dnil=［］，

double(cons(a，σ))=dcons(a，double(σ))=

cons(a×2，double(σ))=a×2:double(σ)，

double(zip(σ，r))=dzip(double(σ)，double(r))=

cons(2 ×head(σ)，double(zip(r，tail(σ))))=

2 ×head(σ):double(zip(r，tail(σ))).

顯然，double 是初始代數(shù)(A*，［nil，cons，zip］)與代數(shù)(A*，［dnil，dcons，dzip］)間的一個 Fold 射

利用分配律λ可將(A*，α=［dnil，dcons，dzip］)提升為Bλ(A*，α)=(BA*，Bλα)，其中Bλα=［nl，cs，zp］，從而得到λ-Fold 射如圖5所示.

圖5 鏈表上的λ-Fold射例子Fig.5 An example ofλ-Fold morphisms on lists

f定義如下:

f(nil)=nl=［］，

f(cons(a，σ))=nl(a，f(σ))=〈2 ×a，f(σ)〉，f(zip(σ，r))=zp(f(σ)，f(r))=

〈2 ×head(σ)，f(zip(r，tail(σ)))〉.

上述的λ-Fold射f遞歸地給出了鏈表σ在函數(shù)double作用下所得到的像的共代數(shù)行為變遷結構，從而將一般的Fold射擴展到共代數(shù)行為變遷結構上.

對于初始代數(shù)(μF，inF)，利用λ可將其提升為Bλ(μF，inF)=(BμF，BλinF=BinF?λμF:FBμF→BμF)，且存在λ-Fold 射如圖6所示.

圖6 初始代數(shù)到BλinF的Fold射Fig.6 Fold morphisms from initial algebras to BλinF

證明 由λ-雙代數(shù)及函子化提升的性質可知圖7的各個圖表均滿足交換.對于任意的(X，αX)及Fold射由文獻［15］中的定理15.3可知是從(BμF，BλinF)到(BX，BλαX)的代數(shù)同態(tài)射和均為從(μF，inF)到(BX，BλαX)的λ-Fold射，由其唯一性有因此是μF上的一個B-共代數(shù)結構與(X，βX)間的共代數(shù)同態(tài)射，而且(μF，為初始B-共代數(shù).再由文獻［17］中的定理3.2.3可知為(μF，inF)上唯一的共代數(shù)結構，且為初始λ-雙代數(shù).

圖7 初始代數(shù)的λ-提升Fig.7 λ-lifting of initial algebras

上述定理給出了一種利用分配律λ:FB?BF及Fold射構造初始代數(shù)上的共代數(shù)結構的方法，從而將初始代數(shù)提升為相應的初始λ-雙代數(shù).

2.2 代數(shù)函子提升

利用分配律可以將具有共代數(shù)行為變遷結構的變量提升為以該變量為參數(shù)的代數(shù)項上的共代數(shù)結構.

定義4 由分配律λ:FB?BF可定義一個代數(shù)函子Fλ，將F:C→C提升為Fλ:CB→CB，使得:對于任意一個共代數(shù)(X，βX)有Fλ(X，βX)=(FX，λX?FβX:FX→BFX)，對于任意一個共代數(shù)同態(tài)射h:(X，βX)→(Y，βY)有Fλh=Fh.

容易驗證Fh是共代數(shù)(FX，λX?FβX)和(FY，λY?FλY)間的同態(tài)射［15］，而Fλ可看成是對代數(shù)函子F的一種λ提升［16］:將X提升為FλX=FX，將βX提升為FλβX=λX?FβX，將h:(X，βX)→(Y，βY)提升為Fλh=Fh:(FX，F(xiàn)λβX)→(FY，F(xiàn)λβY).顯然，這種提升是函子化的.FX中的元素是以參數(shù)X中的元素為變量，以F中的方法為構造操作所得到的代數(shù)項，且X具有B-共代數(shù)結構.而分配律λX說明了如何在給定參數(shù)X的共代數(shù)行為變遷結構的前提下對FX中的元素指派相應的共代數(shù)行為變遷結構.

每一個提升后的共代數(shù)Fλ(X，βX)給出了代數(shù)項上的共代數(shù)行為變遷結構，且存在到終結共代數(shù)(vB，outB)的唯一射[FλβX]B，其中vB為終結共代數(shù)上的載體，且為基調outB上的最大不動點.[FλβX]B使得等式 outB?[FλβX]B=B[FλβX]B?FλβX成立，即滿足圖8中的圖表交換.

[FλβX]B是由基調FλβX所確定的一個 Unfold射，稱為λ-Unfold射.

定理3 上述λ-Unfold 射滿足[FλβX]B=[βX]B?αX.

證明 顯然，[FλβX]B和[βX]B?αX均為從共代數(shù)(FX，F(xiàn)λβX)到終結共代數(shù)(vB，outB)的λ-Unfold 射，由其唯一性可證上述等式成立.

例5 利用分配律λ可將實數(shù)流共代數(shù)(X，βX:X→R ×X)提升為(FX，F(xiàn)λβX=λX?FβX:FX→BFX)(見圖9).對實數(shù)流上的代數(shù)項(σ⊕r)?w，(其中σ，r，w∈R∞)，λ-Unfold 射f=[FλβX]B的定義如下:

圖9 實數(shù)流共代數(shù)的λ-提升Fig.9 λ-lifting of stream coalgebras for real numbers

λ-Unfold射[FλβX]B給出了代數(shù)項與該項在共代數(shù)函子下的全局行為之間的映射關系，從而將定義在變量X上的一般Unfold操作擴展到以該變量X為參數(shù)的代數(shù)項上，并從行為觀察的角度給出了代數(shù)項的全局行為的共遞歸定義.

由λ-Unfold射的唯一性及終結共代數(shù)上的互模擬是等價關系的性質可以得到一種基于共歸納原理的證明代數(shù)項相等的方法:即要證明項代數(shù)FX中的任意兩個元素是相等的，只需證明它們在[FλβX]B的作用下映射到終結代數(shù)中的同一狀態(tài)上.這實際上是將一般變量X上的共歸納證明原則擴展到以該變量為參數(shù)的代數(shù)項上，從而為代數(shù)項的相等性提供了一種基于行為觀察的證明方法，并擴展了共代數(shù)中的共歸納原理，同時與傳統(tǒng)的基于歸納原理的證明方法形成互補.

例6 要證明實數(shù)流上的操作⊕滿足對?的分配律，即?σ，r，w∈R∞.(σ⊕r)?w=(σ?w)⊕(r?w)，由終結共代數(shù)上的互模擬是等價關系的性質可知，只需證明存在某個合適的互模擬關系S=σ，r，w∈R∞}?R∞×R∞，使得:

由⊕和?的定義有:

由假設可知((next(σ)⊕next(r))?next(w)，(next(σ)?next(w))⊕(next(r)?next(w)))∈S成立，即S是一個共代數(shù)互模擬，因此有(σ⊕r)?w=(σ?w)⊕(r?w).

對于終結共代數(shù)(vB，outB)，利用λ可將其提升為Fλ(vB，outB)=(FvB，F(xiàn)λoutB=λvB?FoutB:FvB→BFvB)，且存在到終結共代數(shù)(vB，outB)的λ-Unfold射[FλoutB]B:FvB→vB，如圖10 所示.

圖10 終結共代數(shù)的λ-提升及λ-Unfold射Fig.10 λ-lifting andλ-Unfold morphisms of final coalgebras

定理4λ-Unfold射[FλoutB]B:FvB→vB是終結共代數(shù)(vB，outB)上的一個F-代數(shù)結構，且(vB，[FλoutB]B，outB)為一個λ-雙代數(shù)，且為終結λ-雙代數(shù)，而(vB，[FλoutB]B)為一個終結F-代數(shù).

證明 由定理3的對偶性及圖11的圖表交換可容易證明.

圖11 FλβX到終結共代數(shù)的唯一射Fig.11 Unique morphism from FλβXto final coalgebras

上述定理給出了一種利用分配律λ:FB?BF及Unfold射構造終結共代數(shù)上的代數(shù)結構的方法，從而將終結共代數(shù)提升為終結λ-雙代數(shù).

3 結語

文中利用λ-雙代數(shù)給出ADT的一種抽象描述，并分析其語法構造和動態(tài)行為的性質及兩者間的關系.在此基礎上，進一步利用分配律分別對共代數(shù)和代數(shù)函子進行函子化提升，給出一種構造初始代數(shù)(或終結共代數(shù))上的共代數(shù)(或代數(shù))結構，并將其提升為初始(或終結)λ-雙代數(shù)的方法，從而擴展了代數(shù)中的歸納原理和共代數(shù)中的共歸納原理，并提高了程序語言對ADT中各種性質的描述與證明能力.

在下一步工作中，筆者將繼續(xù)研究ADT上的其它遞歸(如原始遞歸、Course-of-Value迭代)和共遞歸(如原始共遞歸、Course-of-Value共迭代)函數(shù)，并探討ADT上存在合適分配律的前提條件及其規(guī)范格式.

［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.Berlin:Springer，1991:215-240.

［2］Malcolm G.Algebraic types and program transformation［D］.Groningen:Department of Computing Science，University of Groningen，1990:1-50.

［3］Bird R.Introduction to functional programming using Haskell［M］.2nd ed.London:Prentice-Hall，1998.

［4］蘇錦鈿，余珊珊.共歸納數(shù)據(jù)類型上的共遞歸操作及其計算定律［J］.華南理工大學學報:自然科學版，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.

［5］Hensel U，Jacobs B.Coalgebraic theories of sequences in PVS ［J］.Journal of Logic and Computation，1999，9(4):463-500.

［6］Hinze R.Reasoning about codata［C］∥Horváth Z，Plasmeijer R，Zsók V.Central European Functional Programming School(CEFP 2009).Berlin:Springer，2010:42-93.

［7］Hutton G.Fold and unfold for program semantics［C］∥Proceeding of 3rd ACM SIGPLAN International Conference on Functional Programming.New York:ACM Press，1998:280-288.

［8］Vene V，Uustalu T.Functional programming with apomorphisms(corecursion) ［J］.Proceedings of the Estonian Academy of Science:Physics，Mathematics，1998，47(3):147-161.

［9］Rutten J J M M，Turi D.Initial algebra and final coalgebra semantics for concurrency［C］∥Proceedings of REX School/Symposium.Berlin:Springer，1993:477-530.

［10］Turi D.Functorial operational semantics and its denotational dual［D］.Amsterdam:Department of Computer Science，F(xiàn)ree University，1996:1-227.

［11］Turi D，Plotkin G D.Towards a mathematical operation semantics［C］∥Proceedings of 12th Symposium on Logic in Computer Science.Washington:IEEE，1997:280-291.

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

［13］Erwig M.Categorical programming with abstract data types［C］∥7th International Conference on Algebraic Methodology and Software Technology.Berlin:Springer，1998:406-421.

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

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

［16］Bartels F.Generalised coinduction［J］.Electronic Notes in Theoretical Computer Science，2001，44(1):67-87.

［17］Bartels F.On generalised coinduction and probabilistic specification formats:distribute laws in coalgebraic modeling［D］.Amsterdam:Department of Computer Science，F(xiàn)ree University，2004:42-43.