上次课程小结市公开课特等奖市赛课微课一等奖课件

上次课程小结类型系统：赋给程序各部分一组规则类型表示式：由类型结构符作用与基本类型表示式。基本类型表示式：基本类型、类型名、类型变量值类型结构符：×、＋、array(I,T)、pointer(T)、record（F1×F2×...)、D→R简单类型检验：语法制导翻译申明时结构类型表示式引用时计算类型表示式（类型检验）第1页4.4类型表示式等价在简单类型检验中，经过判定所给两个类型表示式是否相等来进行类型检验。对于单态类型，我们引入一个更专业术语，类型等价来描述类型检验。类型等价与类型表示相关，表示不一样，等价概念也不一样。本节讨论三个主要问题：有哪些类型等价程序设计语言要求什么样等价以及等价判别第2页4.4.1结构等价与等价判别若两个仅由类型结构符作用于基本类型组成类型表示式完全相同，则称两个类型表示式结构等价。换句话说，类型表示式结构等价当且仅当二者完全相等。若类型表示式中没有名字，则结构等价就是类型等价。比如int与int结构等价，array(1..10,real)与array(1..10,real)结构等价。反应在类型表示式语法树上，就是两棵语法树完全相同。第3页<1>结构等价判别算法4.1判别类型是否结构等价输入两个类型表示式输出若两个类型表示式结构等价则返回true不然false方法用下述递归函数进行判别：functionsequiv(s,t)returnbooleanisbegin

endsequiv;ifsandtarethesametypethenreturntrue;elsifs=array(s1,s2)andt=array(t1,t2) thenreturnsequiv(s1,t1)andsequiv(s2,t2);elsifs=s1×s2andt=t1×t2 thenreturnsequiv(s1,t1)andsequiv(s2,t2);elsifs=pointer(s1)andt=pointer(t1)thenreturnsequiv(s1,t1);elsifs=s1→s2andt=t1→t2 thenreturnsequiv(s1,t1)andsequiv(s2,t2);elsereturnfalse; endif;第4页<1>结构等价判别（续）例4.13再考虑函数申明functionmax(x,y:integer):integer和调用max(5,8)：在对调用语句max(5,8)类型检验中，因为函数形参类型和实参类型等价（sequiv(s,E2.type)=true），所以最终函数值类型为int。申明时：调用时：E→E1,E2 {E.type:=E1.type×E2.type;}|E1(E2) {E.type:=ifE2.type=sandE1.type=s→t thentelsetype_error;}第5页<2>类型表示式优化表示sequiv(s,t)算法弱点：需要对两棵语法树完全遍历后才能确定它们是否等价。当类型结构符层次很多而且仅在最底层不等价时，算法效率较低。改进思绪：在调用sequiv之前，先用一个简单方法将明确能够确定不等价情况排除。即为了提升效率，牺牲一些次要信息，只有当两个类型表示式主要信息相等时才判定次要信息是否也相等。详细方法：对类型表示式主要信息进行编码。将类型结构符表示每个内部节点多于一个孩子分支剪去，仅保留一个主要分支，类型表示式语法树就退化为一个链，即一条从根到叶子路径。对链上每个节点编码，形成一个类型编码字符串或者整型数。因为类型编码仅反应了类型表示式主要成份，所以两个编码不一样，则类型表示式一定不等价（从而起到过滤作用），反之不一定。第6页<2>类型表示式优化表示（续1）数组类型表示式array(s,t)简化为array(t)，即忽略下标类型保留数组元素类型。函数类型表示式s→t简化为freturns(t)，即忽略参数类型保留返回值类型。指针类型表示式pointer(t)本身就是一个一元结构符，所以无需简化。问题：×与record简化怎样处理？简化类型表示式编码：基本类型类型结构符类型编码结构符编码boolean0000pointer01char0001array10int0010freturns11real0011non00类型表示式化简：第7页<2>类型表示式优化表示（续2）基本类型类型结构符类型编码结构符编码boolean0000pointer01char0001array10int0010freturns11real0011non00例4.14

考虑类型表示式array(1..10,pointer(int→char))：简化后类型表示式为array(pointer(freturns(char)))。将其从左到右转换为编码，得到1001110001。第8页4.4.2引入类型名等价判别若每个类型名作为一个可区分类型出现在表示式中而且使得两个类型表示式完全相同，则称它们名字等价。若将类型表示式中全部名字均用其定义类型表示式替换后两个类型表示式完全相同，则称它们结构等价。例4.15

