【教学课件】第6章递归类型.ppt

《【教学课件】第6章递归类型.ppt》由会员分享，可在线阅读，更多相关《【教学课件】第6章递归类型.ppt（43页珍藏版）》请在得力文库 - 分享文档赚钱的网站上搜索。

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

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

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

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

5、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()不难证明，对所有的自然数不难证

6、明，对所有的自然数n head(tail(n)(odd()=head(tail(2n)()6.2 归纳和余归纳归纳和余归纳余归纳定义的数据和函数的性质证明余归纳定义的数据和函数的性质证明1、可以用归纳法来证明可以用归纳法来证明，例如证明，例如证明head(tail(n)(odd()=head(tail(2n)()2、互模拟、互模拟余归纳证明专用方法余归纳证明专用方法从数学上刻画系统（如对象、进程等）行为等价从数学上刻画系统（如对象、进程等）行为等价这个直观概念这个直观概念指两个系统从观测者角度看，可以互相模拟对方指两个系统从观测者角度看，可以互相模拟对方的行为的行为6.2 归纳和余归纳归纳和余

7、归纳例：无限表例：无限表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 基于互模拟的余归纳证明原理是：基于互模拟的余归纳证明原理

8、是：对互模拟关系对互模拟关系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

9、(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(

10、n)()然后利用等式演算证明然后利用等式演算证明head(tail(n)(merge(odd(),even()=head(tail(n)()6.2 归纳和余归纳归纳和余归纳6.2.2 归纳和余归纳指南归纳和余归纳指南从集合论角度介绍余归纳定义和余归纳证明从集合论角度介绍余归纳定义和余归纳证明原理原理略去不介绍略去不介绍6.2 归纳和余归纳归纳和余归纳6.2.3 代数和余代数代数和余代数从从普普通通算算法法到到交交互互计计算算的的转转变变在在数数学学上上表表现现为一系列的扩展为一系列的扩展 从归纳到余归纳的扩展从归纳到余归纳的扩展表达了从字符串到流的转变表达了从字符串到流的转变 从良基集到非良基

11、集的扩展从良基集到非良基集的扩展非良基集作为流的行为的形式模型被引入非良基集作为流的行为的形式模型被引入 从代数到余代数的扩展从代数到余代数的扩展余余代代数数为为流流的的演演算算提提供供工工具具，它它相相当当于于 演演算算在在图灵计算模型中的地位图灵计算模型中的地位6.2 归纳和余归纳归纳和余归纳交换图表交换图表可用来表达函数之间的等式可用来表达函数之间的等式 f,g(z)=f(z),g(z)f,g(w)=二元积的交换图表二元积的交换图表YZ f,g X YXProj1gfProj2Zf,gX+YXYInleftgfInright二元和的交换图表二元和的交换图表6.2 归纳和余归纳归纳和余归纳

12、范畴论基本知识范畴论基本知识 1、范畴举例、范畴举例 所有的集合和它们之间的函数构成一个范畴所有的集合和它们之间的函数构成一个范畴 所有的代数和它们之间的代数同态构成一个范畴所有的代数和它们之间的代数同态构成一个范畴 所有的图和它们之间的图同态构成一个范畴所有的图和它们之间的图同态构成一个范畴2、范畴的对象和射、范畴的对象和射 每个集合是范畴的一个对象每个集合是范畴的一个对象表示为图表上的一个节点表示为图表上的一个节点 每个函数是相应两个对象之间的射每个函数是相应两个对象之间的射表示为图表上的一条有向边表示为图表上的一条有向边6.2 归纳和余归纳归纳和余归纳3、对象和射构成范畴的条件、对象和射

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

14、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，根据参

15、数，根据参数可知道它是可知道它是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+N1NInleftS0Inr

16、ight6.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 归纳和余归纳归纳和余归纳用函子和交换图表来表示代数同态用函子和交换图表来表示代数

17、同态令令 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:U F(U)，称为该余代数的余代数称为该余代数的余代数结构（也称为运算）结构（也称为运算）由于

18、余代数经常描述由于余代数经常描述动态系统，载体也叫做动态系统，载体也叫做状态空间状态空间Z f,g X YXYProj1gfProj26.2 归纳和余归纳归纳和余归纳余代数和代数的区别余代数和代数的区别本质上这是构造和观察之间的区别本质上这是构造和观察之间的区别 代数由载体集合代数由载体集合U和射入和射入U的函数的函数a:F(U)U 组组成，它告知怎样构造成，它告知怎样构造U的元素的元素 余代数由载体集合余代数由载体集合U和逆向的函数和逆向的函数c:U F(U)组组成，此时不知道怎样形成成，此时不知道怎样形成U的元素，仅有作用在的元素，仅有作用在U上的操作，它给出关于上的操作，它给出关于U的某

19、些信息的某些信息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和和next的机器的机器 可以用状态空间可以用状态空间U上的余代数上的余代数 value,next :U A U来描述，其中来描述，其中 val

20、ue,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|unit|+|t.其中其中t是类型变量是类型变量 t.的解释的解释在递归的类型定义在递归的类型定义t=中，中，引入引入fix(t.)来表示等式来表示等式t=的一个解，的一个解，用

21、用 t.作为作为fix(t.)的语法美化的语法美化 类型表达式中出现变量会导致多态性，目前限于类型表达式中出现变量会导致多态性，目前限于闭表达式闭表达式6.3 递递 归归 类类 型型类型相等问题类型相等问题对类型等式对类型等式t=有两种可能的解释有两种可能的解释 等式左右两边是真正不可区分的类型等式左右两边是真正不可区分的类型这时类型相等变得相当复杂，因为这时类型相等变得相当复杂，因为t=意味着意味着t=t 把等式把等式t=看成要找到类型看成要找到类型t，它和，它和 同构同构 t.t.t 注：注：fix(t.)t.(fix(t.)在同构观点下，类型在同构观点下，类型 t.并不等于并不等于 t.

22、t ，但，但存在把存在把 t.的项的项“转换转换”成成 t.t 的项的函数，的项的函数，反之亦然反之亦然6.3 递递 归归 类类 型型PCF语言语言中递归类型的中递归类型的定型规则定型规则 (Intro)(Elim)函数函数fold和和unfold互逆，满足下面的等式公理互逆，满足下面的等式公理unfold(fold M)=Mfold(unfold M)=M M:t./t fold M:t.M:t.unfold M:t./t(fold/unfold)6.3 递递 归归 类类 型型递归类型的急切归约规则递归类型的急切归约规则值值如果如果V是值，则是值，则fold V也是值也是值公理公理unfol

23、d(fold V)eager V，V是值是值子项规则子项规则函数函数增加了递归类型的增加了递归类型的PCF语言仍有安全性定理语言仍有安全性定理M eager M fold M eager fold M M eager M unfold M eager unfold M 6.3 递递 归归 类类 型型6.3.2 递归的数据结构递归的数据结构递归类型在程序设计语言中有很多应用递归类型在程序设计语言中有很多应用 表示像表和树这样的无界数据结构表示像表和树这样的无界数据结构 表示像循环图这样的带环数据结构表示像循环图这样的带环数据结构 支持动态定型和动态类型派遣（支持动态定型和动态类型派遣（type

24、dispatch）支持协同例程和类似的控制结构支持协同例程和类似的控制结构6.3 递递 归归 类类 型型自然数表类型的递归定义自然数表类型的递归定义 t unit+(nat t)该类型方程的解是函数该类型方程的解是函数 list的一个不动点的一个不动点fix(list)list t.unit+(nat t)这时的这时的fold和和unfold函数的类型是函数的类型是fold:unit+(nat t)t，和，和unfold:t unit+(nat t)二叉树类型的递归定义二叉树类型的递归定义t unit+(t t)6.3 递递 归归 类类 型型自然数类型的递归定义自然数类型的递归定义nat un

25、it+nat 把把nat作为递归类型的一个定义作为递归类型的一个定义nat t.unit+t 注注:t.unit+t=fix(t.unit+t)可以通过下面的同构来理解这个定义可以通过下面的同构来理解这个定义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(

26、Inright fold(Inleft)对任何自然数对任何自然数n 0，可以类似地定义如下，可以类似地定义如下 n fold(Inright fold(Inrightfold(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定义如下

27、定义如下listcase x:list.y:.f:list.Caseunit,list,(unfold x)(w:unit.y)(f)6.4 归纳类型和余归纳类型归纳类型和余归纳类型6.4.1 归纳类型和余归纳类型总揽归纳类型和余归纳类型总揽归纳类型归纳类型 对应到某个类型同构等式的最小解，也叫初始解对应到某个类型同构等式的最小解，也叫初始解 被被看看成成是是包包含含它它们们引引入入形形式式的的“最最小小”类类型型；而而其消去形式是在这引入形式上的一种递归形式其消去形式是在这引入形式上的一种递归形式 自自然然数数类类型型：包包含含引引入入形形式式0和和succ(M)的的最最小小类类型，其中型，

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

29、：正则树类型、惰性自然数类型其他例子：正则树类型、惰性自然数类型6.4 归纳类型和余归纳类型归纳类型和余归纳类型递归的类型同构式递归的类型同构式 考虑递归的类型同构式考虑递归的类型同构式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

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

31、g fhF()6.4 归纳类型和余归纳类型归纳类型和余归纳类型类型抽象子类型抽象子F的最大解的最大解 递递归归的的类类型型同同构构式式t 的的一一个个对对偶偶的的解解则则可可以以通通过取终结过取终结F余代数得到余代数得到 F余代数是一个序对余代数是一个序对 ,f，其中，其中f:F()若若 ,f 是终结代数，则是终结代数，则 是是F的最大不动点的最大不动点 F的最大不动点用的最大不动点用 F表示表示 F(h)F()g fhF()6.4 归纳类型和余归纳类型归纳类型和余归纳类型对函子对函子F的限制的限制 以保证它有最小不动点和最大不动点以保证它有最小不动点和最大不动点 F是类型抽象子是类型抽象子

32、t.，即对，即对 的形式加以限制的形式加以限制 一种比较严格的限制：一种比较严格的限制：类型抽象子类型抽象子 t.是有把握的（是有把握的（positive），），若若t不会出现在不会出现在 的一个函数类型的定义域中的一个函数类型的定义域中 例如例如 t.t t不是有把握的不是有把握的而而 t.nat t和和 t.s t是有把握的是有把握的 6.4 归纳类型和余归纳类型归纳类型和余归纳类型把把 F和和 F加入加入PCF语言语言 :=b|t|unit|+|F|F PCF的类型表达式是由上述文法产生的闭表达式的类型表达式是由上述文法产生的闭表达式 在在PCF语语言言中中为为最最小小不不动动点点和和最

33、最大大不不动动点点类类型型新新增增项项的的形形式式及及其其类类型型，可可通通过过新新增增的的定定型型规规则则来来定定义义 这次把这次把fold和和unfold定义成项常量定义成项常量6.4 归纳类型和余归纳类型归纳类型和余归纳类型把把 F和和 F加入加入PCF语言语言定型规则定型规则 fold F:F(F)F (Intro)fold:unit+(nat t)t 注注:t unit+(nat t)(Intro)unfold F:F F(F)(Elim)unfold:t unit+(nat t)注：绿色为先前介绍注：绿色为先前介绍 递归类型时采用递归类型时采用其他定型规则略其他定型规则略 M:t.unfold M:t./t M:t./t fold M:t.6.4 归纳类型和余归纳类型归纳类型和余归纳类型把把 F和和 F加加入入PCF语语言言项项的的等等式式公公理理和和推理规则推理规则 略去略去定理定理6.2 安全性定理安全性定理习习 题题 第一次：第一次：6.2，6.3第二次：第二次：6.4(a),6.5