帶固定參數(shù)的Monadic遞歸*

蘇錦鈿 余珊珊

(1.華南理工大學(xué) 計(jì)算機(jī)科學(xué)與工程學(xué)院，廣東 廣州 510640;2.廣東藥學(xué)院 醫(yī)藥信息工程學(xué)院，廣東 廣州 510006)

作為歸納數(shù)據(jù)類型［1］上最重要的一種計(jì)算模式，遞歸操作fold［2］在程序設(shè)計(jì)、推理、轉(zhuǎn)換和優(yōu)化等方面具有廣泛的應(yīng)用，并構(gòu)成其他各種復(fù)雜的遞歸計(jì)算的基礎(chǔ)，如原始遞歸、Course-of-Value 迭代、帶參數(shù)的遞歸和累積遞歸等.但fold 一方面要求計(jì)算源中的元素必須具備相應(yīng)的代數(shù)結(jié)構(gòu)，無(wú)法包含額外的參數(shù)用于作為計(jì)算的輸入;另一方面只適合于描述計(jì)算過(guò)程中所產(chǎn)生的確定性結(jié)果，無(wú)法包含其他各種計(jì)算副作用(如偏序、非確定性、異常、連續(xù)、交互式輸入、交互式輸出等).針對(duì)上述問(wèn)題，Cockett 等最早在文獻(xiàn)［3-4］中利用笛卡爾封閉范疇上的強(qiáng)函子提出了強(qiáng)范疇數(shù)據(jù)類型的概念，使得強(qiáng)歸納數(shù)據(jù)類型上的fold 可包含額外的參數(shù)，并將其作為函數(shù)式程序語(yǔ)言Charity 的基礎(chǔ).隨后，Pardo［5-7］進(jìn)一步對(duì)強(qiáng)歸納數(shù)據(jù)類型上帶固定參數(shù)和累積參數(shù)的遞歸操作pfold 和afold 的范疇論性質(zhì)及其計(jì)算律進(jìn)行了分析.筆者在前期工作中也分析了強(qiáng)共歸納數(shù)據(jù)類型上帶固定參數(shù)的共遞歸及其計(jì)算律［8-9］，并將其擴(kuò)展到hylomorhpism 中［10］，同時(shí)還從雙代數(shù)的角度探討了歸納與共歸納數(shù)據(jù)類型、遞歸與共遞歸間的關(guān)系［11］.上述研究都是針對(duì)強(qiáng)歸納或強(qiáng)共歸納數(shù)據(jù)類型上的純函數(shù)，沒(méi)有考慮計(jì)算過(guò)程中可能產(chǎn)生的副作用.

Fokkinga［12］結(jié)合monads 及集合范疇上的正則函子提出任意數(shù)據(jù)類型上的monadic 射和fold.Hu等［13］進(jìn)一步將Fokkinga 的研究擴(kuò)展到任意monads上.Meijer 等［14］則從函數(shù)式程序語(yǔ)言實(shí)現(xiàn)的角度探討monadic fold 的應(yīng)用.Pardo［15］也結(jié)合monads 給出包含計(jì)算副作用的monadic 共遞歸和hylomorphism的定義.在Pardo 和Meijer 的研究基礎(chǔ)上，Ghani等［16］探討了所有歸納數(shù)據(jù)類型上的build 結(jié)合子及其參數(shù)的歸納和monadic 構(gòu)造.這些研究均沒(méi)有考慮帶參數(shù)且包含計(jì)算副作用的遞歸，也沒(méi)有分析相應(yīng)的范疇論性質(zhì)及其代數(shù)計(jì)算律.

因此，文中在上述研究的基礎(chǔ)上，結(jié)合范疇論中的monads 及伴隨概念給出monadic 強(qiáng)歸納數(shù)據(jù)類型的定義及其monadic 強(qiáng)初始性的證明，并分析了其上帶固定參數(shù)且包含計(jì)算副作用的遞歸操作的定義、性質(zhì)及計(jì)算律，從而將Cockett 和Pardo 等對(duì)強(qiáng)歸納數(shù)據(jù)類型及Fokkinga、Hu 和Meijer 等對(duì)monadic 遞歸的研究融合在一起.

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

1.1 代數(shù)和歸納數(shù)據(jù)類型

下面首先給出代數(shù)的范疇論定義.

定義1 給定范疇C 和自函子F:C→C，F(xiàn)－代數(shù)定義為二元組(X，αX:FX→X)，其中X 稱為該F－代數(shù)的載體，αX稱為該F－代數(shù)的基調(diào).任意兩個(gè)F－代數(shù)(X，αX)和(Y，αY)間的F－代數(shù)同態(tài)射f:(X，αX)→(Y，αY)是載體集上的射f:X→Y，且滿足等式fαX=αYFf.

