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

《【教学课件】第6章递归类型.ppt》由会员分享，可在线阅读，更多相关《【教学课件】第6章递归类型.ppt（43页珍藏版）》请在三一办公上搜索。

1、第6章 递归类型,递归定义的类型的例子自然数表的类型类型等式 t unit+(nat t)的一个解二叉树的类型类型等式 t unit+(t t)的一个解使用“”表示解是要使两边同构，而不是相等归纳类型对应到上述类型同构等式的初始解例：自然数类型余归纳类型对应到它们的终结解例：自然数流类型,6.1 引 言,本章的主要内容直观地介绍余归纳的定义、余归纳的证明原理和余代数形式地介绍递归类型形式地介绍归纳类型和余归纳类型解释代数方法是从“构造的”角度研究抽象数据类型余代数方法是从“观察的”的角度描述像对象、自动机、进程、软件构件等基于状态的系统。,6.2 归纳和余归纳,6.2.1 余归纳现象例数据集A

2、上的有限表集可归纳地定义如下(1)基础情况：nil是有限表(2)迭代规则：若aA且是有限表，则cons(a,)是有限表(3)最小化条件：此外，有限表集中不含其它元素最小化规则指所定义的集合是满足(1)和(2)两条约束的最小集合，无任何垃圾在其中,6.2 归纳和余归纳,例数据集A上的无限表集（流）可余归纳地定义如下(1)迭代规则：若aA且是无限表，则cons(a,)是无限表(2)最大化条件：数据集A上的无限表集是满足迭代规则的最大集合最大化条件表示所有未被(1)排除的元素都被包含在所定义的集合中，即该集合中任何无限表都可以通过应用规则(1)若干次（可能是无限次）而得到,6.2 归纳和余归纳,比较

3、两种表都有观察算子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

