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

蘇錦鈿 余珊珊

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

例2 流、鏈表和二叉樹等共歸納數(shù)據(jù)類型都可以表示為共代數(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)二叉樹可以表示為函子BA(X)=A×X×X下的共代數(shù)(X，αX=〈leaf，right，right〉:X→A × X ×X).

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

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

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

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

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

2 共遞歸操作及其計算定律

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

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

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

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

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

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

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

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

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

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

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

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

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

證明由前提可知下圖3中的左、右部分均滿足圖表交換.因此，[α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融合定律在程序計算中具有重要的作用，可以用于消除計算過程中所產(chǎn)生的中間數(shù)據(jù)結(jié)構(gòu)，從而簡化程序計算的結(jié)構(gòu).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

圖6 類型函子Fig.6 Type functor

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

類型函子Dv滿足相應(yīng)的unfold-map融合定律.

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

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

證明 根據(jù)前提可知上述圖中的各個圖表均滿足交換.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 對于兩個雙函子F，G:Set→Set×Set，設(shè)τ:F?G 為一個自然轉(zhuǎn)換，τA，X表示 τA，X:FAX?GAX，則對于 g:X→FAX，有 τA，X?g:X→GAX，且對于f:A→B有:

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

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

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

定律5(類型函子上的unfold-unfold融合定律)對于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 類型函子上的unfold-unfold融合定律Fig.9 Unfold-unfold fusion law for type functor

4 結(jié)語

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

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

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