第6章遞歸類型

1、第第6章章 遞歸類型遞歸類型 遞歸定義的類型的例子遞歸定義的類型的例子 自然數(shù)表的類型自然數(shù)表的類型類型等式類型等式 t unit + (nat t)的一個(gè)解的一個(gè)解 二叉樹的類型二叉樹的類型類型等式類型等式 t unit + (t t)的一個(gè)解的一個(gè)解使用使用“ ”表示解是要使兩邊同構(gòu)，而不是相等表示解是要使兩邊同構(gòu)，而不是相等歸納類型對(duì)應(yīng)到歸納類型對(duì)應(yīng)到上述上述類型同構(gòu)等式的初始解類型同構(gòu)等式的初始解例：自然數(shù)類型例：自然數(shù)類型余歸納類型對(duì)應(yīng)到它們的終結(jié)解余歸納類型對(duì)應(yīng)到它們的終結(jié)解例：自然數(shù)流類型例：自然數(shù)流類型6.1 引引 言言本章的主要內(nèi)容本章的主要內(nèi)容 直觀地介紹余歸納的定義、余歸

2、納的證明原直觀地介紹余歸納的定義、余歸納的證明原理和余代數(shù)理和余代數(shù) 形式地介紹遞歸類型形式地介紹遞歸類型 形式地介紹歸納類型和余歸納類型形式地介紹歸納類型和余歸納類型 解釋解釋 代數(shù)方法是從代數(shù)方法是從“構(gòu)造的構(gòu)造的”角度研究抽象數(shù)據(jù)類型角度研究抽象數(shù)據(jù)類型 余代數(shù)方法是從余代數(shù)方法是從“觀察的觀察的”的角度描述的角度描述像像對(duì)象、對(duì)象、自動(dòng)機(jī)、進(jìn)程、軟件構(gòu)件等基于狀態(tài)的系統(tǒng)。自動(dòng)機(jī)、進(jìn)程、軟件構(gòu)件等基于狀態(tài)的系統(tǒng)。6.2 歸納和余歸納歸納和余歸納6.2.1 余歸納現(xiàn)象余歸納現(xiàn)象 例例數(shù)據(jù)數(shù)據(jù)集集A上的有限表集可歸納地定義上的有限表集可歸納地定義如下如下(1) 基礎(chǔ)基礎(chǔ)情況：情況：nil是有

3、限是有限表表(2) 迭代迭代規(guī)則規(guī)則：若若a A且且 是有限表，則是有限表，則cons(a, )是是有限有限表表(3) 最小最小化條件化條件：此外：此外，有限表集中不含其它，有限表集中不含其它元素元素最小最小化化規(guī)則指規(guī)則指所定義的集合是所定義的集合是滿足滿足(1)和和(2)兩條兩條約束約束的最小集合的最小集合，無無任何垃圾在其中任何垃圾在其中6.2 歸納和余歸納歸納和余歸納 例例數(shù)據(jù)集數(shù)據(jù)集A上的無限表集（流）可余歸納地定義如下上的無限表集（流）可余歸納地定義如下(1) 迭代規(guī)則：迭代規(guī)則：若若a A且且 是無限表，則是無限表，則cons(a, )是是無限表無限表(2) 最大化條件：數(shù)據(jù)集最

