共歸納數(shù)據(jù)類(lèi)型上的共遞歸操作及其計(jì)算定律*

蘇錦鈿 余珊珊

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

歸納數(shù)據(jù)類(lèi)型是類(lèi)型理論的一個(gè)重要組成部分和研究重點(diǎn).程序語(yǔ)言中的有限分支樹(shù)、數(shù)組、隊(duì)列、堆棧和自然數(shù)等都是典型的歸納數(shù)據(jù)類(lèi)型.這一類(lèi)數(shù)據(jù)類(lèi)型的語(yǔ)法構(gòu)造可以通過(guò)一些稱(chēng)為“構(gòu)造子”的操作進(jìn)行歸納地描述.從代數(shù)的角度來(lái)看，每一個(gè)歸納數(shù)據(jù)類(lèi)型可以看成是某個(gè)代數(shù)函子下的一個(gè)初始代數(shù)，其中代數(shù)函子對(duì)應(yīng)著該數(shù)據(jù)類(lèi)型的構(gòu)造操作.由初始代數(shù)的初始性可定義歸納數(shù)據(jù)類(lèi)型上的一個(gè)遞歸操作，稱(chēng)為折疊操作［1］或 catamorphism［2］，且該操作滿(mǎn)足一系列的代數(shù)計(jì)算定律.遞歸操作及其計(jì)算定律在程序的計(jì)算及轉(zhuǎn)換研究中具有非常重要的作用［3-4］.

共歸納數(shù)據(jù)類(lèi)型［5］也稱(chēng)為共代數(shù)數(shù)據(jù)類(lèi)型［6］或共數(shù)據(jù)類(lèi)型［7-8］，是近十幾年來(lái)類(lèi)型理論中研究數(shù)據(jù)類(lèi)型的一種新思路，可看作是歸納數(shù)據(jù)類(lèi)型的范疇對(duì)偶概念.與歸納數(shù)據(jù)類(lèi)型不同，共歸納數(shù)據(jù)類(lèi)型側(cè)重于研究數(shù)據(jù)類(lèi)型在運(yùn)行過(guò)程中所展現(xiàn)出來(lái)的(特別是無(wú)限)動(dòng)態(tài)行為，例如流、鏈表、無(wú)限分支樹(shù)或無(wú)限數(shù)組等.這一類(lèi)具有動(dòng)態(tài)行為特征的數(shù)據(jù)類(lèi)型可以進(jìn)一步抽象為某個(gè)共代數(shù)函子下的一個(gè)終結(jié)共代數(shù)，其中共代數(shù)函子對(duì)應(yīng)著該數(shù)據(jù)類(lèi)型上的觀察操作.由終結(jié)共代數(shù)的終結(jié)性可定義該數(shù)據(jù)類(lèi)型上的一個(gè)共遞歸操作，稱(chēng)為 unfold［9-10］操作或 atamorphism［2］，并且該操作滿(mǎn)足一系列的共代數(shù)計(jì)算定律.由于共遞歸操作及其計(jì)算定律在基于行為特征的函數(shù)定義或程序推理及轉(zhuǎn)換過(guò)程中具有重要的作用，因此 Greiner 等許多學(xué)者［5，8，11-15］均對(duì)共遞歸操作及其計(jì)算定律進(jìn)行了比較深入和全面的研究.這些研究的基本思路是將共歸納數(shù)據(jù)類(lèi)型看作某個(gè)共代數(shù)函子下的終結(jié)共代數(shù)，從而利用終結(jié)共代數(shù)及共歸納原理給出共遞歸操作上的各種計(jì)算定律.但這些研究對(duì)參數(shù)化共歸納數(shù)據(jù)類(lèi)型上的計(jì)算定律的分析較為簡(jiǎn)單，沒(méi)有考慮自然轉(zhuǎn)換下不同類(lèi)型函子上的計(jì)算定律.

