第6章递归类型

1、第第6章章 递归类型递归类型 递归定义的类型的例子递归定义的类型的例子 自然数表的类型自然数表的类型类型等式类型等式 t unit + (nat t)的一个解的一个解 二叉树的类型二叉树的类型类型等式类型等式 t unit + (t t)的一个解的一个解使用使用“ ”表示解是要使两边同构，而不是相等表示解是要使两边同构，而不是相等归纳类型对应到归纳类型对应到上述上述类型同构等式的初始解类型同构等式的初始解例：自然数类型例：自然数类型余归纳类型对应到它们的终结解余归纳类型对应到它们的终结解例：自然数流类型例：自然数流类型6.1 引引 言言本章的主要内容本章的主要内容 直观地介绍余归纳的定义、余归

2、纳的证明原直观地介绍余归纳的定义、余归纳的证明原理和余代数理和余代数 形式地介绍递归类型形式地介绍递归类型 形式地介绍归纳类型和余归纳类型形式地介绍归纳类型和余归纳类型 解释解释 代数方法是从代数方法是从“构造的构造的”角度研究抽象数据类型角度研究抽象数据类型 余代数方法是从余代数方法是从“观察的观察的”的角度描述的角度描述像像对象、对象、自动机、进程、软件构件等基于状态的系统。自动机、进程、软件构件等基于状态的系统。6.2 归纳和余归纳归纳和余归纳6.2.1 余归纳现象余归纳现象 例例数据数据集集A上的有限表集可归纳地定义上的有限表集可归纳地定义如下如下(1) 基础基础情况：情况：nil是有

3、限是有限表表(2) 迭代迭代规则规则：若若a A且且 是有限表，则是有限表，则cons(a, )是是有限有限表表(3) 最小最小化条件化条件：此外：此外，有限表集中不含其它，有限表集中不含其它元素元素最小最小化化规则指规则指所定义的集合是所定义的集合是满足满足(1)和和(2)两条两条约束约束的最小集合的最小集合，无无任何垃圾在其中任何垃圾在其中6.2 归纳和余归纳归纳和余归纳 例例数据集数据集A上的无限表集（流）可余归纳地定义如下上的无限表集（流）可余归纳地定义如下(1) 迭代规则：迭代规则：若若a A且且 是无限表，则是无限表，则cons(a, )是是无限表无限表(2) 最大化条件：数据集最

