第第6章章 递归类型递归类型递归定义的类型的例子递归定义的类型的例子自然数表的类型自然数表的类型类型等式类型等式 t unit + (nat t)的一个解的一个解二叉树的类型二叉树的类型类型等式类型等式 t unit + (t t)的一个解的一个解使用使用“ ”表示解是要使两边同构，而不是相等表示解是要使两边同构，而不是相等归纳类型对应到归纳类型对应到上述上述类型同构等式的初始解类型同构等式的初始解例：自然数类型例：自然数类型余归纳类型对应到它们的终结解余归纳类型对应到它们的终结解例：自然数流类型例：自然数流类型6.1 引引 言言本章的主要内容本章的主要内容直观地介绍余归纳的定义、余归纳的证明原直观地介绍余归纳的定义、余归纳的证明原理和余代数理和余代数形式地介绍递归类型形式地介绍递归类型形式地介绍归纳类型和余归纳类型形式地介绍归纳类型和余归纳类型解释解释代数方法是从代数方法是从“构造的构造的”角度研究抽象数据类型角度研究抽象数据类型余代数方法是从余代数方法是从“观察的观察的”的角度描述的角度描述像像对象、对象、自动机、进程、软件构件等基于状态的系统。自动机、进程、软件构件等基于状态的系统。6.2 归纳和余归纳归纳和余归纳6.2.1 余归纳现象余归纳现象例例数据集数据集A上的有限表集可归纳地定义如下上的有限表集可归纳地定义如下(1) 基础情况：基础情况：nil是有限表是有限表(2) 迭代规则：迭代规则：若若a A且且 是有限表，则是有限表，则cons(a, )是是有限表有限表(3) 最小化条件：此外，有限表集中不含其它元素最小化条件：此外，有限表集中不含其它元素最小化规则指所定义的集合是满足最小化规则指所定义的集合是满足(1)和和(2)两条两条约束的最小集合，约束的最小集合，无无任何垃圾在其中任何垃圾在其中6.2 归纳和余归纳归纳和余归纳例例数据集数据集A上的无限表集（流）可余归纳地定义如下上的无限表集（流）可余归纳地定义如下(1) 迭代规则：迭代规则：若若a A且且 是无限表，则是无限表，则cons(a, )是无限表是无限表(2) 最大化条件：数据集最大化条件：数据集A上的无限表集是满足迭代上的无限表集是满足迭代规则的最大集合规则的最大集合最大化条件表示所有未被最大化条件表示所有未被(1)排除的元素都被包排除的元素都被包含在所定义的集合中，即该集合中任何无限表都可含在所定义的集合中，即该集合中任何无限表都可以通过应用规则以通过应用规则(1)若干次（可能是无限次）而得到若干次（可能是无限次）而得到6.2 归纳和余归纳归纳和余归纳比较比较两种表两种表都有观察算子都有观察算子head和运算算子和运算算子tail head(cons(a, ) = a tail(cons(a, ) = 计算计算有限表有限表表长的函数表长的函数length length(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( ) 用等式演算可得用等式演算可得 head(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、互模拟、互模拟余归纳证明专用方法余归纳证明专用方法从数学上刻画系统（如对象、进程等）行为等价从数学上刻画系统（如对象、进程等）行为等价这个直观概念这个直观概念指两个系统从观测者角度看，可以互相模拟对方指两个系统从观测者角度看，可以互相模拟对方的行为的行为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(odd( ), even( ) = 互模拟是满足下面条件的关系互模拟是满足下面条件的关系R： 若若 , R，则，则 head( ) = head( ) 并且并且 tail( ), tail( ) R 基于互模拟的余归纳证明原理是：基于互模拟的余归纳证明原理是： 对互模拟关系对互模拟关系R，若，若 , R，则，则 = 定义关系定义关系 R = merge(odd( ), even( ), | 是一个无限表是一个无限表只要证明只要证明R是互模拟关系即可是互模拟关系即可 6.2 归纳和余归纳归纳和余归纳 对于第一个条件对于第一个条件 head(merge(odd( ), even( ) = head(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、利用归纳和等式演算，也可以证明、利用归纳和等式演算，也可以证明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 归纳和余归纳指南归纳和余归纳指南从集合论角度介绍余归纳定义和余归纳证明从集合论角度介绍余归纳定义和余归纳证明原理原理略去不介绍略去不介绍6.2 归纳和余归纳归纳和余归纳6.2.3 代数和余代数代数和余代数从从普普通通算算法法到到交交互互计计算算的的转转变变在在数数学学上上表表现现为一系列的扩展为一系列的扩展 从归纳到余归纳的扩展从归纳到余归纳的扩展表达了从字符串到流的转变表达了从字符串到流的转变 从良基集到非良基集的扩展从良基集到非良基集的扩展非良基集作为流的行为的形式模型被引入非良基集作为流的行为的形式模型被引入 从代数到余代数的扩展从代数到余代数的扩展余余代代数数为为流流的的演演算算提提供供工工具具，它它相相当当于于 演演算算在在图灵计算模型中的地位图灵计算模型中的地位6.2 归纳和余归纳归纳和余归纳交换图表交换图表可用来表达函数之间的等式可用来表达函数之间的等式 f, g (z) = f (z), g(z) f, g(w) = 二元积的交换图表二元积的交换图表YZ f, g X YXProj1gfProj2Zf, gX + YXYInleftgfInright二元和的交换图表二元和的交换图表6.2 归纳和余归纳归纳和余归纳范畴论基本知识范畴论基本知识 1、范畴举例、范畴举例 所有的集合和它们之间的函数构成一个范畴所有的集合和它们之间的函数构成一个范畴 所有的代数和它们之间的代数同态构成一个范畴所有的代数和它们之间的代数同态构成一个范畴 所有的图和它们之间的图同态构成一个范畴所有的图和它们之间的图同态构成一个范畴2、范畴的对象和射、范畴的对象和射 每个集合是范畴的一个对象每个集合是范畴的一个对象表示为图表上的一个节点表示为图表上的一个节点 每个函数是相应两个对象之间的射每个函数是相应两个对象之间的射表示为图表上的一条有向边表示为图表上的一条有向边6.2 归纳和余归纳归纳和余归纳3、对象和射构成范畴的条件、对象和射构成范畴的条件 射是可以合成的射是可以合成的函数可以合成，代数同态和图同态可以合成函数可以合成，代数同态和图同态可以合成 射的合成满足结合律射的合成满足结合律函数和同态的合成有性质函数和同态的合成有性质(h g) f = h (g f) 每个对象都有一个恒等射每个对象都有一个恒等射每个集合（代数）都有一个恒等函数（同态）每个集合（代数）都有一个恒等函数（同态） 若若f : A B是对象是对象A到到B的射，的射，idA和和idB分别表示分别表示A和和B的恒等射，的恒等射，表示射的合成运算，那么表示射的合成运算，那么f idA = idB f = f 显然恒等函数和恒等同态都满足该性质显然恒等函数和恒等同态都满足该性质6.2 归纳和余归纳归纳和余归纳4、函子、函子 范畴之间保结构的映射范畴之间保结构的映射 以集合范畴到它自身的映射为例，满足下面以集合范畴到它自身的映射为例，满足下面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 ) 下面都用下面都用F，根据参数，根据参数可知道它是可知道它是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+ N1NInleftS0Inright6.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 + (tre