4、(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、定义evene

5、ven=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()对于第二个

6、条件需证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(ta

7、il(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 代数和余代数从普通算法到交互计算的转变在数学上表现为一系列的扩展 从归纳到余归纳的扩展表达了从字符串到流的转变 从良基集到非良基集的扩展非良基集作为流的行为的形式模型被引入 从代数到余代数的扩展余代数为流的演算

8、提供工具，它相当于演算在图灵计算模型中的地位,6.2 归纳和余归纳,交换图表可用来表达函数之间的等式 f,g(z)=f(z),g(z)f,g(w)=,二元积的交换图表,Y,二元和的交换图表,6.2 归纳和余归纳,范畴论基本知识 1、范畴举例 所有的集合和它们之间的函数构成一个范畴 所有的代数和它们之间的代数同态构成一个范畴 所有的图和它们之间的图同态构成一个范畴2、范畴的对象和射 每个集合是范畴的一个对象表示为图表上的一个节点 每个函数是相应两个对象之间的射表示为图表上的一条有向边,6.2 归纳和余归纳,3、对象和射构成范畴的条件 射是可以合成的函数可以合成，代数同态和图同态可以合成 射的合成

9、满足结合律函数和同态的合成有性质(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都在集合范

10、畴中，则F1(g f)=F1(g)F1(f),下面都用F，根据参数可知道它是F0还是F1,6.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,6.2 归纳和余归纳,例：二叉树 以集合A的元素标记节点的二叉树的集合用tree(A)表示 空树nil可用函数nil:1 tree(A)表示 node:tree(A)A tree(A)tree(A)表

11、示从两棵子树和一个节点标记构造一棵树 nil和node形成函子F(X)=1+(X A X)的一个代数nil,node:1+(tree(A)A tree(A)tree(A),6.2 归纳和余归纳,用函子和交换图表来表示代数同态令 F是函子 a:F(U)U和b:F(V)V是两个函数 则F代数U,a到V,b的同态是函数f:U V，满足f a=b F(f)可进一步定义初始代数,6.2 归纳和余归纳,定义余代数 令F是函子，F的一个余代数（简称F余代数）是一个序对U,c，其中 U是集合，称为该余代数的载体 c是函数c:U F(U)，称为该余代数的余代数结构（也称为运算）由于余代数经常描述动态系统，载体也

12、叫做状态空间,6.2 归纳和余归纳,余代数和代数的区别本质上这是构造和观察之间的区别 代数由载体集合U和射入U的函数a:F(U)U 组成，它告知怎样构造U的元素 余代数由载体集合U和逆向的函数c:U F(U)组成，此时不知道怎样形成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可进一步定义终结代数,6.2 归纳和余归纳,例：考虑有两个按键value和next的机器 可以用状态空间U上的余代数 val

13、ue,next:U A U来描述，其中 value,next由两个函数value:U A和next:U U组成 连续地交替按next键和value键，可以产生无限序列(a1,a2,)它可以看成N A上的一个函数，其中ai=value(next(i)(u)A,6.3 递 归 类 型,6.3.1 递归类型总揽在PCF的类型中加入递归类型:=b|t|unit|+|t.其中t是类型变量 t.的解释在递归的类型定义t=中，引入fix(t.)来表示等式t=的一个解，用 t.作为fix(t.)的语法美化 类型表达式中出现变量会导致多态性，目前限于闭表达式,6.3 递 归 类 型,类型相等问题对类型等式t=有

14、两种可能的解释 等式左右两边是真正不可区分的类型这时类型相等变得相当复杂，因为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)=Mfold(unfold M)=M,(fold/unfold),6.3 递 归 类 型,递归类型的急切归约规则值如果V是值，则fold V也是值公理unfold

15、(fold V)eager V，V是值子项规则函数增加了递归类型的PCF语言仍有安全性定理,M eager M unfold M eager unfold M,6.3 递 归 类 型,6.3.2 递归的数据结构递归类型在程序设计语言中有很多应用 表示像表和树这样的无界数据结构 表示像循环图这样的带环数据结构 支持动态定型和动态类型派遣（type dispatch）支持协同例程和类似的控制结构,6.3 递 归 类 型,自然数表类型的递归定义 t unit+(nat t)该类型方程的解是函数list的一个不动点fix(list)list t.unit+(nat t)这时的fold和unfold函数

16、的类型是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)可以通过下面的同构来理解这个定义nat unit+nat unit+(unit+nat)unit+(unit+(unit+nat)unit+(unit+(unit+(unit+(unit+nat),6.3 递 归 类 型,自然数类型的递归定义nat unit+(unit+(unit+(un

17、it+(unit+nat)自然数0和1的定义如下0 fold(Inleft)1 fold(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定义如下list

18、case x:list.y:.f:list.Caseunit,list,(unfold x)(w:unit.y)(f),6.4 归纳类型和余归纳类型,6.4.1 归纳类型和余归纳类型总揽归纳类型 对应到某个类型同构等式的最小解，也叫初始解 被看成是包含它们引入形式的“最小”类型；而其消去形式是在这引入形式上的一种递归形式 自然数类型：包含引入形式0和succ(M)的最小类型，其中M也是引入形式 其他例子：串、表、树和任何其他可以看成从它引入形式有限地生成的类型,6.4 归纳类型和余归纳类型,余归纳类型 对应到某个类型同构等式的最大解，也叫终结解 其引入形式是一种在消去形式需要时提供元素的方法

19、自然数流类型：一个流可想象成处于由一个自然数（它的头）和另一个流（它的尾）构成的序对的生成过程中 其他例子：正则树类型、惰性自然数类型,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,()(y.:Inrightunit,(My)t 的解是一个类型，使得和F()之间存在一

20、个同构，即是F的不动点,6.4 归纳类型和余归纳类型,类型抽象子F的最小解 对于f:F()，,f是一个F代数，满足下面的交换图表 若,f是初始F代数，则是F的最小不动点 F的最小不动点用F表示 对初始F代数就是最小不动点的理解需要回顾初始代数没有“垃圾”的特点,6.4 归纳类型和余归纳类型,类型抽象子F的最大解 递归的类型同构式t 的一个对偶的解则可以通过取终结F余代数得到 F余代数是一个序对,f，其中f:F()若,f是终结代数，则是F的最大不动点 F的最大不动点用F表示,6.4 归纳类型和余归纳类型,对函子F的限制 以保证它有最小不动点和最大不动点 F是类型抽象子t.，即对的形式加以限制 一

21、种比较严格的限制：类型抽象子t.是有把握的（positive），若t不会出现在的一个函数类型的定义域中 例如t.t t不是有把握的而t.nat t和t.s t是有把握的,6.4 归纳类型和余归纳类型,把F和F加入PCF语言:=b|t|unit|+|F|F PCF的类型表达式是由上述文法产生的闭表达式 在PCF语言中为最小不动点和最大不动点类型新增项的形式及其类型，可通过新增的定型规则来定义 这次把fold和unfold定义成项常量,6.4 归纳类型和余归纳类型,把F和F加入PCF语言定型规则 foldF:F(F)F(Intro)fold:unit+(nat t)t 注:t unit+(nat t)(Intro)unfoldF:F F(F)(Elim)unfold:t unit+(nat t)注：绿色为先前介绍 递归类型时采用其他定型规则略,6.4 归纳类型和余归纳类型,把F和F加入PCF语言项的等式公理和推理规则 略去定理6.2 安全性定理,习 题,第一次：6.2，6.3第二次：6.4(a),6.5,