对于下述Pascal程序段：typecell=array[1..10,int];typelink=^cell;var next :link; last :link; p :^cell; q,r :^cell;采取名字等价，则变量next和last类型表示式为link，变量p、q、r类型表示式为pointer(cell)，显然next和last名字等价，p、q、r名字等价。若将名字用它们所代表结构代替，则5个变量类型表示式均为pointer(array(1..10,int))。所以它们全部结构等价。第9页4.4.2引入类型名等价判别（续1）名字等价经过对取值范围相同不过代表不一样意义对象取不一样类型名，使得它们含有不一样类型。不一样类型对象不能进行运算，从而防止了潜在错误；名字等价提升了程序可靠性，不过降低了程序灵活性；程序设计语言能够依据不一样需求采取不一样等价策略。比如Algol68采取结构等价，而Ada采取名字等价。例4.16

下述Ada类型定义语句将完全相同结构定义为不一样名字：typemale_typeisnode_array;typefemale_typeisnode_array;male:male_type;female:female_type;在名字等价下，变量male和female类型不一样，使得这两个变量之间不能运算。

第10页为何要求采取何种类型等价

Pascal没有要求采取何种等价，其等价问题依赖于实现，给熟悉名字等价或结构等价程序员带来无须要使用上混乱。Pascal关于类型等价一个处理方案是：变量申明时对类型每次引用，均隐含地为它结构一个类型名，然后采取名字等价。type cell=array[1..10,int];type link=^cell;

np=^cell;

nqr=^cell;var next:link; last:link; p:np; q,r:nqr;typecell=array[1..10,int];typelink=^cell;var next :link; last :link;

p :^cell;

q,r :^cell;在名字等价定义下，原来与q和r类型等价p现在被认为不与任何变量类型等价。第11页为何要求采取何种类型等价（续）Pascal这种类型等价实现方法，似乎比名字等价更为严格。程序员能够采取一个变通方法将Pascal程序转换为名字等价，若有不一样变量申明含有结构等价类型时，一定要先定义这类型，即为这类型命名。例4.17定义下述两个申明语句，变量a和参数x实质上结构等价：vara:array[1..10]ofinteger;functiontest(x:array[1..10]ofinteger):integer;依据Pascal等价策略，a与x类型不等价，所以a不能作为函数test实参。若希望a作为test实参，则必须首先为它们共同类型命名，然后a和x均被申明为这类型名所定义类型：typearr_type=array[1..10]ofinteger;vara:arr_type;functiontest(x:arr_type):integer;从而使得a与x类型等价。第12页单态类型检验普通过程确定一个类型等价方式：没有类型名情况下全部等价问题均是结构等价；名字能够作为类型表示式时，就需要确定等价策略，是采取名字等价还是采取结构等价；依据类型信息结构类型表示式，名字等价与结构等价唯一区分就是类型名是否能够出现在类型表示式中；判定表示式类型等价就是判定它们类型表示式是否相等。第13页4.5多态函数类型检验通俗讲，程序设计语言中多态就是一个符号能够有各种意思。多态与强类型是密不可分，即使一个符号能够有各种意思，不过编译器必须确保它每次使用是确定而且是类型正确，不然并不是多态而是弱类型。弱类型经典例子是C，比如在C程序中char类型变量和int类型变量能够运算，不过运算结果正确性由程序员负责。第14页4.5.1多态函数与类型变量表示通用多态中参数多态被称为多态函数。多态函数基本特征是参数类型是类型变量且该变量能够取无穷多个值，不过全部类型均对应同一代码序列。多态函数中形参类型是变量，称为类型变量，用α、β、δ等表示。从语言结构使用方式推断其类型，被称为类型推断（typeinference）。比如从函数体推断函数类型。例4.18对于函数定义：functionderef(p);beginreturnp^end；从函数体中能够看出，p类型应该是指向某对象指针，而p^返回它所指向对象。设该对象类型为α，则p类型是pointer(α)，所以函数deref(p)类型应该是：

α.pointer(α)→α (4.1)即对于任何一个类型为α对象，函数deref(p)是将指向α对象一个指针类型映射到该对象。deref习惯上也被称为脱引用。<1>多态函数、类型变量与类型推断第15页<2>含多态函数语言文法多态函数与单态函数本质区分是形参不但能够是常量也能够是变量。所以对(AG4.1)和(AG4.4)文法进行扩充，将含有类型变量类型定义引入产生式。P→D;ED→D;D|id:QQ→