若代數(shù)函子F:C→C 存在初始代數(shù)，記為(μF，inF)，則對(duì)于任意一個(gè)F－代數(shù)(X，αX)，總存在從(μF，inF)到(X，αX)的唯一F－代數(shù)同態(tài)射foldF(αX):μF→X，即滿足等式foldF(αX)inF=αXFinF.

操作foldF(αX)是由基調(diào)αX所確定的迭代射，在函數(shù)式程序語(yǔ)言中常稱為fold［2］或catamorphism［17］.

為保證代數(shù)函子總是存在相應(yīng)的初始代數(shù)，文中只考慮以下的代數(shù)函子［15］.

定義2 范疇C 上的代數(shù)函子F:C→C 是由以下的函子歸納構(gòu)造而成:

式中:Id 表示標(biāo)識(shí)函子;A 表示A 上的常量函子;F +F 表示函子間的共積，F(xiàn)×F 表示函子間的積;F〈F，F(xiàn)，…，F(xiàn)〉(或記為F〈Fi〉)表示F:Cn→C 與其他代數(shù)函子F1，F(xiàn)2，…，F(xiàn)n的組合，且F1，F(xiàn)2，…，F(xiàn)n均具有相同的元數(shù).

Vene 在文獻(xiàn)［18］中證明了若F 為ω－共連續(xù)的(例如保持ω－共極限)，則對(duì)應(yīng)的F－初始代數(shù)存在.對(duì)于分配范疇［19］(如集合范疇或完全偏序范疇)來(lái)說(shuō)，定義2 中的代數(shù)函子都是ω－共連續(xù)函子，因此其初始代數(shù)總是存在.

下面如無(wú)特別說(shuō)明，均假定范疇C 為分配范疇，并用F 或G 等大寫字母表示定義2 中的代數(shù)函子.

Kock 在文獻(xiàn)［20］中證明了分配范疇C 上的定義2 中的代數(shù)函子都是強(qiáng)函子.

1.2 Monads

定義4 范疇C 上的monad 可表示一個(gè)Kleisli三元組(T，η，－*)，其中T:為C 中對(duì)象間的映射，映射η 對(duì)于任意對(duì)象XC 有ηX:X→TX;提升函數(shù)－*對(duì)于任意射f:X→TY 有f*:TX→TY，且滿足以下等式(即使得圖1 中的所有圖表滿足交換條件):

(1)ηX*=IdTX;

(2)對(duì)于f:X→TY，有f*ηX=f;

(3)對(duì)于f:X→TY 和g:Y→TZ，有g(shù)*f*=(g*f)*.

圖1 Kleisli 三元組的圖表交換Fig.1 Graph commutation of Kleisli triples

Monads 也可從范疇論的角度給出相應(yīng)的定義.

定義5 范疇C 上的monad 定義為一個(gè)三元組(T，η，μ)，其中T:C→C 為自函子，η:IdT 和μ:T2T 為自然轉(zhuǎn)換，且滿足等式μηT=μTη=Id 和μTμ=μμT.

稱η 和μ 分別為該monad 的單位元和倍乘操作.容易驗(yàn)證(T，η，－*)和(T，η，μ)定義之間存在一一對(duì)應(yīng)關(guān)系.為了便于討論，文中有時(shí)候用monads的Kleisli 三元組定義，有時(shí)候用其范疇論定義.

例1 下面是部分典型的monads 結(jié)構(gòu).

(1)標(biāo)識(shí)monad(Id，Id，Id):表示將一個(gè)類型映射到它本身.在計(jì)算意義上，標(biāo)識(shí)monad 代表平凡的狀態(tài)，即不進(jìn)行任何動(dòng)作并立即返回值.η 和μ 均為標(biāo)識(shí)射.對(duì)于射f:X→X，f*也為標(biāo)識(shí)射，將f 映射為自身;

(2)異常monad(Id +E，inl，［Id，inr］):表示計(jì)算可能成功并返回給定類型的輸出值，也可能失敗并返回類型為E 的輸出值(E 為異常的集合).ηX=inl:X→X +E，μ=［Id，inr］:(X +E)+E→X +E;對(duì)于f:X→TY，f*=［f，inr］:X+E→X+E，使得f*(c)=c(cE)和f*(x)=f(x)(xX);若E 為1，則稱其為部分monad(Id+1，inl，［Id，inr］);