因此，文中從范疇論的角度給出共歸納數(shù)據(jù)類(lèi)型的共代數(shù)描述，并結(jié)合實(shí)例對(duì)共歸納數(shù)據(jù)類(lèi)型上的共遞歸操作及其計(jì)算定律進(jìn)行分析，特別是利用雙函子及類(lèi)型函子對(duì)參數(shù)化共歸納數(shù)據(jù)類(lèi)型進(jìn)行抽象描述，并給出類(lèi)型函子上的計(jì)算定律及其證明.

1 共歸納數(shù)據(jù)類(lèi)型

作為歸納數(shù)據(jù)類(lèi)型的范疇對(duì)偶概念，共歸納數(shù)據(jù)類(lèi)型關(guān)注的不是數(shù)據(jù)類(lèi)型的語(yǔ)法構(gòu)造，而是數(shù)據(jù)類(lèi)型在執(zhí)行的過(guò)程中所展現(xiàn)出來(lái)的外部動(dòng)態(tài)行為特征.

例1 下面是程序語(yǔ)言中一些典型的共歸納數(shù)據(jù)類(lèi)型.

(1)流.用于描述輸入/輸出設(shè)備與程序之間交互關(guān)系的流一般包含兩個(gè)操作，一個(gè)操作value:AN→A用于得到流當(dāng)前狀態(tài)所能顯示的值(假設(shè)值的類(lèi)型為A，則無(wú)限流可表示為AN，其中N為自然數(shù))，另一個(gè)操作next:AN→AN則使流進(jìn)入下一個(gè)狀態(tài):

(2)鏈表.對(duì)于一個(gè)由空鏈表nil和插入操作cons遞歸定義而成的參數(shù)化鏈表(假定鏈表中元素的類(lèi)型為A，A∞=AN∪Aω是由無(wú)限鏈表AN和有限鏈表Aω所構(gòu)成的集合)，可通過(guò)兩個(gè)操作head和tail進(jìn)行觀察，其中head:A∞→1+A用于獲取鏈表的頭部元素，tail:A∞→1+A∞用于返回鏈表中除頭元素外的剩余元素.若數(shù)組為空，則兩個(gè)操作均返回⊥∈1:

(3)二叉樹(shù).對(duì)于以A中元素為標(biāo)簽的二叉樹(shù)btree(A)，可通過(guò)以下的操作進(jìn)行觀察:

其中l(wèi)eaf操作給出了根節(jié)點(diǎn)上的標(biāo)簽，left和right則分別返回以左右結(jié)點(diǎn)為根的二叉樹(shù).

從上述例子可以看出，共歸納數(shù)據(jù)類(lèi)型是由某個(gè)數(shù)據(jù)類(lèi)型集合及其上的一組析構(gòu)操作所構(gòu)成，其中析構(gòu)操作給出了對(duì)數(shù)據(jù)類(lèi)型的觀察結(jié)果.對(duì)于給定的共歸納數(shù)據(jù)類(lèi)型X，其上的析構(gòu)操作σ通常具有σ:X→A1×A2×…×An的形式，其中Ai為某個(gè)已知的數(shù)據(jù)類(lèi)型，表示對(duì)X的一種觀察結(jié)果.

作為代數(shù)的范疇對(duì)偶概念，共代數(shù)本質(zhì)上也可以看成是由集合及其上一組滿(mǎn)足一定性質(zhì)的操作所構(gòu)成，通常具有αX:X→FX的形式.在計(jì)算機(jī)科學(xué)中，共代數(shù)常被看成是具有內(nèi)部狀態(tài)的系統(tǒng)，X是系統(tǒng)中所有可能狀態(tài)的集合，基調(diào)αX是對(duì)系統(tǒng)的一種觀察.

