【教学课件】第10章子定型.ppt

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

1、第10章 子定型,子定型是类型上的一种关系，该关系隐含一个类型的值可以代替另一个类型的值和子定型有关的语言概念是记录、对象及依赖于子类型关系的各种多态性本章考虑子定型和体现子定型在程序设计中作用的一些语言概念,第10章 子定型,本章的主要内容带记录和子定型的简单类型化演算等式理论和语义模型递归类型的子定型和递归记录作为对象的模型,10.1 引 言,子定型出现在许多程序设计语言中Fortran语言整型和实型（浮点）表达式混合写出整数到实数的转换有一些典型的子定型性质Pascal语言子界1.10是整数的子区间类型化面向对象语言子类型的对象可以用来代替任何超类型的对象,10.1 引 言,包容在大多数

2、类型化程序设计语言中，一个原则是：当两个类型相等时，若表达式属其中一个类型，则它同时也属另一个类型有了子定型后，则用叫做“包容”的子定型性质来代替这个原则：如果A是B的子类型，那么类型A的表达式也有类型B如果A是B的子类型，那么可以用A的元素代替B的元素,10.1 引 言,记录类型记录类型R：有整型成员a和布尔型成员b，表达式r.a和r.b都是允许的记录类型S：仅有整型成员a，s.a是合法的在类型S的元素上有意义的操作，在类型R的元素上也都有意义包含类型S的记录的任何表达式中，可以安全地使用类型R的记录去代替而不会发生类型错误R是S的子类型,10.1 引 言,记号A:B将用来表示A是B的子类型

3、断言A:B的含义有两种一般的观点1、类型A的值的每种表示都是类型B的值的一种表示2、类型A的值的每种表示都可以按某种“标准”的方式转换成类型B的值的一种表示本章观点一种语言和它的子定型性质可以由一组规则来定义子定型是类型之间的关系，而继承性是实现之间的关系,10.2 有子定型的简单类型化演算,本节用子定型来拓展，得到演算:用它来讨论子定型的一些本质特征笛卡儿积、和、unit及null可以加入而不会使它变得复杂一个:基调是一个三元组=B,Sub,CB是类型常量集合C是项常量的集合Sub是类型常量b,bB之间的子定型断言b:b的集合,10.2 有子定型的简单类型化演算,1、类型:的类型表达式和的类

4、型表达式一样:=b|:独有的特征:(ref:)(trans:)它们是所考虑的每个子定型系统的一部分，它使得子类型关系是一个前序关系,10.2 有子定型的简单类型化演算,在每个系统中，对每种类型形式，至少有一条公理或推理规则，用来标识这种类型形式的子定型性质对于函数类型有(:)对第二个变元是单调的，但是对第一个变元是反单调的,10.2 有子定型的简单类型化演算,一个简单示例：int:real引起的下列安排 int realint intreal real real int把int int解释成一个函数集合，这些函数的定义域至少是所有整数的集合,10.2 有子定型的简单类型化演算,:从Sub中的断

5、言，用公理和推理规则可以证明子定型断言:引理 对任何基调，如果:，那么 匹配 对:的子定型的语义解释子定型可以解释为转换或者包含转换解释有助于澄清子定型为什么是前序而不是偏序前序解释：可能同时有:和:，但 可相互转换的值集并不一定有同样表示,10.2 有子定型的简单类型化演算,2、项:项的定型规则包括项的所有定型规则：(cst)、(var)、(Intro)、(Elim)、(add var)新增包容规则(subsumption),10.2 有子定型的简单类型化演算,例10.1假定基调中有int:real、2:int、2.0:real和div:realrealreal令M是项x:real.(div

6、 x 2.0):real real确定M 2的类型 方式1:利用real real:int real的事实方式2:利用int:real，使得2:real,10.2 有子定型的简单类型化演算,3、等式规则:等式证明系统和的正好包含同样的公理和推理规则等价关系:(ref)、(sym)和(trans)加变量到类型指派:(add var)抽象和应用:()、()和()同余关系:()和()通常，只有在 M 和 N 都可推导时，才把等式 M N 看成是良形的,10.2 有子定型的简单类型化演算,有了子定型后会引起一些定型上的混淆外延公理()x:.(Mx)M x在M中不是自由的会导致相等的项有不同的类型适当地