4、大化條件：數(shù)據(jù)集A上的無限表集是滿足迭代上的無限表集是滿足迭代規(guī)則的最大集合規(guī)則的最大集合最大化條件表示所有未被最大化條件表示所有未被(1)排除的元素都被包排除的元素都被包含在所定義的集合中，即該集合中任何無限表都可含在所定義的集合中，即該集合中任何無限表都可以通過應(yīng)用規(guī)則以通過應(yīng)用規(guī)則(1)若干次（可能是無限次）而得到若干次（可能是無限次）而得到6.2 歸納和余歸納歸納和余歸納 比較比較 兩種表兩種表都有觀察算子都有觀察算子head和運(yùn)算算子和運(yùn)算算子tail head(cons(a, ) = a tail(cons(a, ) = 計(jì)算計(jì)算有限表有限表表長(zhǎng)的函數(shù)表長(zhǎng)的函數(shù)length len

5、gth(nil) = 0 length(cons(a, ) = 1 + length( ) 若若有函數(shù)有函數(shù)f : A A，定義，定義其應(yīng)用到無限表所有元其應(yīng)用到無限表所有元素的素的拓展函數(shù)拓展函數(shù)ext(f ) head(ext(f )( ) = f (head( ) tail(ext(f )( ) = ext(f )(tail( )6.2 歸納和余歸納歸納和余歸納 例例無限表無限表上的上的odd運(yùn)算運(yùn)算（忽略所有（忽略所有偶數(shù)位置的元素偶數(shù)位置的元素） head(odd( ) = head( ) tail(odd( ) = odd(tail(tail( ) 用等式演算可得用等式演算可得 h

6、ead(tail(odd( ) = head(odd(tail(tail( ) = head(tail(tail( ) 不難證明，對(duì)所有的自然數(shù)不難證明，對(duì)所有的自然數(shù)n head(tail(n) (odd( ) = head(tail(2n) ( )6.2 歸納和余歸納歸納和余歸納 余歸納定義的數(shù)據(jù)和函數(shù)的性質(zhì)證明余歸納定義的數(shù)據(jù)和函數(shù)的性質(zhì)證明1、可以用歸納法來證明可以用歸納法來證明，例如證明，例如證明head(tail(n) (odd( ) = head(tail(2n) ( )2、互模擬、互模擬余歸納證明專用方法余歸納證明專用方法 從數(shù)學(xué)上刻畫系統(tǒng)（如對(duì)象、進(jìn)程等）行為等價(jià)從數(shù)學(xué)上刻畫

7、系統(tǒng)（如對(duì)象、進(jìn)程等）行為等價(jià)這個(gè)直觀概念這個(gè)直觀概念 指兩個(gè)系統(tǒng)從觀測(cè)者角度看，可以互相模擬對(duì)方指兩個(gè)系統(tǒng)從觀測(cè)者角度看，可以互相模擬對(duì)方的行為的行為6.2 歸納和余歸納歸納和余歸納 例：無限表例：無限表1、定義、定義oddhead(odd( ) = head( )tail(odd( ) = odd(tail(tail( )2、定義、定義eveneven = odd tail3、定義、定義mergehead(merge( , ) = head( )tail(merge( , ) = merge( , (tail( )6.2 歸納和余歸納歸納和余歸納4、基于互模擬證明、基于互模擬證明merge

8、(odd( ), even( ) = 互模擬是滿足下面條件的關(guān)系互模擬是滿足下面條件的關(guān)系R： 若若 , R，則，則 head( ) = head( ) 并且并且 tail( ), tail( ) R 基于互模擬的余歸納證明原理是：基于互模擬的余歸納證明原理是： 對(duì)互模擬關(guān)系對(duì)互模擬關(guān)系R，若，若 , R，則，則 = 定義關(guān)系定義關(guān)系 R = merge(odd( ), even( ), | 是一個(gè)無限表是一個(gè)無限表 只要證明只要證明R是互模擬關(guān)系即可是互模擬關(guān)系即可 6.2 歸納和余歸納歸納和余歸納 對(duì)于第一個(gè)條件對(duì)于第一個(gè)條件 head(merge(odd( ), even( ) = he

9、ad(odd( ) = head( ) 對(duì)于第二個(gè)條件對(duì)于第二個(gè)條件需證需證 tail(merge(odd( ), even( ), tail( ) 也在也在R中，從下面等式證明可得中，從下面等式證明可得 tail(merge(odd( ), even( )= merge(even( ), tail(odd( )= merge(odd(tail( ), odd(tail(tail( )= merge(odd(tail( ), even(tail( ) merge(odd(tail( ), even(tail( ), tail( ) 在在R中中6.2 歸納和余歸納歸納和余歸納5、利用歸納和等式演

10、算，也可以證明、利用歸納和等式演算，也可以證明merge(odd( ), even( ) = 需用歸納法先證明下面幾個(gè)等式：需用歸納法先證明下面幾個(gè)等式：head(tail(n)(odd( ) = head(tail(2n)( )head(tail(2n)(merge( , ) = head(tail(n)( )head(tail(2n + 1)(merge( , ) = head(tail(n)( ) 然后利用等式演算證明然后利用等式演算證明head(tail(n)(merge(odd( ), even( ) = head(tail(n)( )6.2 歸納和余歸納歸納和余歸納6.2.2 歸納

11、和余歸納指南歸納和余歸納指南 從集合論角度介紹余歸納定義和余歸納證明從集合論角度介紹余歸納定義和余歸納證明原理原理 略去不介紹略去不介紹6.2 歸納和余歸納歸納和余歸納6.2.3 代數(shù)和余代數(shù)代數(shù)和余代數(shù) 從普通算法到交互計(jì)算的轉(zhuǎn)變?cè)跀?shù)學(xué)上表現(xiàn)從普通算法到交互計(jì)算的轉(zhuǎn)變?cè)跀?shù)學(xué)上表現(xiàn)為一系列的擴(kuò)展為一系列的擴(kuò)展 從歸納到余歸納的擴(kuò)展從歸納到余歸納的擴(kuò)展表達(dá)了從字符串到流的轉(zhuǎn)變表達(dá)了從字符串到流的轉(zhuǎn)變 從良基集到非良基集的擴(kuò)展從良基集到非良基集的擴(kuò)展非良基集作為流的行為的形式模型被引入非良基集作為流的行為的形式模型被引入 從代數(shù)到余代數(shù)的擴(kuò)展從代數(shù)到余代數(shù)的擴(kuò)展余代數(shù)為流的演算提供工具，它相當(dāng)于余

12、代數(shù)為流的演算提供工具，它相當(dāng)于 演算在演算在圖靈計(jì)算模型中的地位圖靈計(jì)算模型中的地位6.2 歸納和余歸納歸納和余歸納 交換圖表交換圖表可用來表達(dá)函數(shù)之間的等式可用來表達(dá)函數(shù)之間的等式 f, g (z) = f (z), g(z) f, g(w) = 二元積的交換圖表二元積的交換圖表YZ f, g X YXProj1gfProj2Zf, gX + YXYInleftgfInright二元和的交換圖表二元和的交換圖表( ) 0,( ) 1,f xwxg ywy如果如果6.2 歸納和余歸納歸納和余歸納 范疇論基本知識(shí)范疇論基本知識(shí) 1、范疇舉例、范疇舉例 所有的集合和它們之間的函數(shù)構(gòu)成一個(gè)范疇所有

13、的集合和它們之間的函數(shù)構(gòu)成一個(gè)范疇 所有的代數(shù)和它們之間的代數(shù)同態(tài)構(gòu)成一個(gè)范疇所有的代數(shù)和它們之間的代數(shù)同態(tài)構(gòu)成一個(gè)范疇 所有的圖和它們之間的圖同態(tài)構(gòu)成一個(gè)范疇所有的圖和它們之間的圖同態(tài)構(gòu)成一個(gè)范疇2、范疇的對(duì)象和射、范疇的對(duì)象和射 每個(gè)集合是范疇的一個(gè)對(duì)象每個(gè)集合是范疇的一個(gè)對(duì)象表示為圖表上的一個(gè)節(jié)點(diǎn)表示為圖表上的一個(gè)節(jié)點(diǎn) 每個(gè)函數(shù)是相應(yīng)兩個(gè)對(duì)象之間的射每個(gè)函數(shù)是相應(yīng)兩個(gè)對(duì)象之間的射表示為圖表上的一條有向邊表示為圖表上的一條有向邊6.2 歸納和余歸納歸納和余歸納3、對(duì)象和射構(gòu)成范疇的條件、對(duì)象和射構(gòu)成范疇的條件 射是可以合成的射是可以合成的函數(shù)可以合成，代數(shù)同態(tài)和圖同態(tài)可以合成函數(shù)可以合成，

14、代數(shù)同態(tài)和圖同態(tài)可以合成 射的合成滿足結(jié)合律射的合成滿足結(jié)合律函數(shù)和同態(tài)的合成有性質(zhì)函數(shù)和同態(tài)的合成有性質(zhì)(h g) f = h (g f) 每個(gè)對(duì)象都有一個(gè)恒等射每個(gè)對(duì)象都有一個(gè)恒等射每個(gè)集合（代數(shù)）都有一個(gè)恒等函數(shù)（同態(tài)）每個(gè)集合（代數(shù)）都有一個(gè)恒等函數(shù)（同態(tài)） 若若f : A B是對(duì)象是對(duì)象A到到B的射，的射，idA和和idB分別表示分別表示A和和B的恒等射，的恒等射，表示射的合成運(yùn)算，那么表示射的合成運(yùn)算，那么f idA = idB f = f 顯然恒等函數(shù)和恒等同態(tài)都滿足該性質(zhì)顯然恒等函數(shù)和恒等同態(tài)都滿足該性質(zhì)6.2 歸納和余歸納歸納和余歸納4、函子、函子 范疇之間保結(jié)構(gòu)的映射范疇之

15、間保結(jié)構(gòu)的映射 以集合范疇到它自身的映射為例，滿足下面以集合范疇到它自身的映射為例，滿足下面3個(gè)個(gè)條件的映射條件的映射F 稱為函子，其中的稱為函子，其中的F0 將集合映射到集將集合映射到集合，合，F(xiàn)1將函數(shù)映射到函數(shù)將函數(shù)映射到函數(shù) (1) 若若f : A B在集合范疇中，在集合范疇中，則則F1(f ) : F0(A) F0(B)也在集合范疇中也在集合范疇中 (2) 對(duì)任何集合對(duì)任何集合A，F(xiàn)1(idA) = (3) 若若f : A B和和g : B C都在集合范疇中，都在集合范疇中， 則則F1(g f ) = F1(g) F1(f )0( )FAid 下面都用下面都用F，根據(jù)參數(shù)，根據(jù)參數(shù)可

16、知道它是可知道它是F0還是還是F16.2 歸納和余歸納歸納和余歸納 基于函子來定義單類代數(shù)基于函子來定義單類代數(shù) 令令F是函子，是函子，F(xiàn)的一個(gè)代數(shù)（簡(jiǎn)稱的一個(gè)代數(shù)（簡(jiǎn)稱F代數(shù)）是一個(gè)代數(shù)）是一個(gè)序?qū)π驅(qū)?U, a ，其中，其中U是集合，稱為該代數(shù)的載體，是集合，稱為該代數(shù)的載體，a是函數(shù)是函數(shù)a : F(U) U，稱為該代數(shù)的代數(shù)結(jié)構(gòu)（也，稱為該代數(shù)的代數(shù)結(jié)構(gòu)（也稱為運(yùn)算）稱為運(yùn)算） 例：自然數(shù)例：自然數(shù) 自然數(shù)上的零和后繼函數(shù)自然數(shù)上的零和后繼函數(shù)0 : 1 N 和和S : N N 形成形成函子函子F(X) =1+X 的的F代數(shù)代數(shù) N, 0, S : 1+N N N0, S 1+ N1N

17、InleftS0Inright6.2 歸納和余歸納歸納和余歸納 例：二叉樹例：二叉樹 以集合以集合A的元素標(biāo)記節(jié)點(diǎn)的二叉樹的集合用的元素標(biāo)記節(jié)點(diǎn)的二叉樹的集合用tree(A)表示表示 空樹空樹nil可用函數(shù)可用函數(shù)nil : 1 tree(A)表示表示 node : tree(A) A tree(A) tree(A)表示從兩棵表示從兩棵子樹和一個(gè)節(jié)點(diǎn)標(biāo)記構(gòu)造一棵樹子樹和一個(gè)節(jié)點(diǎn)標(biāo)記構(gòu)造一棵樹 nil和和node形成函子形成函子F(X) =1+ (X A X)的一個(gè)代的一個(gè)代數(shù)數(shù)nil, node : 1 + (tree(A) A tree(A) tree(A) 6.2 歸納和余歸納歸納和余歸納

18、 用函子和交換圖表來表示代數(shù)同態(tài)用函子和交換圖表來表示代數(shù)同態(tài)令令 F是函子是函子 a : F(U) U和和b : F(V) V是兩個(gè)函數(shù)是兩個(gè)函數(shù) 則則F代數(shù)代數(shù) U, a 到到 V, b 的的同態(tài)是函數(shù)同態(tài)是函數(shù)f : U V，滿足滿足f a = b F(f ) 可進(jìn)一步定義初始代數(shù)可進(jìn)一步定義初始代數(shù) F(f )F(U)UVbafF(V)6.2 歸納和余歸納歸納和余歸納 定義余代數(shù)定義余代數(shù) 令令F是函子，是函子，F(xiàn)的一個(gè)余代數(shù)（簡(jiǎn)稱的一個(gè)余代數(shù)（簡(jiǎn)稱F余代數(shù)）余代數(shù)）是一個(gè)序?qū)κ且粋€(gè)序?qū)?U, c ，其中，其中 U是集合，稱為該余代數(shù)的載體是集合，稱為該余代數(shù)的載體 c是函數(shù)是函數(shù)c

19、: U F(U)，稱為該余代數(shù)的余代數(shù)稱為該余代數(shù)的余代數(shù)結(jié)構(gòu)（也稱為運(yùn)算）結(jié)構(gòu)（也稱為運(yùn)算）由于余代數(shù)經(jīng)常描述由于余代數(shù)經(jīng)常描述動(dòng)態(tài)系統(tǒng)，載體也叫做動(dòng)態(tài)系統(tǒng)，載體也叫做狀態(tài)空間狀態(tài)空間Z f, g X YXYProj1gfProj26.2 歸納和余歸納歸納和余歸納 余代數(shù)和代數(shù)的區(qū)別余代數(shù)和代數(shù)的區(qū)別本質(zhì)上這是構(gòu)造和觀察之間的區(qū)別本質(zhì)上這是構(gòu)造和觀察之間的區(qū)別 代數(shù)由載體集合代數(shù)由載體集合U和射入和射入U(xiǎn)的函數(shù)的函數(shù)a : F(U) U 組組成，它告知怎樣構(gòu)造成，它告知怎樣構(gòu)造U的元素的元素 余代數(shù)由載體集合余代數(shù)由載體集合U和逆向的函數(shù)和逆向的函數(shù)c : U F(U)組組成，此時(shí)不知道怎樣

20、形成成，此時(shí)不知道怎樣形成U的元素，僅有作用在的元素，僅有作用在U上的操作，它給出關(guān)于上的操作，它給出關(guān)于U的某些信息的某些信息6.2 歸納和余歸納歸納和余歸納 用函子和交換圖表來表示余代數(shù)同態(tài)用函子和交換圖表來表示余代數(shù)同態(tài)令令 F是函子是函子 a : U F(U)和和b : V F(V)是兩個(gè)函數(shù)是兩個(gè)函數(shù)則則 F余代數(shù)余代數(shù) V, b 到到 U, a 的的同態(tài)是一個(gè)函數(shù)同態(tài)是一個(gè)函數(shù)f : V U，滿足滿足a f = F(f ) b 可進(jìn)一步定義終結(jié)代數(shù)可進(jìn)一步定義終結(jié)代數(shù)F(f )F(U)UVbafF(V)6.2 歸納和余歸納歸納和余歸納 例：例：考慮有兩個(gè)按鍵考慮有兩個(gè)按鍵value

21、和和next的機(jī)器的機(jī)器 可以用狀態(tài)空間可以用狀態(tài)空間U上的余代數(shù)上的余代數(shù) value, next : U A U來描述，其中來描述，其中 value, next 由兩個(gè)函數(shù)由兩個(gè)函數(shù)value : U A和和next : U U組成組成 連續(xù)地交替按連續(xù)地交替按next鍵和鍵和value鍵，可以產(chǎn)生無限序鍵，可以產(chǎn)生無限序列列(a1, a2, ) 它可以看成它可以看成N A上的一個(gè)函數(shù)，其中上的一個(gè)函數(shù)，其中ai = value(next(i)(u) A6.3 遞遞 歸歸 類類 型型6.3.1 遞歸類型總攬遞歸類型總攬 在在PCF的類型中加入遞歸類型的類型中加入遞歸類型 := b | t

22、| unit | + | | | t. 其中其中t是類型變量是類型變量 t. 的解釋的解釋在遞歸的類型定義在遞歸的類型定義t = 中，中，引入引入fix( t. ) 來表示等式來表示等式t = 的一個(gè)解，的一個(gè)解，用用 t. 作為作為fix( t. )的語法美化的語法美化 類型表達(dá)式中出現(xiàn)變量會(huì)導(dǎo)致多態(tài)性，目前限于類型表達(dá)式中出現(xiàn)變量會(huì)導(dǎo)致多態(tài)性，目前限于閉表達(dá)式閉表達(dá)式6.3 遞遞 歸歸 類類 型型 類型相等問題類型相等問題對(duì)類型等式對(duì)類型等式t = 有兩種可能的解釋有兩種可能的解釋 等式左右兩邊是真正不可區(qū)分的類型等式左右兩邊是真正不可區(qū)分的類型這時(shí)類型相等變得相當(dāng)復(fù)雜，因?yàn)檫@時(shí)類型相等變

23、得相當(dāng)復(fù)雜，因?yàn)閠 = 意味著意味著t = t 把等式把等式t = 看成要找到類型看成要找到類型t，它和，它和 同構(gòu)同構(gòu) t. t. t 注：注：fix( t. ) t. (fix( t. )在同構(gòu)觀點(diǎn)下，類型在同構(gòu)觀點(diǎn)下，類型 t. 并不等于并不等于 t. t ，但，但存在把存在把 t. 的項(xiàng)的項(xiàng)“轉(zhuǎn)換轉(zhuǎn)換”成成 t. t 的項(xiàng)的函數(shù)，的項(xiàng)的函數(shù)，反之亦然反之亦然6.3 遞遞 歸歸 類類 型型 PCF語言語言中遞歸類型的中遞歸類型的定型規(guī)則定型規(guī)則 ( Intro) ( Elim) 函數(shù)函數(shù)fold和和unfold互逆，滿足下面的等式公理互逆，滿足下面的等式公理 unfold(fold M)

24、 = M fold(unfold M) = M M: t. /t fold M : t. M : t. unfold M : t. /t (fold/unfold)6.3 遞遞 歸歸 類類 型型 遞歸類型的急切歸約規(guī)則遞歸類型的急切歸約規(guī)則值值如果如果V是值，則是值，則fold V也是值也是值公理公理unfold(fold V) eager V， V是值是值子項(xiàng)規(guī)則子項(xiàng)規(guī)則函數(shù)函數(shù) 增加了遞歸類型的增加了遞歸類型的PCF語言仍有安全性定理語言仍有安全性定理M eager M fold M eager fold M M eager M unfold M eager unfold M 6.3 遞遞

25、 歸歸 類類 型型6.3.2 遞歸的數(shù)據(jù)結(jié)構(gòu)遞歸的數(shù)據(jù)結(jié)構(gòu) 遞歸類型在程序設(shè)計(jì)語言中有很多應(yīng)用遞歸類型在程序設(shè)計(jì)語言中有很多應(yīng)用 表示像表和樹這樣的無界數(shù)據(jù)結(jié)構(gòu)表示像表和樹這樣的無界數(shù)據(jù)結(jié)構(gòu) 表示像循環(huán)圖這樣的帶環(huán)數(shù)據(jù)結(jié)構(gòu)表示像循環(huán)圖這樣的帶環(huán)數(shù)據(jù)結(jié)構(gòu) 支持動(dòng)態(tài)定型和動(dòng)態(tài)類型派遣（支持動(dòng)態(tài)定型和動(dòng)態(tài)類型派遣（type dispatch） 支持協(xié)同例程和類似的控制結(jié)構(gòu)支持協(xié)同例程和類似的控制結(jié)構(gòu)6.3 遞遞 歸歸 類類 型型 自然數(shù)表類型的遞歸定義自然數(shù)表類型的遞歸定義 t unit + (nat t) 該類型方程的解是函數(shù)該類型方程的解是函數(shù) list的一個(gè)不動(dòng)點(diǎn)的一個(gè)不動(dòng)點(diǎn)fix( list

26、) list t.unit + (nat t) 這時(shí)的這時(shí)的fold和和unfold函數(shù)的類型是函數(shù)的類型是fold : unit + (nat t) t，和，和unfold : t unit + (nat t) 二叉樹類型的遞歸定義二叉樹類型的遞歸定義t unit + (t t)6.3 遞遞 歸歸 類類 型型 自然數(shù)類型的遞歸定義自然數(shù)類型的遞歸定義nat unit + nat 把把nat作為遞歸類型的一個(gè)定義作為遞歸類型的一個(gè)定義nat t.unit + t 注注: t.unit + t = fix( t.unit + t ) 可以通過下面的同構(gòu)來理解這個(gè)定義可以通過下面的同構(gòu)來理解這個(gè)定

27、義nat unit + nat unit + (unit + nat) unit + (unit + (unit + nat) unit+(unit+(unit+(unit+(unit+nat) 6.3 遞遞 歸歸 類類 型型 自然數(shù)類型的遞歸定義自然數(shù)類型的遞歸定義nat unit+(unit+(unit+(unit+(unit+nat) 自然數(shù)自然數(shù)0和和1的定義如下的定義如下 0 fold(Inleft ) 1 fold(Inright fold(Inleft ) 對(duì)任何自然數(shù)對(duì)任何自然數(shù)n 0，可以類似地定義如下，可以類似地定義如下 n fold(Inright fold(Inrigh

28、tfold(Inleft ) 后繼函數(shù)正好使用后繼函數(shù)正好使用fold和和Inright：succ x:nat. fold(Inright x)6.3 遞遞 歸歸 類類 型型 自然數(shù)表的類型自然數(shù)表的類型list unit + (nat list)list t.unit + (nat t)nil fold(Inleft )cons x l fold(Inright x, l )根據(jù)表的形式進(jìn)行分支的函數(shù)根據(jù)表的形式進(jìn)行分支的函數(shù)listcase定義如下定義如下listcase x:list. y: . f:list .Caseunit, list, (unfold x) ( w:unit.y)

29、 (f )6.4 歸納類型和余歸納類型歸納類型和余歸納類型6.4.1 歸納類型和余歸納類型總攬歸納類型和余歸納類型總攬 歸納類型歸納類型 對(duì)應(yīng)到某個(gè)類型同構(gòu)等式的最小解，也叫初始解對(duì)應(yīng)到某個(gè)類型同構(gòu)等式的最小解，也叫初始解 被看成是包含它們引入形式的被看成是包含它們引入形式的“最小最小”類型；而類型；而其消去形式是在這引入形式上的一種遞歸形式其消去形式是在這引入形式上的一種遞歸形式 自然數(shù)類型：包含引入形式自然數(shù)類型：包含引入形式0和和succ(M)的最小類的最小類型，其中型，其中M也是引入形式也是引入形式 其他例子：串、表、樹和任何其他可以看成從它其他例子：串、表、樹和任何其他可以看成從它引

30、入形式有限地生成的類型引入形式有限地生成的類型6.4 歸納類型和余歸納類型歸納類型和余歸納類型 余歸納類型余歸納類型 對(duì)應(yīng)到某個(gè)類型同構(gòu)等式的最大解，也叫終結(jié)解對(duì)應(yīng)到某個(gè)類型同構(gòu)等式的最大解，也叫終結(jié)解 其引入形式是一種在消去形式需要時(shí)提供元素的其引入形式是一種在消去形式需要時(shí)提供元素的方法方法 自然數(shù)流類型：一個(gè)流可想象成處于由一個(gè)自然自然數(shù)流類型：一個(gè)流可想象成處于由一個(gè)自然數(shù)（它的頭）和另一個(gè)流（它的尾）構(gòu)成的序?qū)Φ臄?shù)（它的頭）和另一個(gè)流（它的尾）構(gòu)成的序?qū)Φ纳蛇^程中生成過程中 其他例子：正則樹類型、惰性自然數(shù)類型其他例子：正則樹類型、惰性自然數(shù)類型6.4 歸納類型和余歸納類型歸納類型

31、和余歸納類型 遞歸的類型同構(gòu)式遞歸的類型同構(gòu)式 考慮遞歸的類型同構(gòu)式考慮遞歸的類型同構(gòu)式t unit + t，并解釋到集合，并解釋到集合 t. 被稱為類型抽象子，被看成集合范疇的函子被稱為類型抽象子，被看成集合范疇的函子F(1) ( t. ) = unit + ，( t. ) = unit + (2) 擴(kuò)展擴(kuò)展 t. ，能將函數(shù)映射到函數(shù)，因而，能將函數(shù)映射到函數(shù)，因而稱為稱為F對(duì)任意的對(duì)任意的M : ，F(xiàn)(M): F( ) F( )定義為：定義為：F(M) = z: unit + .Case unit, , unit+ z ( x.unit:Inleftunit, ( ) ( y. : In

32、rightunit, (My) t 的解是一個(gè)類型的解是一個(gè)類型 ，使得，使得 和和F( )之間存在一之間存在一個(gè)同構(gòu)，即個(gè)同構(gòu)，即 是是F的不動(dòng)點(diǎn)的不動(dòng)點(diǎn)6.4 歸納類型和余歸納類型歸納類型和余歸納類型 類型抽象子類型抽象子F的最小解的最小解 對(duì)于對(duì)于f : F( ) ， , f 是一個(gè)是一個(gè)F代數(shù)，滿足下面的代數(shù)，滿足下面的交換圖表交換圖表 若若 , f 是初始是初始F代數(shù)，則代數(shù)，則 是是F的最小不動(dòng)點(diǎn)的最小不動(dòng)點(diǎn) F的最小不動(dòng)點(diǎn)用的最小不動(dòng)點(diǎn)用 F表示表示 對(duì)初始對(duì)初始F代數(shù)就是代數(shù)就是最小不動(dòng)點(diǎn)的理解需要最小不動(dòng)點(diǎn)的理解需要回顧初始代數(shù)沒有回顧初始代數(shù)沒有“垃垃圾圾”的特點(diǎn)的特點(diǎn)F(h )F( ) g fhF( )6.4 歸納類型和余歸納類型歸納類型和余歸納類型 類型抽象子類型抽象子F的最大解的最大解 遞歸的類型同