定義1 給定集合范疇Set及其上的一個(gè)自函子F:Set→Set，一個(gè) F-共代數(shù)定義為一個(gè)二元組(X，αX:X→FX)，其中X是Set中的對(duì)象，稱(chēng)為該F-共代數(shù)的載體，αX:X→FX是Set中的射，稱(chēng)為該F-共代數(shù)的變遷射或基調(diào).任意兩個(gè)F-共代數(shù)(X，αX:X→FX)和(Y，αY:Y→FY)之間的同態(tài)射 f:(X，αX)→(Y，αY)是 Set中的射 f:X→Y，且滿(mǎn)足圖1 所示的圖表交換.

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

由于共歸納數(shù)據(jù)類(lèi)型本質(zhì)上也是由集合及其上一組滿(mǎn)足某些性質(zhì)的操作所構(gòu)成，因此可以進(jìn)一步抽象為某個(gè)共代數(shù)，其中共代數(shù)函子對(duì)應(yīng)著該數(shù)據(jù)類(lèi)型上的析構(gòu)操作.

例2 流、鏈表和二叉樹(shù)等共歸納數(shù)據(jù)類(lèi)型都可以表示為共代數(shù).

(1)流可以表示為函子SA(X)=A×X下的共代數(shù)(X，αX=〈value，next〉:X→A ×X)，X 為流中所有可能狀態(tài)的集合.

(2)鏈表可以表示為函子LA(X)=A×X+1下的共代數(shù)(X，αX=〈head，tail〉:X→A ×X+1).

(3)二叉樹(shù)可以表示為函子BA(X)=A×X×X下的共代數(shù)(X，αX=〈leaf，right，right〉:X→A × X ×X).

共歸納數(shù)據(jù)類(lèi)型不僅可以抽象地描述為共代數(shù)，而且是對(duì)應(yīng)共代數(shù)函子上的最大固定點(diǎn)，即為該函子的一個(gè)終結(jié)共代數(shù)，記為(vF，outF:vF→FvF).該終結(jié)共代數(shù)實(shí)際上就給出了共歸納類(lèi)型的定義.

例如，流可以看成是函子SA(X)=A×X下的一個(gè)終結(jié)共代數(shù)(AN，〈value，next〉:AN→A × AN)，鏈表可以看成是函子LA(X)=A×X+1下的一個(gè)終結(jié)共代數(shù)(A∞，〈head，tail〉:A∞→A × A∞+1)，二叉樹(shù)可以看成是函子BA(X)=A×X×X下的一個(gè)終結(jié)共代數(shù)(btree(A)，〈leaf，left，right〉:btree(A)→A ×btree(A)×btree(A))，其中btree(A)是由A中的元素所構(gòu)成的無(wú)限二叉樹(shù)結(jié)構(gòu).

根據(jù)文獻(xiàn)[16]中的定理9.1可得到終結(jié)代數(shù)上的一個(gè)重要性質(zhì).

定理1(文獻(xiàn)[16]中定理9.1)終結(jié)共代數(shù)上的基調(diào)是一個(gè)同構(gòu)射.

即基調(diào) outF:vF→FvF是一個(gè)同構(gòu)射，其逆outF－1:FvF→vF給出了載體集vF上的構(gòu)造操作.例如，函子FX=A×X的終結(jié)共代數(shù)上的基調(diào)outF=〈value，next〉的逆 outF－1=［scons］為流上的一個(gè)構(gòu)造操作，其中scons:A×X→X表示將一個(gè)類(lèi)型為A的元素作為前綴添加到一個(gè)流中.文獻(xiàn)［17］中指出在許多情況下函子F的終結(jié)共代數(shù)(vF，outF)可以理解為同一函子下的初始代數(shù)(μF，inF:μF→FμF)的某種形式的補(bǔ)充.例如，有限及無(wú)限鏈表集A∞可看成是函子FX=1+A×X下只包含有限鏈表Aω的初始代數(shù)的一種補(bǔ)充.事實(shí)上，根據(jù)上述定理1可將(vF，outF)的逆(vF，outF－1)看成是一個(gè)代數(shù).但這容易使得對(duì)共歸納原理的形式化描述變得更加復(fù)雜，而且也不符合共代數(shù)的非良基集性質(zhì).