(3)積monad(Id×S，〈IdX，e!X〉，Id×mr－ ×Id):TX=X ×S 描述計(jì)算中包含了簡(jiǎn)單的輸出處理或計(jì)算資源(如時(shí)間或空間)，其中(S，e，m)為一個(gè)獨(dú)異點(diǎn)，e:1→S 為單位元函數(shù)，m:S ×S→S 為S 上的二元函數(shù).ηX=〈IdX，e!X〉:X→X ×S，μX=IdX×mr:(X×S)×S→X×S.對(duì)于f:X→Y×S 有f*=Id ×mrf×IdS，即f*(x，s)=〈fst(f(x))，m(snd(f(x))，s)〉(xX，sS).其中，!X:X→1 為任意元素對(duì)終結(jié)對(duì)象1 的射，r:(X×S)×S→X×(S×S)為交換元素位置的自然同構(gòu)射.

類似地，還有許多其他的monads，如數(shù)組、狀態(tài)、副作用、Input/Output、writer 和連續(xù)monad 等.

定義6 稱范疇C 上的(T，η，－*)為強(qiáng)monad當(dāng)且僅當(dāng)T 為強(qiáng)函子，且同時(shí)滿足以下等式:

(1)CA中的對(duì)象與C 中的對(duì)象相同;

(2)CA中任意兩個(gè)對(duì)象X 和Y 之間的射為C中對(duì)象間形如f:X×A→Y 的射;

(3)CA中任意對(duì)象X 上的單位射為fst:X×A→X;

(4)CA中任意兩個(gè)射f:X×A→Y 和g:Y×A→Z間的組合為gAf=g〈f，snd〉:X×A→Z.

若將C 看成是純函數(shù)范疇，則CA就是描述了所有計(jì)算源中包含參數(shù)類型A 的計(jì)算范疇.

利用monad(T，η，－*)可將射f:X×A→Y 提升為fT=ηXf:X ×A→TY，從而描述了帶固定參數(shù)A且產(chǎn)生副作用T 的計(jì)算.稱形如f:X ×A→TY 的射為帶固定參數(shù)的monadic 射.若(T，η，－*)為強(qiáng)monad，則fT可進(jìn)一步提升為射f#=μYTf:TX ×A→TY，f#表示對(duì)fT的提升.

定義8 給定范疇CA及范疇C 上的一個(gè)強(qiáng)monad(T，η，－*)，定義范疇CT為:

(1)CT中的對(duì)象與CA的對(duì)象相同;

(2)CT中的射為CA中射f:X ×A→TY 的提升fT=ηYf:X×A→TY;

(3)CT中任意對(duì)象X 上的單位射為CA中X 上單位射fst:X×A→X 的提升fstT:X×A→TX;

(4)CT中任意兩個(gè)射f:X×A→TY 和g:Y×A→TZ 間的組合為gTf=g#〈f，snd〉=〈f，snd〉:X×A→TZ.

范疇CT描述了所有帶參數(shù)A 且產(chǎn)生副作用的計(jì)算范疇，組合gTf 給出了計(jì)算結(jié)果及副作用在計(jì)算中的傳遞.顯然，－T可看成從范疇CA到CT的一個(gè)函子，將范疇CA中的對(duì)象X 映射為自身XT=X，將范疇CA中的f:X ×A→Y 映射為對(duì)應(yīng)的fT，將范疇CA中的射f:X×A→Y 和g:Y×A→Z 間的組合gAf 映射為范疇CT中的射(gAf)T=gTTfT.

Pardo 在文獻(xiàn)［5］中定義了函子－^ :C→CA用于將C 中的f:X→Y 提升為f^=ffst:X×A→Y，將C 中射f:X→Y 和g:Y→Z 間的組合gf 提升為

定義9 給定范疇C 上的monad(T，η，－*)和自函子F:C→C，稱自然轉(zhuǎn)換 :FTTF 為F 對(duì)T 的分配律，當(dāng)且僅當(dāng)以下等式成立:

若分配律 存在，可定義函子F :CT→CT，將CT中的對(duì)象X 映射為X=FX，將f:X×A→TY 映射為f=XFf:FX ×A→TFY，將f:X ×A→TY 和g:Y×A→TZ 間的組合gTf 映射為F (gTf)=F gTF f:FX×A→TFZ.

2 Monadic 強(qiáng)歸納數(shù)據(jù)類型