7、定义M（y:.N且:）会出现:x:.(Mx):M:其中:由于:是可推导的，因此 x:.(Mx)M:可以使用,10.2 有子定型的简单类型化演算,两个项在一种类型下相等而在另一种类型下不相等在中，等式的形式写成 M N:，以直接表示这两个项的公共定型x:real.x x:real.x:real realx:real.x x:real.x:int real通常，如果A:B，在类型A上有不同值的表达式在类型B上却相等是可能的,M=N:,:M=N:,10.2 有子定型的简单类型化演算,子定型和等式的一般原则由下面推理规则给出该规则是一条导出规则,(subsumption eq),10.2 有子定型的简

8、单类型化演算,例10.3 对任何:项 x:.M:，并且:,可以证明等式 x:.M=x:.M:证明的最后两步：x:.(x:.M)x=x:.M:/使用()x:.(x:.M)x=x:.M:/使用()此例说明，在:项上，和归约没有合流性 可以由加一条归约规则来补救 x:.M x:.M:若:(type label),10.3 记 录,10.3.1 记录子定型的一般性质类型分别为1,n的成员l1,ln构成的记录的类型l1:1,ln:n记录和笛卡儿积相比，有更加丰富的子定型性质，因此记录到积的翻译不能保子定型,10.3 记 录,例employee name:string,manager:string,sal

9、ary:int manager name:string,manager:string,salary:int,dept:departmentmanager:employee确定一个记录类型是否为另一个的子类型的主要原则是所有的操作必须保持合理和良定义,10.3 记 录,例employee name:string,manager:string,salary:int manager name:string,manager:string,salary:large_int,dept:departmentmanager:employee记录子定型涉及加成员和将成员的类型限制到其子类型,10.3 记 录,1

10、0.3.2 带记录和子定型的类型化演算1、类型:,record的基调和:的基调一样，类型表达式文法是:=b|l1:,ln:记录类型中label:type的序没有什么意义,10.3 记 录,子定型的公理和推理规则包括:的(ref:),(trans:)和(:)在内增加下面的推理规则(record:),10.3 记 录,记录子定型的包含解释把记录看成一个部分函数把记录类型看成满足某种限制的部分函数集合例：记录表达式a=3,b=true看成a,3,b,true记录类型a:int,b:bool的每个记录是至少在 a,b上有定义的函数 a:int,b:bool,c:char:a:int,b:bool记录子

11、定型的转换解释,10.3 记 录,2、项:,record预备项由下面的文法给出M:=c|x|M M|x:.M|l1=M,ln=M|M.l:,record增加两条定型规则(Record Intro)(Record Elim),10.3 记 录,3、等式规则记录的等式公理类似于序对的等式公理 l1=M1,ln=Mn.li=Mi:i(record selection)l1=M.l1,ln=M.ln=M:l1:1,ln:n(record ext)l1=M1,ln=Mn=l(1)=M(1),l(n)=M(n):l1:1,ln:n(重新定序公理)其中是1,n的任意置换,10.3 记 录,例 b=true,

12、a=3,c=“Hello”=a=3,b=true,c=“Hello”:b:bool,a:int,c:string a=3,b=true,c=“Hello”=a=3,b=true:a:int,b:bool,10.4 子定型的语义模型,10.4.1 概述:最一般的转换语义每个类型解释为一个集合每当A:B，则有从A到B的“转换”函数若A是B的子集，可用恒等函数完成从A到B的转换,10.4 子定型的语义模型,10.4.2 子定型的转换解释如果b1:b2直接由基调给出，相应的转换函数必须作为解释的一部分给出如果:是使用某个证明规则从基调可证明的，那么从该基调给出的“基本”转换函数可以定义相应的转换函数有

13、了转换函数，那就可以给类型化的项以含义定义类型化项的含义的自然方式是在项的定型推导上归纳,10.4 子定型的语义模型,定义类型化项的含义的自然方式是在项的定型推导上归纳如果 M:可由推导，那么该项的含义将是把到的转换函数应用到与 M:的定型推导有关的含义上对于:，所需要的转换函数是恒等函数、基本转换和由函数合成定义的转换,10.4 子定型的语义模型,任何的语义模型可以作为:的语义模型只要对基本转换函数能找到适当的解释其它转换函数都是可定义的从的等式可靠性和完备性定理中可导出:的对应定理,10.4 子定型的语义模型,从:基调=B,Sub,C开始，将上的每个:项翻译成基调B,CSub上的项让CSu