2 共遞歸操作及其計(jì)算定律

由終結(jié)共代數(shù)的終結(jié)性可以定義每一個(gè)共歸納類(lèi)型上的一個(gè)操作，用于表示由該類(lèi)型上的結(jié)構(gòu)化共遞歸定義而成的函數(shù)，稱(chēng)為unfold操作或atamorphism.該函數(shù)就是由任意的F-共代數(shù)(X，αX)到其終結(jié)共代數(shù)(vF，outF)的唯一同態(tài)射，記為[αX]F:X→vF.由于[αX]F為一個(gè)共代數(shù)同態(tài)射，因此滿(mǎn)足等式:outF?[αX]F=F[αX]F?αX，即得如圖 2 所示的圖表交換.

圖2 終結(jié)共代數(shù)及其unfold操作Fig.2 Final coalgebras and its unfold operation

由終結(jié)共代數(shù)的終結(jié)性可以得到著名的共歸納原理(包括共歸納定義原則和證明原則).

(1)共歸納定義原則 要定義一個(gè)以終結(jié)共代數(shù)載體集為目標(biāo)的函數(shù)，只要根據(jù)所定義的函數(shù)所應(yīng)滿(mǎn)足的性質(zhì)，為該函數(shù)的源構(gòu)造一個(gè)合適的共代數(shù)即可;

(2)共歸納證明原則 要證明兩個(gè)以終結(jié)共代數(shù)載體集為目標(biāo)的函數(shù)相等，只需要證明這兩個(gè)函數(shù)都是同一共代數(shù)到終結(jié)共代數(shù)的同態(tài)即可.

例3 例1中的各個(gè)共歸納數(shù)據(jù)類(lèi)型上的unfold操作分別定義為