type-variable.Q|T (G4.6)T→T'→'T|T×T|unary-constructor(T)|basic-type|type-variable|(T)E→E(E)|E,E|id此扩充与将数据简单变量扩充为含有数组元素类似。首先，文法将原来单态类型T扩展为多态类型Q，Q除了包含T产生式全部，又引入了受约束类型变量。同时T产生式中增加了类型变量，即将类型变量引入类型。引入数组元素后赋值句文法A→V:=EV→id[EL]|idEL→EL，E|EE→E+E|(E)|V第16页<2>含多态函数语言文法（续1）例4.19

按文法(G4.6)书写一个程序以下：

P→D;ED→D;D|id:QQ→

type-variable.Q|T (G4.6)T→T'→'T|T×T|unary-constructor(T)|basic-type|type-variable|(T)E→E(E)|E,E|idderef:

α.pointer(α)→α;q:pointer(pointer(int));defef(deref(q));首先申明deref和q，然后是函数调用defef(deref(q))，其中内层函数调用返回值作为外层调用实参。显然，两个相同函数在不一样位置出现含有不一样参数类型和返回值类型。

第17页<2>含多态函数语言文法（续2）deref:

α.pointer(α)→α;q:pointer(pointer(int));defef(deref(q));P→D;ED→D;D|id:QQ→

type-variable.Q|T (G4.6)T→T'→'T|T×T|unary-constructor(T)|basic-type|type-variable|(T)E→E(E)|E,E|id函数名作用于参数得到函数返回值每次引入一个固定变元第18页结束（4月29日）

“五一”节高兴！

（五一后第一周两次课！）第19页多态函数简单回顾多态函数、类型变量与类型推断含多态函数语言文法deref:

α.pointer(α)→α;q:pointer(pointer(int));defef(deref(q));P→D;ED→D;D|id:QQ→

type-variable.Q|T (G4.6)T→T'→'T|T×T|unary-constructor(T)|basic-type|type-variable|(T)E→E(E)|E,E|idP→D;ED→D;D|id:QQ→

type-variable.Q|T (G4.6)T→T'→'T|T×T|unary-constructor(T)|basic-type|type-variable|(T)E→E(E)|E,E|id每次引入一个新类型变量替换变量试图得到匹配保留替换结果以继续匹配第20页4.5.2代换、实例与合一多态函数类型检验普通方法：首先设法消除类型变量，然后判定消除类型变量后类型表示式是否结构等价。详细有三点与单态类型检验不一样：(1)消除约束变元类型表示式中约束变元在语法树中每次出现均要被替换为自由变元，且同一类型表示式多态函数不一样出现，变元能够有不一样类型。方法是每引入一个多态类型表示式，就为变元引入一个新类型变量。如将

α.pointer(α)→α改为pointer(α0)→α0或pointer(αi)→αi，从而消除了全称量词和约束变元。第21页4.5.2代换、实例与合一（续1）(2)合一（unify）类型表示式

判断类型表示式s和t是否等价变成能否使s和t“合一”，即当把s和t类型变量用不含类型变量类型表示式替换后判断s和t是否结构等价。比如在对derefi进行类型检验时，将αi用pointer(int)替换，即αi=pointer(int)，可使得函数形参类型pointer(αi)与实参类型pointer(pointer(int))等价。(3)统计合一结果

对每次合一结果，需要统计下来，方便后续类型检验使用。比如将αi用pointer(int)替换后结果是正确，则此结果需要统计下来，再用于deref0类型检验。第22页4.5.2代换、实例与合一（续2）术语（基本概念）：代换（Substitutions）代换是从类型变量到类型表示式一个映射。比如类型变量αi到类型表示式pointer(int)映射。实例（instances）代换结果被称为代换一个实例，用S(t)表示。S(t)<t表示S(t)是t一个代换实例。类型表示式pointer(int)是类型变量αi一个实例，能够表示为pointer(int)<αi。不含类型变量类型表示式是其本身一个实例，比如int<int。合一（Unification）若存在代换S，使得S(t1)=S(t2)，则称表示式t1和t2能合一，该代换过程被称为合一操作。S(αi)=pointer(int)，所以αi和pointer(int)能合一。第23页最普通合一代价最小代换被称为最普通合一。所谓代价最小代换含有下述性质：S(t1)=S(t2)