14、b是C和一组写成c 形式的不同常量符号的并集对每个子定型b1:b2,有符号c:b1b2转换函数上的协调限制 c ca=c ca:a b所有这样的等式集合称为,b2,b2,b,ak,a1,al,b,a1,b1,b1,10.4 子定型的语义模型,1、转换函数c的定义是在:证明上的归纳(ref:):c x:.x(trans:)c x:.c(c x)(:)c f:1 2.x:1.c(f(c x)通过一系列不改变相关转换函数的证明变换，可以证明这些转换函数是唯一的,12,12,2,2,1,1,10.4 子定型的语义模型,2、项的翻译对基调=B,Sub,C上的任何:项M:,定义它到基调B,CSub上的项的

15、翻译Trans(M:),由:项的定型规则上的归纳，Trans的定义如下(cst)Trans(c:)=c(var)Trans(x:x:)=x(Intro)Trans(x:.M:)=x:.Trans(,x:M:)(Elim)Trans(MN:)=Trans(M:)Trans(N:),10.4 子定型的语义模型,(add var)Trans(,x:M:)=Trans(M:)(subsumption)若M:是可用:从M:推导的，则Trans(M:)cTrans(M:)引理10.6如果 M:是基调B,Sub,C上一个可推导的:定型断言，则Trans(M:):是基调B,CSub上可推导的定型断言,10.4

16、 子定型的语义模型,命题10.10 令=B,Sub,C是一个:基调，并且令M:是上的一个:项若对于M:有两个定型推导，并且令M1,M2=Trans(M:)是按这两个定型推导得到的M的两个翻译则使用的证明规则可得 M1=M2:,10.5 递归类型和对象的记录模型,本节研究带函数成员的记录用“方法结果”的记录来表示对象:选择一个记录的成员同发送相应的消息到一个对象返回同样的值对于带参数的方法，记录选择将返回一个函数这个模型简单、易理解、提供了面向对象的概念可以用类型化演算来研究的某种感觉,10.5 递归类型和对象的记录模型,在面向对象的程序设计中，对象类型经常可以递归地定义点类型 point ty

17、pe point=x:int,y:int,move:int int point如果有带x和y坐标和一个方向的“有向”点，那么每个有向点可以有保自己方向的move方法:,record,的类型表达式:=t|b|l1:1,lk:k|t.其中t.看成是fix(t.)的语法美化。为了可读性，仍用形式为t=的声明来定义递归类型,10.5 递归类型和对象的记录模型,type point=x:int,y:int,move:int int point看成类型point t.x:int,y:int,move:int int t fix(t.x:int,y:int,move:int int t)的语法美化即，仍用形

18、式为t=的声明来定义递归类型类型表达式等式公理t.=s.s/ts在中不是自由的()t.=t./t(unfold)相当于fix M=M(fix M),10.5 递归类型和对象的记录模型,若pt:pointt.x:int,y:int,move:intintt,那么使用类型等式(unfold)：t.=t./t则有 pt:x:int,y:int,move:int int point于是 pt.move:int int point,10.5 递归类型和对象的记录模型,例 定义点“类”如下class pointinstance variablesxval:int,yval:intconstructor p

19、oint(xv:int)(yv:int)xval=xv,yval=yvmethod x:intreturn xvalmethod y:intreturn yvalmethod move(dx:int)(dy:int):pointreturn point(self.x+dx)(self.y+dy)end,10.5 递归类型和对象的记录模型,例 略去无关部分class pointinstance variablesxval:int,yval:intconstructor point(xv:int)(yv:int)xval=xv,yval=yvmethod move(dx:int)(dy:int):

20、pointreturn point(self.x+dx)(self.y+dy)end一个类定义一个类型并定义一个创建对象的函数把对象的类型写成记录类型，把创建对象的函数写成返回记录的函数,10.5 递归类型和对象的记录模型,例（续）对象的记录模型点对象的类型是递归记录类型type point=x:int,y:int,move:int int point创建该类型的点的函数可以递归定义如下letrec mk_point(xv:int)(yv:int)=x=xv,y=yv,move=dx:int.dy:int.mk_point(xv+dx)(yv+dy),10.5 递归类型和对象的记录模型,例（续

21、）对象的记录模型type point=x:int,y:int,move:int int pointletrec mk_point(xv:int)(yv:int)=x=xv,y=yv,move=dx:int.dy:int.mk_point(xv+dx)(yv+dy)mk_point重新写成mk_pointfix(f:intintpoint.xv:int.yv:int.x=xv,y=yv,move=dx:int.dy:int.f(xv+dx)(yv+dy)其中fix:(int int point)(int int point)(int int point),10.5 递归类型和对象的记录模型,(m

22、k_point 3 2).move 4 6(fix(f:int int point.xv:int.yv:int.x=xv,y=yv,move=dx:int.dy:int.f(xv+dx)(yv+dy)3 2).move 4 6=(xv:int.yv:int.x=xv,y=yv,move=dx:int.dy:int.(fix()(xv+dx)(yv+dy)3 2).move 4 6=(x=3,y=2,move=dx:int.dy:int.(fix()(3+dx)(2+dy).move 4 6=(dx:int.dy:int.(fix()(3+dx)(2+dy)4 6=(fix()(3+4)(2+6

23、)=x=7,y=8,move=dx:int.dy:int.(fix()(7+dx)(8+dy),10.5 递归类型和对象的记录模型,下面讨论递归类型的子定型先考虑一些直观的例子type point=x:int,y:int,move:int int pointtype col_point=x:int,y:int,c:color,move:int int col_point总希望col_point是point的子类型关键看pt.move和c_pt.move是否“相容”可以通过考虑操作序列来理解它们的相容性,10.5 递归类型和对象的记录模型,第二个例子：子定型失败在表面上类似的递归记录类型上 ty

24、pe simple_set=member?:elt bool,insert:elt simple_set,intersect:simple_set simple_settype sized_set=member?:elt bool,insert:elt sized_set,intersect:sized_set sized_set,size:int两个intersect的变元类型是不同的,10.5 递归类型和对象的记录模型,type simple_set=member?:elt bool,insert:elt simple_set,intersect:simple_set simple_set

25、type sized_set=member?:elt bool,insert:elt sized_set,intersect:sized_set sized_set,size:int假定s,t:simple_set且r:sized_set计算两个简单集合的交集的表达式 s.intersect t表达式r.intersect t可能会引起错误,10.5 递归类型和对象的记录模型,type simple_set=member?:elt bool,insert:elt simple_set,intersect:simple_set simple_settype sized_set=member?:e

26、lt bool,insert:elt sized_set,intersect:sized_set sized_set,size:inttype sized_set=member?:elt bool,改用insert:elt sized_set,sized_set intersect:simple_set sized_set,来解决size:int,10.5 递归类型和对象的记录模型,:,record,的等式规则和子定型规则(trans:)（10.2节）(:)（10.2节）record:)（10.3节）需要一条推理规则从相等断言得到子定型断言，还需要一条规则用于递归类型,10.5 递归类型和对象

27、的记录模型,:,record,的等式规则和子定型规则从相等断言得到子定型断言的规则(=:)用于递归类型的规则 t在中不是自由的，s在中不是自由的(:),10.5 递归类型和对象的记录模型,证明col_point:point最后一步的形式必定是应先证int:int和col_point:point int(int col_point):int(int point)后者从自反性和假设col_point:point，两次应用(:)规则可得,10.5 递归类型和对象的记录模型,加相等测试方法到点和有色点,则子定型失败type eq_point=x:int,y:int,eq:eq_point boolty

28、pe eq_col_point=x:int,y:int,eq:eq_col_pointbool,c:color最后一步的形式总是需要先证int:int和eq_col_point:eq_point(eq_col_point bool):(eq_point bool)后者需要证明eq_col_point:eq_point eq_point:eq_col_point,eq_col_point:eq_point x:int,y:int,eq:eq_col_pointbool,c:color:x:int,y:int,eq:eq_point bool eq_col_point.:eq_point.,习 题,第一次：10.1,10.4第二次：10.14,