(1)對(duì)于任意的流共代數(shù)(X，αX=〈vs，ns〉:X→A×X，unfold操作為唯一射 f=[αX]SA:X→AN，滿(mǎn)足value ?f=vs和 next?f=f?ns.

(2)對(duì)于任意的鏈表共代數(shù)(X，αX=〈hd，tl〉:X→A×X+1，unfold為唯一射 f=[αX]LA:X→A∞，使得滿(mǎn)足 head ?f=hd 和 tail?f=f?tl.

(3)對(duì)于任意的二叉樹(shù)共代數(shù)(X，αX=〈lf，lt，rt〉:X→A×X ×X)，unfold為唯一射 f=[αX]BA:X→btree(A)，使得滿(mǎn)足 leaf?f=lf、left?f=f?lt和 right?f=f?rt.

共歸納數(shù)據(jù)類(lèi)型上的unfold操作滿(mǎn)足以下的共代數(shù)計(jì)算定律［2］.

定律1(單元定律)若unfold操作的源是終結(jié)共代數(shù)，那么該unfold操作為單元射，即:[outF]F=IdvF.

證明由任意的單元射IdvF:vF→vF都為同態(tài)射及unfold操作的唯一性可知[outF]F=IdvF成立.

定律2(unfold-map融合定律)對(duì)一個(gè)unfold操作和一個(gè)共代數(shù)同態(tài)射進(jìn)行復(fù)合后仍然為一個(gè)unfold 操作，即:αY?f=Ff?αX?[αY]F?f=[αX]F.

證明由前提可知下圖3中的左、右部分均滿(mǎn)足圖表交換.因此，[αY]F?f和[αX]F為共代數(shù)(X，αX)到終結(jié)共代數(shù)(vF，outF)的 unfold操作.由 unfold 操作的唯一性可知有 αY?f=Ff?αX?[αY]F?f=[αX]F.證畢.

圖3 共代數(shù)同態(tài)射及其unfold操作Fig.3 Homomorphism between coalgebras and its unfold operation

unfold-map融合定律在程序計(jì)算中具有重要的作用，可以用于消除計(jì)算過(guò)程中所產(chǎn)生的中間數(shù)據(jù)結(jié)構(gòu)，從而簡(jiǎn)化程序計(jì)算的結(jié)構(gòu).

例4 自然數(shù)流上的倍乘函數(shù)double:NatN→NatN將流中的每一個(gè)自然數(shù)元素都乘以2后構(gòu)成一個(gè)新的流:

顯然，double:(NatN，〈vl，nt〉)→(NatN，〈value，next〉)是自然數(shù)流之間的一個(gè)共代數(shù)同態(tài)射，且double 為一個(gè) unfold 射[〈vl，nt〉]SA.

函數(shù)merge:NatN×NatN→NatN依次交替地將兩個(gè)自然數(shù)流中的頭元素取出，并構(gòu)成一個(gè)新的流，即merge(a1:x1，x2)=a1:merge(x2，x1).顯然，merge 滿(mǎn)足以下等式:

因此，merge:(NatN× NatN，〈vs，ns〉)→(NatN，〈vl，nt〉)是一個(gè)同態(tài)射.對(duì)函數(shù) double和 merge進(jìn)行合并可得到以下等式:

double?merge表示先利用merge將兩個(gè)自然數(shù)流合并在一起，然后再將double函數(shù)作用于該流，最終得到一個(gè)新的自然數(shù)流.

根據(jù)unfold-map融合定律可以不需要merge和double函數(shù)，而是直接利用函數(shù) dmerge:(NatN×NatN，〈vs，ns〉)→(NatN，〈value，next〉)依次交替地將兩個(gè)自然數(shù)流中的頭元素取出并乘以2后構(gòu)成一個(gè)新的流，即

圖4 基于unfold-map融合定律的流實(shí)例Fig.4 Examples of stream for unfold-map fusion law

最后一個(gè)定律稱(chēng)為unfold-unfold定律，用于對(duì)產(chǎn)生并且消耗一個(gè)中間共代數(shù)結(jié)構(gòu)的函數(shù)進(jìn)行結(jié)合.應(yīng)用該定律時(shí)，要求中間的共代數(shù)結(jié)構(gòu)必須是由一個(gè)unfold操作產(chǎn)生的，并且該unfold操作的目標(biāo)共代數(shù)是通過(guò)一個(gè)自然轉(zhuǎn)換構(gòu)造而成.

所謂的自然轉(zhuǎn)換是指函子間的一個(gè)轉(zhuǎn)換函數(shù)τ:F?G，將一個(gè) F-共代數(shù)轉(zhuǎn)換為一個(gè) G-共代數(shù)，使得:若f:X→Y 為F-共代數(shù)(X，αX:X→FX)和(Y，αY:Y→FY)間的同態(tài)射，則 f同時(shí)為 G-共代數(shù)(X，τX(jué)?αX:X→GX)和(Y，τY?αY:Y→GY)間的同態(tài)射，即滿(mǎn)足 Gf?τX(jué)?αX=τY?αY?f.

直觀地說(shuō)，一個(gè)自然轉(zhuǎn)換τ:F?G可看成是一個(gè)多項(xiàng)式函數(shù)，將某一類(lèi)共代數(shù)轉(zhuǎn)換成另一類(lèi)共代數(shù).

定律3(unfold-unfold融合定律)給定一個(gè)自然轉(zhuǎn)換關(guān)系τ:F?G，對(duì)于 F-共代數(shù)(X，αX)，有:

證明對(duì)于任意的 F-共代數(shù)(X，αX)，由于unfold操作是一個(gè)同態(tài)射，根據(jù)自然轉(zhuǎn)換和unfold的性質(zhì)可知圖5中的各個(gè)圖表均滿(mǎn)足交換.[τvF?outF]G?[αX]F和[τX(jué)?αX]G均為 G-共代數(shù)(X，τX(jué)?αX)到G-終結(jié)共代數(shù)(vG，outG)的unfold操作.由unfold操作的唯一性可知[τvF?outF]G?[αX]F=[τX(jué)?αX]G.證畢.

圖5 unfold-unfold融合定律Fig.5 Unfold-unfold fusion law

3 參數(shù)化共歸納數(shù)據(jù)類(lèi)型

上述的流、鏈表和二叉樹(shù)等共歸納數(shù)據(jù)類(lèi)型通常都是參數(shù)化的，因此可以進(jìn)一步抽象為某個(gè)雙函子F:Set→Set×Set下的共代數(shù).通過(guò)固定雙函子F的共域中的第1個(gè)參數(shù)(假設(shè)該參數(shù)的類(lèi)型為A)，可得到一個(gè)一元函子F:Set→A×Set，記為FA，使得FAX=FA(A，X).設(shè)DvA是由FA所確定的終結(jié)共代數(shù)上的載體，則Dv:Set→Set可以提升為一個(gè)類(lèi)型函子［3］，使得對(duì)于任意的 f:A→B，有:Dvf=[F(f，IdDvA)?outFA]FB，如圖 6 所示.

圖6 類(lèi)型函子Fig.6 Type functor

例5 若Dv為流類(lèi)型構(gòu)造子，則對(duì)于類(lèi)型A有DvA=AN，對(duì)于射 f:A→B 有:Dvf=fN=[〈f?value，next〉]SB:AN→BN;若 Dv為鏈表類(lèi)型構(gòu)造子，則對(duì)于類(lèi)型A有 DvA=A∞，對(duì)于射f:A→B有:Dvf=f∞=[〈f?head，tail〉]LB:A∞→B∞;若 Dv為一個(gè)二叉樹(shù)類(lèi)型構(gòu)造子，則對(duì)于類(lèi)型A有DvA=btree(A)，對(duì)于射f:A→B 有:Dvf=btree(f)=[〈f?leaf，left，right〉]BB:btree(A)→btree(B).

類(lèi)型函子Dv滿(mǎn)足相應(yīng)的unfold-map融合定律.

圖7 類(lèi)型函子的unfold-map融合定律Fig.7 Unfold-map fusion law for type functor

定律4(類(lèi)型函子上的unfold-map融合定律)對(duì)于 f:A→B 和 g:X→FAX，有:Dvf?[g]FA=[F(f，IdX)?g]FB.

證明 根據(jù)前提可知上述圖中的各個(gè)圖表均滿(mǎn)足交換.Dvf?[g]FA和[F(f，IdX)?g]FB均為共代數(shù)(X，F(xiàn)(f，IdX)?g)到(DvB，outFB)的 unfold 操作.由unfold 的唯一性可知 Dvf?[g]FA=[F(f，IdX)?g]FB.證畢.

定理2 對(duì)于兩個(gè)雙函子F，G:Set→Set×Set，設(shè)τ:F?G 為一個(gè)自然轉(zhuǎn)換，τA，X表示 τA，X:FAX?GAX，則對(duì)于 g:X→FAX，有 τA，X?g:X→GAX，且對(duì)于f:A→B有:

證明 由類(lèi)型函子的性質(zhì)及unfold操作的唯一性可證明成立.

在自然轉(zhuǎn)換的作用下，類(lèi)型函子Dv滿(mǎn)足相應(yīng)的unfold-unfold融合定律，如圖8所示.

圖8 自然轉(zhuǎn)換下的類(lèi)型函子Fig.8 Type functor via natural transformation

定律5(類(lèi)型函子上的unfold-unfold融合定律)對(duì)于f:A→B、g:X→FAX及自然轉(zhuǎn)換τ:F?G，有:

證明由unfold的定義及自然轉(zhuǎn)換保持態(tài)射和組合關(guān)系的性質(zhì)可知，Dvf?[g]FA=[τB，X?F(f，IdX)?g]GB和[G(f，IdX)?τA，X?g]GB均為共代數(shù)(X，G(f，IdX)?τA，X?g)到(DvB，outGB)的 unfold 操作，因此由其唯一性可證明上述等式成立.證畢.

其融合定律如圖9所示.

圖9 類(lèi)型函子上的unfold-unfold融合定律Fig.9 Unfold-unfold fusion law for type functor

4 結(jié)語(yǔ)

對(duì)共歸納數(shù)據(jù)類(lèi)型上的共遞歸操作及其計(jì)算定律進(jìn)行研究有助于人們更加深入地了解抽象數(shù)據(jù)類(lèi)型的動(dòng)態(tài)行為特征，提高程序語(yǔ)言對(duì)其動(dòng)態(tài)行為的描述能力.更重要的，可以將終結(jié)共代數(shù)及共歸納原理等共代數(shù)理論引入到類(lèi)型理論中，便于在程序中定義更加復(fù)雜的函數(shù)或開(kāi)展基于行為特征的推理或轉(zhuǎn)換工作.

在下一步工作中，將對(duì)其它的共遞歸操作(例如原始共遞歸和Course-of-value共遞歸等)及其計(jì)算定律進(jìn)行深入的研究.

［1］Bird R.Introduction to functional programming using haskell［M］.2nd edition.UK:Prentice-Hall，1998.

［2］Meijer E，F(xiàn)okkinga E，Paterson R.Functional programming with bananas，lenses，envelopes and barbed wire［C］∥Functional Programming Languages and Computer Architecture.Berlin:Springer，1991:215-240.

［3］Bird R，Moor O D.Algebra of programming［M］.UK:Prentice Hall，1997.

［4］Gibbons J.Lecture notes on algebraic and coalgebraic methods for calculating functional programs［C］∥Summer School on Algebraic and Coalgebraic Methods in the Mathematics of Program Construction.UK:Oxford，2000.

［5］Greiner J.Programming with inductive and co-inductive types［R］.Pittsburgh:School of Computer Science，Carnegie-Mellon University，1992.

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

［7］Kieburtz R B.Codata and comonads in Haskell［EB/OL］.(1999-12-31).http:∥citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.5169.

［8］Hinze R.Reasoning about Codata［C］∥Proceedings of centraleuropean functionalprogramming school-third summer school.Berlin:Springer Berlin Heidelberg，2010:42-93.

［9］Hutton G.Fold and unfold for program semantics［C］∥Proceedings of the 3rd ACM Sigplan International Conference on Functional Programming.［S.l.］:ACM，1998:280-288.

［10］Gibbons J，Jones G.The under-appreciated unfold ［C］∥Proc 3rd ACM Sigplan International Conference on Functional Programming.New York:ACM，1998:273-279.

［11］Harper R.Practical foundations fro programming languages［M］.［S.l.］:Carnegie Mellon University，2010.

［12］Vos T.Program construction and generation based on recursive types［D］.Utrecht:University of Utrecht，1995.

［13］Vene V，Uustalu T.Functional programming with apomor phism(Corecursion)［J］∥Proceedings of the Estonian Academy of Science:Physics，Mathematics，1998，47(3):147-161.

［14］Uustalu T，Vene V.Primitive(Co)recursion and course-of-value(Co)iteration，categorically ［J］.Informatica，1999，10(1):5-26.

［15］Vene V.Categorical programming with inductive and coinductive types［D］.Estonia:Department of Computer Science，University of Tartu，2000:1-100.

［16］Rutten J J M M.Universal coalgebra:a theory of systems［J］.Theoretical Computer Science，2000，249(1):3-80.

［17］Barr M.Terminal coalgebras in well-founded set theory［J］.Theoretical Computer Science，1993，114(2):299-315.