為區(qū)別于一般的F－代數(shù)(X，αX:FX→X)，將形如()的結(jié)構(gòu)稱為FA－ 代數(shù).任意兩個(gè)FA－代數(shù)(X，φX)和(Y，φY)間的FA－代數(shù)同態(tài)射f:(X，φX)→(Y，φY)為射f:X ×A→Y，且滿足f.若 射f:X→Y 滿足fφX=φYFf ×IdA，則稱f 為(X，φX)和(Y，φY)間的純FA－代數(shù)同態(tài)射.由范疇C 上的所有FA－代數(shù)及其FA－ 代數(shù)同態(tài)射可構(gòu)成范疇Alg(FA).

類似地，將形如(X，φX:FX ×A→TX)的代數(shù)稱為monadic FA－代數(shù).給定強(qiáng)monad(T，η，－*)及分配律:FTTF，任意兩個(gè)monadic FA－代數(shù)(X，φX)和(Y，φY)間的monadic FA－代數(shù)同態(tài)射為射f:X×A→TY，且滿足f#〈φX，snd〉=φY#〈f，snd〉.若射f:X→Y 滿足TfφX=φYFf×IdA，則稱f 為(X，φX)和(Y，φY)間的純monadic FA－代數(shù)同態(tài)射.由范疇C 上所有monadic FA－代數(shù)及其monadic FA－代數(shù)同態(tài)射可構(gòu)成范疇AlgT(FA).

定義10 給定范疇Alg(FA)和AlgT(FA)，定義函子L:Alg(FA)→AlgT(FA)為:

(1)L 將Alg(FA)中的FA－代數(shù)(X，φX)映射為AlgT(FA)中對(duì)應(yīng)的L(X，φX)=(X，φ);

(2)L 將Alg(FA)中(X，φX)和(Y，φY)間的FA－代數(shù)同態(tài)射f:X×A→Y 映射為AlgT(FA)中(X，)和(Y，)間的monadic FA－代數(shù)同態(tài)射Lf=fT:X×A→TY;

(3)L 將Alg(FA)中任意對(duì)象X 上的單位射fst:X×A→X 映射為AlgT(FA)中對(duì)應(yīng)的fstT:X×A→TX;

(4)L 將Alg(FA)中的FA代數(shù)同態(tài)射f:X×A→Y和g:X×Y→Z 間的組合gAf 映射為AlgT(FA)中對(duì)應(yīng)的monadic FA－代數(shù)同態(tài)射組合L(gAf)=LgTLf.

由L 的定義可知L 保持單位射及射之間的組合關(guān)系.因此，L 確實(shí)為函子.

定義11 給定范疇Alg(FA)和AlgT(FA)，定義函子V:AlgT(FA)→Alg(FA)為:

(1)V 將AlgT(FA)的monadic FA－代數(shù)(X，φX)映射為Alg(FA)中的FA－ 代數(shù)V(X，φX)= (TX，X×IdA:FTX×A→TX);

(2)V 將AlgT(FA)的monadic FA－代數(shù)同態(tài)射f:X×A→TY 映射為Alg(FA)中的FA－代數(shù)同態(tài)射Vf=f#:TX×A→TY;

(3)V 將AlgT(FA)中任意對(duì)象X 上的單位射fstT:X×A→TX 映射為Alg(FA)中對(duì)應(yīng)對(duì)象TX 上的單位射fst:TX×A→TX;

(4)V 將AlgT(FA)的monadic FA－代數(shù)同態(tài)射f:X×A →TY 和g:Y×A→TZ 間的組合gTf 映射為Alg(FA)中對(duì)應(yīng)的FA－代數(shù)同態(tài)射組合V(gTf )=VgAVf.

命題1 L:Alg(FA)→AlgT(FA)和V:AlgT(FA)→Alg(FA)構(gòu)成伴隨關(guān)系且L 為左伴隨，V 為右伴隨.

證明 由L 和V 的定義可知存在自然轉(zhuǎn)換ηX×fst:IdVL，使得對(duì)于Alg(FA)中任意的FA－代數(shù)同態(tài)射f:X×A→TY，AlgT(FA)中均存在對(duì)應(yīng)的monadic FA－代數(shù)同態(tài)射g:X ×A→TY，并滿足f=VgAηX×fst，如圖2 所示.

圖2 函子L 和V 間的伴隨關(guān)系Fig.2 Adjoint between the functors L and V

根據(jù)伴隨關(guān)系的定義(見(jiàn)文獻(xiàn)［21］中定義13.2.1)可知構(gòu)成伴隨關(guān)系，且L 為左伴隨，V 為右伴隨.證畢.