4、大化条件：数据集A上的无限表集是满足迭代上的无限表集是满足迭代规则的最大集合规则的最大集合最大化条件表示所有未被最大化条件表示所有未被(1)排除的元素都被包排除的元素都被包含在所定义的集合中，即该集合中任何无限表都可含在所定义的集合中，即该集合中任何无限表都可以通过应用规则以通过应用规则(1)若干次（可能是无限次）而得到若干次（可能是无限次）而得到6.2 归纳和余归纳归纳和余归纳 比较比较 两种表两种表都有观察算子都有观察算子head和运算算子和运算算子tail head(cons(a, ) = a tail(cons(a, ) = 计算计算有限表有限表表长的函数表长的函数length len

5、gth(nil) = 0 length(cons(a, ) = 1 + length( ) 若若有函数有函数f : A A，定义，定义其应用到无限表所有元其应用到无限表所有元素的素的拓展函数拓展函数ext(f ) head(ext(f )( ) = f (head( ) tail(ext(f )( ) = ext(f )(tail( )6.2 归纳和余归纳归纳和余归纳 例例无限表无限表上的上的odd运算运算（忽略所有（忽略所有偶数位置的元素偶数位置的元素） head(odd( ) = head( ) tail(odd( ) = odd(tail(tail( ) 用等式演算可得用等式演算可得 h

6、ead(tail(odd( ) = head(odd(tail(tail( ) = head(tail(tail( ) 不难证明，对所有的自然数不难证明，对所有的自然数n head(tail(n) (odd( ) = head(tail(2n) ( )6.2 归纳和余归纳归纳和余归纳 余归纳定义的数据和函数的性质证明余归纳定义的数据和函数的性质证明1、可以用归纳法来证明可以用归纳法来证明，例如证明，例如证明head(tail(n) (odd( ) = head(tail(2n) ( )2、互模拟、互模拟余归纳证明专用方法余归纳证明专用方法 从数学上刻画系统（如对象、进程等）行为等价从数学上刻画

7、系统（如对象、进程等）行为等价这个直观概念这个直观概念 指两个系统从观测者角度看，可以互相模拟对方指两个系统从观测者角度看，可以互相模拟对方的行为的行为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( ) = 互模拟是满足下面条件的关系互模拟是满足下面条件的关系R： 若若 , R，则，则 head( ) = head( ) 并且并且 tail( ), tail( ) R 基于互模拟的余归纳证明原理是：基于互模拟的余归纳证明原理是： 对互模拟关系对互模拟关系R，若，若 , R，则，则 = 定义关系定义关系 R = merge(odd( ), even( ), | 是一个无限表是一个无限表 只要证明只要证明R是互模拟关系即可是互模拟关系即可 6.2 归纳和余归纳归纳和余归纳 对于第一个条件对于第一个条件 head(merge(odd( ), even( ) = he

9、ad(odd( ) = head( ) 对于第二个条件对于第二个条件需证需证 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( ) = 需用归纳法先证明下面几个等式：需用归纳法先证明下面几个等式：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 代数和余代数代数和余代数 从普通算法到交互计算的转变在数学上表现从普通算法到交互计算的转变在数学上表现为一系列的扩展为一系列的扩展 从归纳到余归纳的扩展从归纳到余归纳的扩展表达了从字符串到流的转变表达了从字符串到流的转变 从良基集到非良基集的扩展从良基集到非良基集的扩展非良基集作为流的行为的形式模型被引入非良基集作为流的行为的形式模型被引入 从代数到余代数的扩展从代数到余代数的扩展余代数为流的演算提供工具，它相当于余

12、代数为流的演算提供工具，它相当于 演算在演算在图灵计算模型中的地位图灵计算模型中的地位6.2 归纳和余归纳归纳和余归纳 交换图表交换图表可用来表达函数之间的等式可用来表达函数之间的等式 f, g (z) = f (z), g(z) f, g(w) = 二元积的交换图表二元积的交换图表YZ f, g X YXProj1gfProj2Zf, gX + YXYInleftgfInright二元和的交换图表二元和的交换图表( ) 0,( ) 1,f xwxg ywy如果如果6.2 归纳和余归纳归纳和余归纳 范畴论基本知识范畴论基本知识 1、范畴举例、范畴举例 所有的集合和它们之间的函数构成一个范畴所有

13、的集合和它们之间的函数构成一个范畴 所有的代数和它们之间的代数同态构成一个范畴所有的代数和它们之间的代数同态构成一个范畴 所有的图和它们之间的图同态构成一个范畴所有的图和它们之间的图同态构成一个范畴2、范畴的对象和射、范畴的对象和射 每个集合是范畴的一个对象每个集合是范畴的一个对象表示为图表上的一个节点表示为图表上的一个节点 每个函数是相应两个对象之间的射每个函数是相应两个对象之间的射表示为图表上的一条有向边表示为图表上的一条有向边6.2 归纳和余归纳归纳和余归纳3、对象和射构成范畴的条件、对象和射构成范畴的条件 射是可以合成的射是可以合成的函数可以合成，代数同态和图同态可以合成函数可以合成，

14、代数同态和图同态可以合成 射的合成满足结合律射的合成满足结合律函数和同态的合成有性质函数和同态的合成有性质(h g) f = h (g f) 每个对象都有一个恒等射每个对象都有一个恒等射每个集合（代数）都有一个恒等函数（同态）每个集合（代数）都有一个恒等函数（同态） 若若f : A B是对象是对象A到到B的射，的射，idA和和idB分别表示分别表示A和和B的恒等射，的恒等射，表示射的合成运算，那么表示射的合成运算，那么f idA = idB f = f 显然恒等函数和恒等同态都满足该性质显然恒等函数和恒等同态都满足该性质6.2 归纳和余归纳归纳和余归纳4、函子、函子 范畴之间保结构的映射范畴之

15、间保结构的映射 以集合范畴到它自身的映射为例，满足下面以集合范畴到它自身的映射为例，满足下面3个个条件的映射条件的映射F 称为函子，其中的称为函子，其中的F0 将集合映射到集将集合映射到集合，合，F1将函数映射到函数将函数映射到函数 (1) 若若f : A B在集合范畴中，在集合范畴中，则则F1(f ) : F0(A) F0(B)也在集合范畴中也在集合范畴中 (2) 对任何集合对任何集合A，F1(idA) = (3) 若若f : A B和和g : B C都在集合范畴中，都在集合范畴中， 则则F1(g f ) = F1(g) F1(f )0( )FAid 下面都用下面都用F，根据参数，根据参数可

16、知道它是可知道它是F0还是还是F16.2 归纳和余归纳归纳和余归纳 基于函子来定义单类代数基于函子来定义单类代数 令令F是函子，是函子，F的一个代数（简称的一个代数（简称F代数）是一个代数）是一个序对序对 U, a ，其中，其中U是集合，称为该代数的载体，是集合，称为该代数的载体，a是函数是函数a : F(U) U，称为该代数的代数结构（也，称为该代数的代数结构（也称为运算）称为运算） 例：自然数例：自然数 自然数上的零和后继函数自然数上的零和后继函数0 : 1 N 和和S : N N 形成形成函子函子F(X) =1+X 的的F代数代数 N, 0, S : 1+N N N0, S 1+ N1N

17、InleftS0Inright6.2 归纳和余归纳归纳和余归纳 例：二叉树例：二叉树 以集合以集合A的元素标记节点的二叉树的集合用的元素标记节点的二叉树的集合用tree(A)表示表示 空树空树nil可用函数可用函数nil : 1 tree(A)表示表示 node : tree(A) A tree(A) tree(A)表示从两棵表示从两棵子树和一个节点标记构造一棵树子树和一个节点标记构造一棵树 nil和和node形成函子形成函子F(X) =1+ (X A X)的一个代的一个代数数nil, node : 1 + (tree(A) A tree(A) tree(A) 6.2 归纳和余归纳归纳和余归纳

18、 用函子和交换图表来表示代数同态用函子和交换图表来表示代数同态令令 F是函子是函子 a : F(U) U和和b : F(V) V是两个函数是两个函数 则则F代数代数 U, a 到到 V, b 的的同态是函数同态是函数f : U V，满足满足f a = b F(f ) 可进一步定义初始代数可进一步定义初始代数 F(f )F(U)UVbafF(V)6.2 归纳和余归纳归纳和余归纳 定义余代数定义余代数 令令F是函子，是函子，F的一个余代数（简称的一个余代数（简称F余代数）余代数）是一个序对是一个序对 U, c ，其中，其中 U是集合，称为该余代数的载体是集合，称为该余代数的载体 c是函数是函数c

19、: U F(U)，称为该余代数的余代数称为该余代数的余代数结构（也称为运算）结构（也称为运算）由于余代数经常描述由于余代数经常描述动态系统，载体也叫做动态系统，载体也叫做状态空间状态空间Z f, g X YXYProj1gfProj26.2 归纳和余归纳归纳和余归纳 余代数和代数的区别余代数和代数的区别本质上这是构造和观察之间的区别本质上这是构造和观察之间的区别 代数由载体集合代数由载体集合U和射入和射入U的函数的函数a : F(U) U 组组成，它告知怎样构造成，它告知怎样构造U的元素的元素 余代数由载体集合余代数由载体集合U和逆向的函数和逆向的函数c : U F(U)组组成，此时不知道怎样

20、形成成，此时不知道怎样形成U的元素，仅有作用在的元素，仅有作用在U上的操作，它给出关于上的操作，它给出关于U的某些信息的某些信息6.2 归纳和余归纳归纳和余归纳 用函子和交换图表来表示余代数同态用函子和交换图表来表示余代数同态令令 F是函子是函子 a : U F(U)和和b : V F(V)是两个函数是两个函数则则 F余代数余代数 V, b 到到 U, a 的的同态是一个函数同态是一个函数f : V U，满足满足a f = F(f ) b 可进一步定义终结代数可进一步定义终结代数F(f )F(U)UVbafF(V)6.2 归纳和余归纳归纳和余归纳 例：例：考虑有两个按键考虑有两个按键value

21、和和next的机器的机器 可以用状态空间可以用状态空间U上的余代数上的余代数 value, next : U A U来描述，其中来描述，其中 value, next 由两个函数由两个函数value : U A和和next : U U组成组成 连续地交替按连续地交替按next键和键和value键，可以产生无限序键，可以产生无限序列列(a1, a2, ) 它可以看成它可以看成N A上的一个函数，其中上的一个函数，其中ai = value(next(i)(u) A6.3 递递 归归 类类 型型6.3.1 递归类型总揽递归类型总揽 在在PCF的类型中加入递归类型的类型中加入递归类型 := b | t

22、| unit | + | | | t. 其中其中t是类型变量是类型变量 t. 的解释的解释在递归的类型定义在递归的类型定义t = 中，中，引入引入fix( t. ) 来表示等式来表示等式t = 的一个解，的一个解，用用 t. 作为作为fix( t. )的语法美化的语法美化 类型表达式中出现变量会导致多态性，目前限于类型表达式中出现变量会导致多态性，目前限于闭表达式闭表达式6.3 递递 归归 类类 型型 类型相等问题类型相等问题对类型等式对类型等式t = 有两种可能的解释有两种可能的解释 等式左右两边是真正不可区分的类型等式左右两边是真正不可区分的类型这时类型相等变得相当复杂，因为这时类型相等变

23、得相当复杂，因为t = 意味着意味着t = t 把等式把等式t = 看成要找到类型看成要找到类型t，它和，它和 同构同构 t. t. t 注：注：fix( t. ) t. (fix( t. )在同构观点下，类型在同构观点下，类型 t. 并不等于并不等于 t. t ，但，但存在把存在把 t. 的项的项“转换转换”成成 t. t 的项的函数，的项的函数，反之亦然反之亦然6.3 递递 归归 类类 型型 PCF语言语言中递归类型的中递归类型的定型规则定型规则 ( Intro) ( Elim) 函数函数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 递递 归归 类类 型型 递归类型的急切归约规则递归类型的急切归约规则值值如果如果V是值，则是值，则fold V也是值也是值公理公理unfold(fold V) eager V， V是值是值子项规则子项规则函数函数 增加了递归类型的增加了递归类型的PCF语言仍有安全性定理语言仍有安全性定理M eager M fold M eager fold M M eager M unfold M eager unfold M 6.3 递递

25、 归归 类类 型型6.3.2 递归的数据结构递归的数据结构 递归类型在程序设计语言中有很多应用递归类型在程序设计语言中有很多应用 表示像表和树这样的无界数据结构表示像表和树这样的无界数据结构 表示像循环图这样的带环数据结构表示像循环图这样的带环数据结构 支持动态定型和动态类型派遣（支持动态定型和动态类型派遣（type dispatch） 支持协同例程和类似的控制结构支持协同例程和类似的控制结构6.3 递递 归归 类类 型型 自然数表类型的递归定义自然数表类型的递归定义 t unit + (nat t) 该类型方程的解是函数该类型方程的解是函数 list的一个不动点的一个不动点fix( list

26、) list t.unit + (nat t) 这时的这时的fold和和unfold函数的类型是函数的类型是fold : unit + (nat t) t，和，和unfold : t unit + (nat t) 二叉树类型的递归定义二叉树类型的递归定义t unit + (t t)6.3 递递 归归 类类 型型 自然数类型的递归定义自然数类型的递归定义nat unit + nat 把把nat作为递归类型的一个定义作为递归类型的一个定义nat t.unit + t 注注: t.unit + t = fix( t.unit + t ) 可以通过下面的同构来理解这个定义可以通过下面的同构来理解这个定

27、义nat unit + nat unit + (unit + nat) unit + (unit + (unit + nat) unit+(unit+(unit+(unit+(unit+nat) 6.3 递递 归归 类类 型型 自然数类型的递归定义自然数类型的递归定义nat unit+(unit+(unit+(unit+(unit+nat) 自然数自然数0和和1的定义如下的定义如下 0 fold(Inleft ) 1 fold(Inright fold(Inleft ) 对任何自然数对任何自然数n 0，可以类似地定义如下，可以类似地定义如下 n fold(Inright fold(Inrigh

28、tfold(Inleft ) 后继函数正好使用后继函数正好使用fold和和Inright：succ x:nat. fold(Inright x)6.3 递递 归归 类类 型型 自然数表的类型自然数表的类型list unit + (nat list)list t.unit + (nat t)nil fold(Inleft )cons x l fold(Inright x, l )根据表的形式进行分支的函数根据表的形式进行分支的函数listcase定义如下定义如下listcase x:list. y: . f:list .Caseunit, list, (unfold x) ( w:unit.y)

29、 (f )6.4 归纳类型和余归纳类型归纳类型和余归纳类型6.4.1 归纳类型和余归纳类型总揽归纳类型和余归纳类型总揽 归纳类型归纳类型 对应到某个类型同构等式的最小解，也叫初始解对应到某个类型同构等式的最小解，也叫初始解 被看成是包含它们引入形式的被看成是包含它们引入形式的“最小最小”类型；而类型；而其消去形式是在这引入形式上的一种递归形式其消去形式是在这引入形式上的一种递归形式 自然数类型：包含引入形式自然数类型：包含引入形式0和和succ(M)的最小类的最小类型，其中型，其中M也是引入形式也是引入形式 其他例子：串、表、树和任何其他可以看成从它其他例子：串、表、树和任何其他可以看成从它引

30、入形式有限地生成的类型引入形式有限地生成的类型6.4 归纳类型和余归纳类型归纳类型和余归纳类型 余归纳类型余归纳类型 对应到某个类型同构等式的最大解，也叫终结解对应到某个类型同构等式的最大解，也叫终结解 其引入形式是一种在消去形式需要时提供元素的其引入形式是一种在消去形式需要时提供元素的方法方法 自然数流类型：一个流可想象成处于由一个自然自然数流类型：一个流可想象成处于由一个自然数（它的头）和另一个流（它的尾）构成的序对的数（它的头）和另一个流（它的尾）构成的序对的生成过程中生成过程中 其他例子：正则树类型、惰性自然数类型其他例子：正则树类型、惰性自然数类型6.4 归纳类型和余归纳类型归纳类型

31、和余归纳类型 递归的类型同构式递归的类型同构式 考虑递归的类型同构式考虑递归的类型同构式t unit + t，并解释到集合，并解释到集合 t. 被称为类型抽象子，被看成集合范畴的函子被称为类型抽象子，被看成集合范畴的函子F(1) ( t. ) = unit + ，( t. ) = unit + (2) 扩展扩展 t. ，能将函数映射到函数，因而，能将函数映射到函数，因而称为称为F对任意的对任意的M : ，F(M): F( ) F( )定义为：定义为：F(M) = z: unit + .Case unit, , unit+ z ( x.unit:Inleftunit, ( ) ( y. : In

32、rightunit, (My) t 的解是一个类型的解是一个类型 ，使得，使得 和和F( )之间存在一之间存在一个同构，即个同构，即 是是F的不动点的不动点6.4 归纳类型和余归纳类型归纳类型和余归纳类型 类型抽象子类型抽象子F的最小解的最小解 对于对于f : F( ) ， , f 是一个是一个F代数，满足下面的代数，满足下面的交换图表交换图表 若若 , f 是初始是初始F代数，则代数，则 是是F的最小不动点的最小不动点 F的最小不动点用的最小不动点用 F表示表示 对初始对初始F代数就是代数就是最小不动点的理解需要最小不动点的理解需要回顾初始代数没有回顾初始代数没有“垃垃圾圾”的特点的特点F(h )F( ) g fhF( )6.4 归纳类型和余归纳类型归纳类型和余归纳类型 类型抽象子类型抽象子F的最大解的最大解 递归的类型同