S'.S'(t1)=S'(t2)都有S'<S，即

t.S'(t)<S(t)或者说S是代换次数最少一个实例，即一旦有了能够确定类型是否等价代换结果，就马上停顿代换。代换算法与类型等价算法很相同。此处代换算法仅考虑了函数情况，而其它类型结构符类型代换与之类似。第24页代换算法算法4.2代换算法输入类型表示式t输出t代换实例方法用下述递归函数进行代换：functionsubs(t:type_expression)returntype_expressionisbeginendsubs;if tisabasic_type thenreturnt;--基本类型代换是其本身elsiftisavariablethen returnS(t);--返回类型变量一个代换实例elsif tist1→t2 thenreturnsubs(t1)→subs(t2);--分别代换映射两边类型表示式end if;与等价算法比较在算法中加入其它类型结构符第25页代换算法（续）iftisabasic_typethenreturnt;--基本类型代换是其本身elsiftisavariablethenreturnS(t);--类型变量代换实例elsif tist1→t2thenreturnsubs(t1)→subs(t2);--分别代换end if;real<realint→int<α→αpointer(int)<pointer(α)α<β而：int≮real，因为int和real是不一样基本类型表示式。int→real≮α→α，因为α代换不一致，映射左边被代换为int，而右边被代换为real。int→α≮α→α，因为α代换不完全，映射左边被代换，而右边没有代换。例4.20依据算法4.2能够判断：第26页4.5.3多态函数类型检验多态函数类型检验基本思想是对两个要被检验类型进行合一操作。所谓判定类型表示式e和f是否能合一，就是能否找到一个代换S，使得S(e)=S(f)，即检验e和f在代换S下是否等价。检验方法是分别给出e和f语法树，假如两棵语法树经过代换之后重合为一棵语法树，则说明e和f能合一。第27页4.5.3多态函数类型检验（续1）fresh(t)：将类型表示式t中约束变元用一新自由变元来代替，若t是一个类型常量则结果依然是t本身。这一过程类似于产生暂时变量语义函数newtemp。不一样是fresh产生是类型变量自由变元α、β、δ等。比如fresh(deref:

α.pointer(α)→α)能够得到pointer(α1)→α1，fresh(int)=int。union(m,n)：结构m和n等价类，并在等价类中选取一个代表。union(m,n)选取等价类代表关键是：两个类型表示式中非类型变量类型表示式被优先选取为代表，从而确保了类型变量到类型表示式代换。不然任选其一作为代表，比如能够选取节点编号小。find(m)：找到并返回m所在等价类中代表。语义函数：第28页4.5.3多态函数类型检验（续2）算法4.3

类型表示式合一算法输入以m和n为根两棵类型表示式语法树输出若m和n代表类型表示式能合一则返回true不然false方法用下述递归函数进行代换：

functionunify(m,n:nptr)returnbooleanisbeginendunify;s:=find(m); t:=find(n); --分别找到m和n所在等价类代表if s=t thenreturntrue;elsif s和t代表相同基本类型thenunion(s,t);

returntrue;elsif s和t代表相同类型结构符并分别有孩子节点(s1,s2)和(t1,t2)thenunion(s,t);

--结构等价类returnunify(s1,t1)andunify(s2,t2);--分别合一左右孩子elsif s或t代表一个变量thenunion(s,t);

returntrue;else returnfalse;

--其它均不可合一endif;第29页4.5.3多态函数类型检验（续3）多态函数文法(G4.6)中表示式类型检验语义规则：E→E1(E2){ γ:=mkleaf(newtypevar); unify(E1.type,mknode('→',E2.type,γ); E.type:=γ;} (AG4.6)|E1,E2{ E.type:=mknode('×',E1.type,E2.type);}|id { E.type:=fresh(id.type);}函数调用E→E1(E2)语义处理：设E1.type=α且在函数申明时α已确定(α=s→t)，设E2.type=β。则应有未知类型γ，使得S(α)=S(β→γ)。为此设α语法树根节点为n，并建立一个类型为γ叶节点和一个类型为β→γ新节点m。若m与n合一成功则其结果γ成为E.type类型。第30页deref(deref(q))类型检验例4.21用算法4.3和(AG4.6)，对deref(deref(q))进行类型检验。E→E1(E2){ γ:=mkleaf(newtypevar); unify(E1.type,mknode('→',E2.type,γ); E.type:=γ;} (AG4.6)|id { E.type:=fresh(id.type);}E1→