Pardo［5］證明了分配范疇上的強(qiáng)歸納數(shù)據(jù)類型具有強(qiáng)初始性，即(μF:FμF×A→μF)是范疇Alg(FA)中的初始代數(shù).由于左伴隨保持極限，因此L 將Alg(FA)中的FA－初始代數(shù)提升為AlgT(FA)中對(duì)應(yīng)的monadic FA－初始代數(shù)，且保持其初始性.即(μF:FμF×A→TμF)是AlgT(FA)中的初始代數(shù)，且具有初始性.

定義12 稱強(qiáng)函子F 的初始代數(shù)(μF，inF)為monadic 強(qiáng)初始的，當(dāng)且僅當(dāng)對(duì)于對(duì)象A，提升iFμF×A→TμF 是范疇AlgT(FA)中的一個(gè)初始對(duì)象.

即對(duì)于AlgT(FA)中的任意monadic FA－代數(shù)(X，φX)，總是存在從(μF)到(X，φX)的唯一monadic FA－代數(shù)同態(tài)射f:μF ×A→TX，并稱(μF，)是monadic 強(qiáng)初始的.

命題2 對(duì)于分配范疇上的代數(shù)函子F 及強(qiáng)monad(T，η，－*)，若存在分配律:FTTF，則F－初始代數(shù)是monadic 強(qiáng)初始的.

證明 由命題1 可得.證畢.

由命題2 可給出monadic 強(qiáng)歸納數(shù)據(jù)類型的定義.

定義13 稱一個(gè)歸納數(shù)據(jù)類型是monadic 強(qiáng)歸納類型當(dāng)且僅當(dāng)該歸納數(shù)據(jù)類型所對(duì)應(yīng)的初始代數(shù)是monadic 強(qiáng)初始的.

3 帶固定參數(shù)的Monadic 遞歸

定義14 給定強(qiáng)函子F:C→C、強(qiáng)monad(T，η，－*)和對(duì)象AC，對(duì)于任意一個(gè)monadic FA－代數(shù)(X，φX)，帶固定參數(shù)的monadic 遞歸pmfold，記為pmfoldF(φX):μF ×A→TX，是指滿足以下等式的最小解:

即使得圖3 滿足圖表交換條件.

圖3 pmfold 的定義Fig.3 Definition of pmfold

每一個(gè)pmfoldF(φX)可看成是在遞歸計(jì)算過(guò)程中計(jì)算源包含了參數(shù)類型為A 的元素，該參數(shù)的值在計(jì)算過(guò)程中保持不變，且所產(chǎn)生的計(jì)算副作用封裝在T 中.

命題3 每一個(gè)fold 都可看成是計(jì)算過(guò)程中不使用參數(shù)且不產(chǎn)生任何計(jì)算副作用的pmfold.

證明 對(duì)于任意一個(gè)F－代數(shù)(X，αX)，由定義14可知每一個(gè)foldF(αX):μF→X 相當(dāng)于在計(jì)算過(guò)程中不使用參數(shù)A 且T 為標(biāo)識(shí)monad 的pmfold，并滿足:證畢.

命題4 文獻(xiàn)［5］中的每一個(gè)pfold 都可看成是帶固定參數(shù)但不產(chǎn)生任何計(jì)算副作用的pmfold.

證明 對(duì)于任意一個(gè)FA－代數(shù)(X，φX)，由定義14 及文獻(xiàn)［5］中pfold 的定義可知pfoldF(φX):μF×A→X 相當(dāng)于T 為標(biāo)識(shí)monad 的pmfold，并滿足等式pfoldF(φX)T=pmfoldF(φTX).證畢.

命題5 文獻(xiàn)［12］中的每一個(gè)monadic fold 都可看成是不使用任何參數(shù)的pmfold.

證明 對(duì)于任意一個(gè)monadic F－代數(shù)(X，αX:FX→TX)，由定義14 及文獻(xiàn)［12］中monadic fold 的定義可知每一個(gè)monadic fold(［αX］)T:μF→TX 相當(dāng)于計(jì)算過(guò)程中不使用參數(shù)A 的pmfold，且滿足等式證畢.由命題3－ 5 可知pmfold 實(shí)際上給出fold、pfold［5］和monadic fold［12］的一種抽象描述.因此，它們的標(biāo)識(shí)律、消去律和融合律等計(jì)算律在pmfold 中仍然成立.下面給出pmfold 上的部分典型計(jì)算律.

定律1(標(biāo)識(shí)律) 每一個(gè)pmfold 滿足等式:

證明 由前面－^ 和－#的定義和定義14 容易驗(yàn)證為一個(gè)pmfold，且等于ηXfst.再由－#的定義可知IdTμF×A成立.證畢.

定律2(消去律) pmfold 滿足:

證明 由定義14 可得.證畢.

定律3(pmfold 與monadic FA－代數(shù)同態(tài)射融合律) pmfold 與monadic FA－代數(shù)同態(tài)射之間的組合仍是pmfold，即:f=pmfoldF(φX)∧g#〈φX，snd〉=〈F g，snd〉gTf=pmfoldF(φY).

證明 由前提可知圖4 中的左右部分均滿足圖表交換條件.因此，整個(gè)圖4 滿足圖表交換條件.

圖4 pmfold 與monadic FA－代數(shù)同態(tài)射的融合律Fig.4 Fusion law for pmfold and monadic FA-algebraic homomorphism

類似地，可證明pmfold 與純monadic FA－代數(shù)同態(tài)射之間的組合仍是一個(gè)pmfold.

定律4(pmfold 與純monadic FA－代數(shù)同態(tài)射融合律) pmfold 與純monadic FA－代數(shù)同態(tài)射之間的組合仍是pmfold:f=pmfoldF(φX)∧TgφY=φXFg×IdATgf=pmfoldF(φY).

定律5(pmfold-pmfold 融合律) 若存在自然轉(zhuǎn)換子ρ:FG，將每個(gè)monadic GA－代數(shù)(X，φX)映射為對(duì)應(yīng)的monadic FA－代數(shù)(X，φXρX×IdA)，將每個(gè)monadic GA－代數(shù)同態(tài)射f:(X，φX)→(Y，φY)映射為對(duì)應(yīng)的monadic FA－ 代數(shù)同態(tài)射，則兩個(gè)pmfold g= pmfoldG(φX)與f= pmfoldF(ρμG×IdA)間的組合仍是一個(gè)pmfold:

(φXρX×IdA)，其中κ:GTTG 為函子G 對(duì)T 的分配律.

證明 由前提及函子和自然轉(zhuǎn)換保持同態(tài)射的性質(zhì)可知圖5 中的左半部分以及右邊的上下部分均滿足圖表交換條件，因此整個(gè)圖5 滿足圖表交換條件.

圖5 pmfold 間的融合律Fig.5 Fusion law for pmfold

由于fold、pfold 和monadic fold 均可看成是pmfold 的一種特殊情況，因此pmfold 與它們間的組合仍是pmfold 操作.

利用上述各種融合律可以消去pmfold 在計(jì)算過(guò)程中所產(chǎn)生的中間數(shù)據(jù)，從而簡(jiǎn)化或優(yōu)化程序的計(jì)算.

4 應(yīng)用分析

4.1 歸納數(shù)據(jù)類型及fold 射

例2 程序語(yǔ)言中常用的樹、數(shù)組和自然數(shù)等都是典型的歸納數(shù)據(jù)類型:

(1)設(shè)BTree(A)是以集合A 中的元素為標(biāo)簽的二元樹，其上的構(gòu)造子包括empty:1→X 和node:X ×A×X→X，即二元樹BTree(A)可看成是代數(shù)函子RX=1 +X ×A ×X 所對(duì)應(yīng)的初始代數(shù)(BTree(A)，inR=［empty，node］).

(2)設(shè)［A］是所有包含集合A 中元素的有限數(shù)組的集合，其上的構(gòu)造子包括:nil:1→［A］用于將數(shù)組初始化為空，cons:A×［A］→［A］用于將一個(gè)類型為A 的元素插入到給定的數(shù)組中，concat:［A］×［A］→［A］用于將兩個(gè)數(shù)組串聯(lián)成一個(gè)新的數(shù)組.顯然，［A］就是程序語(yǔ)言中類型為A 的參數(shù)化數(shù)組，且為代數(shù)函子L=1 +A×X+X×X 的初始代數(shù)(［A］，inL=［nil，cons，concat］).

(3)自然數(shù)Nat 上的構(gòu)造子包括:zero:1→Nat用于將自然數(shù)初始化為0，succ:Nat →Nat 為映射succk(0)asucck+1(0)，用于對(duì)自然數(shù)加1，add:Nat×Nat→Nat 用于對(duì)兩個(gè)自然數(shù)相加.則Nat 可看成是代數(shù)函子NX=1 +X+X×X 的初始代數(shù)(Nat，inN=［zero，succ，add］).

由歸納數(shù)據(jù)類型所對(duì)應(yīng)的初始代數(shù)及其初始性可以給出許多fold 操作的定義.典型地，在函數(shù)式程序語(yǔ)言Haskell 中，數(shù)組類型［］上的各種折疊遞歸函數(shù)如fold、foldl 和foldr，以及針對(duì)非空數(shù)組的foldl1 和foldr1，都是基于［］的初始性和唯一性.

為了簡(jiǎn)單起見(jiàn)，一般直接將數(shù)組上的cons(a，l)表示為a:l，將concat(l，s)表示為l::s，將Nat 上的succ(p)表示為p+1，將add(p，q)表示為p+q.

4.2 pmfold 例子

下面以二元樹上的遍歷操作為例說(shuō)明pmfold的應(yīng)用.

例3 BTree(A)上的先序遍歷操作traverse:BTree(A)×［A］→［A］×［A］定義為(其中b1，b2BTree(A)，aA，l［A］，s［A］，且s 初始值為空數(shù)組［］):

(1)traverse(empty，l)=〈［］，［］〉;

(2)traverse(node(b1，a，b2)，l)=if isin(a，l)then

其中isin:A×［A］→1 +1 用于判斷某個(gè)元素是否存在于給定的數(shù)組中，即isin(a，l)=if al then true else false.

顯然，函數(shù)traverse 表示遞歸地對(duì)二元樹中的所有節(jié)點(diǎn)進(jìn)行先序遍歷，并返回由這些節(jié)點(diǎn)所構(gòu)成的數(shù)組;若節(jié)點(diǎn)存在于某個(gè)給定的數(shù)組中，則同時(shí)以數(shù)組的形式輸出該節(jié)點(diǎn).因此，traverse 可看成是增強(qiáng)了二元樹上的先序遍歷操作，允許在遍歷的過(guò)程中添加某些約束條件(如根據(jù)某個(gè)給定的數(shù)組對(duì)樹中的元素進(jìn)行判斷)，并產(chǎn)生相應(yīng)的輸出和計(jì)算副作用.

根據(jù)定義14，traverse 是從monadic R［A］－代數(shù)A×BTree(A))×［A］→［A］×［A］)到(［A］，φ［A］=［tnil，tconcat］:(1 +［A］×A ×［A］)×［A］→［A］×［A］)的pmfold 操作:pmfoldR(φ［A］):BTree(A)×［A］→［A］×［A］，其中參數(shù)A 為數(shù)組［A］，計(jì)算副作用封裝在積monad(Id ×［A］，η，－*)中，tnil(1，l)=〈［］，［］〉，tconcat((b1，a，b2)，l)=if isin(a，l)then〈a:b1::b2，a:b1::b2〉else〈a:b1::b2，b1::b2〉.

類似地，二元(或多元)樹及圖上的各種遍歷(如中序或后序)操作都可擴(kuò)展為相應(yīng)的pmfold 操作.

例4 ［A］上的函數(shù)filter:［A］×［A］→［A］×［A］定義為:

顯然，filter 表示根據(jù)給定的數(shù)組參數(shù)對(duì)另一個(gè)數(shù)組中的元素進(jìn)行過(guò)濾，并按原順序返回剩余的元素，同時(shí)以數(shù)組的形式輸出被過(guò)濾的元素.filter 可看成是從(［A］，φ［A］=［tnil，tconcat］)到(［A］，φ［A］'=［fnil，fconcat］)的monadic R［A］－ 代數(shù)同態(tài)射，其中fnil(［］，l)=〈［］，［］〉，fconcat(a:b1::b2，l)=if isin(a，l)then〈b1::b2，a:b1::b2〉else〈a:b1::b2，b1::b2〉.

用定律5 可將filter 和例3 中的traverse 函數(shù)融合在一起:ftree=filtertraverse:BTree(A)×［A］→［A］×［A］，且ftree 定義為:

else〈a:ftree(b1，l)::ftree(b2，l)，ftree(b1，l)::ftree(b2，l)〉.

函數(shù)ftree 表示對(duì)二元樹進(jìn)行先序遍歷，且在遍歷的過(guò)程中根據(jù)給定的數(shù)組對(duì)二元樹中的元素進(jìn)行過(guò)濾，并以數(shù)組的形式輸出遍歷結(jié)果和被過(guò)濾的元素.由定律5 可知ftree 為pmfold 操作ftree=pmfoldR(φ［A］').

5 結(jié)語(yǔ)

文中的主要貢獻(xiàn)包括以下兩點(diǎn):

(1)證明了分配范疇上某些代數(shù)函子的初始代數(shù)在合適的條件上是monadic 強(qiáng)初始的，給出monadic 強(qiáng)歸納數(shù)據(jù)類型及其上帶固定參數(shù)且包含計(jì)算副作用的遞歸操作pmfold 的定義;

(2)給出pmfold 上部分典型的范疇論性質(zhì)及計(jì)算律，并分析了它與一般fold、pfold 和monadic fold之間的關(guān)系.

對(duì)帶固定參數(shù)且包含計(jì)算副作用的遞歸操作的研究有助于進(jìn)一步提高遞歸操作對(duì)復(fù)雜計(jì)算的描述能力，促進(jìn)歸納數(shù)據(jù)類型在程序語(yǔ)言設(shè)計(jì)、轉(zhuǎn)換及優(yōu)化等方面的應(yīng)用，并提高程序設(shè)計(jì)的模塊性、隔離性和靈活性.

下一步將研究如何把文中工作擴(kuò)展到包含累積參數(shù)的遞歸計(jì)算中，并探討monads 對(duì)計(jì)算副作用的結(jié)構(gòu)化描述以及comonads 對(duì)計(jì)算上下文的結(jié)構(gòu)化描述間的有機(jī)結(jié)合.

［1］Greiner J.Programming with inductive and co-inductive types［R］.Pittsburgh:Carnegie-Mellon University，1992:22-29.

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

［3］Cockett J R B，Spencer D.Strong categorical datatypes I［C］∥Proceedings of International Meeting on Category Theory 1991.Ottawa:Canadian Mathematical Society，1991:141-169.

［4］Cockett J R B，Spencer D.Strong categorical datatypes II:a term logic for categorical programming［J］.Theoretical Computer Science，1995，139(1):69-113.

［5］Pardo A.A calculational approach to strong datatypes［R］.Oslo:Department of Informatics，University of Oslo，1997.

［6］Pardo A.Towards merging recursion and comonads［R］.Utrecht:University of Utrecht，2000:50-68.

［7］Pardo A.Generic accumulations［C］∥Proceedings of IFIP TC2/WG2.1 Working Conference on Generic Programming.New York:ACM，2003:49-78.

［8］蘇錦鈿，余珊珊.廣義共迭代及其計(jì)算律［J］.華南理工大學(xué)學(xué)報(bào):自然科學(xué)版，2012，40(9):62-68.Su Jin-dian，Yu Shan-shan.Generalised coiteration and its calculation laws［J］.Journal of South China University of Technology:Natural Science Edition，2012，40(9):62-68.

［9］蘇錦鈿，余珊珊.帶參數(shù)的共遞歸操作及其計(jì)算定律［J］.計(jì)算機(jī)研究與發(fā)展，2013，50(12):2672-2690.Su Jin-dian，Yu Shan-shan.Corecursive operations with parameters and their computation laws［J］.Journal of Computer Research and Development，2013，50(12):2672-2690.

［10］余珊珊，李師賢，蘇錦鈿.一種帶參數(shù)的Hylomorphisms及其計(jì)算律［J］.計(jì)算機(jī)研究與發(fā)展，2013，50(3):602-618.Yu Shan-shan，Li Shi-xian，Su Jin-dian.Hylomorphisms with parameters and its associated calculational laws［J］.Journal of Computer Research and Development，2013，50(3):602-618.

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

［12］Fokkinga M M.Monadic maps and folds for arbitrary datatypes［R］.Twente:University of Twente，1994.

［13］Hu Z，Iwasaki H.Promotional transformation of monadic programs［C］∥Proceedings of Fuji International Workshop on Functional and Logic Programming.Singapore:World Scientific，1995:196-210.

［14］Meijer E，Jeuring J.Merging monads and folds for functional programming［C］∥Proceedings of LNCS 925:Advanced Functional Programming.Berlin:Springer，1995:228-266.

［15］Pardo A.Monadic corecursion-definition，fusion laws，and applications［J］.Electronic Notes in Theoretical Computer Science，1998，11(1):105-139.

［16］Ghani N，Johann P，Uustalu T，et al.Monadic augment and generalised short cut fusion ［J］.Journal of Functional Programming，2007，17(6):731-776.

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

［18］Vene V.Categorical programming with inductive and coinductive types［D］.Estonia:Institute of Computer Science，University of Tartu，2000:22-31.

［19］Walters R F C.Data types in distributive categories［J］.Bulletion of the Australian Mathematical Society，1989，40(1):79-82.

［20］Kock A.Strong functors and monoidal monads［J］.Archiv der Mathematik，1972，23(1):113-120.

［21］Barr M，Wells C.Category theory for computing science［M］.2nd ed.Montréal:Centre De Recherches Mathematiques，1999.