泛代数和代数数据类型.ppt

Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,中国科大,*,第,2,章 泛代数和代数数据类型,函数式程序设计语言,PCF,由三部分组成,代数数据类型：自然数类型和布尔类型,带函数和积等类型的纯类型化,演算,不动点算子,第,2,章到第,4,章对,这三,部分进行透彻的研究,本章研究像自然数类型和布尔类型这样的代数数据类型,2,.1,引 言,代数数据类型,包括,一个或多个值集,一组在这些集合上的函数,基本限制是其函数不能有函数变元,基本“类型”(,type,),符号被称为“类别”(,sort,),泛代数（也叫做等式逻辑）,定义和研究代数数据类型的一般数学框架,本章研究泛代数和它在程序设计中定义常用数据类型时的作用,2,.1,引 言,本章主要内容：,代数项和它们在多类别代数中的解释,等式规范（也叫代数规范）和等式证明系统,等式证明系统的可靠性和完备性（公理语义和指称语义的等价）,代数之间的同态关系和初始代数,数据类型的代数理论,从代数规范导出的重写规则（操作语义）,包括了大多数逻辑系统中的一些公共议题,2,.2,代数、基调和项,2.2.1,代数,代数,一个或多个集合，叫做载体,一组特征元素和一阶函数，也叫做代数函数,f,:,A,1,A,k,A,例：,N,N,0,1,+,载体,N,是自然数集合,特征元素0,1,N,，,也叫做零元函数,函数+,:,N,N,N,2,.2,代数、基调和项,多个载体的例子,A,PCF,N,B,0,1,+,true,false,Eq,?,下面逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要，可用来,定义数据类型,证明数据类型的性质,还必须讨论这种语法描述的指称语义,满足一组等式的除了,A,PCF,外，可能还有：,A,5,PCF,N,5,B,0,1,2,3,4,+,5,true,false,Eq,?,2,.2,代数、基调和项,2,.2.2,代数项的语法,基调,S,，,F,S,是一个集合,，,其元素叫做,类别,函数符号,f,:,s,1,s,k,s,的,集合,F,，,其中,表达式,s,1,s,k,s,叫做,f,的类型,零元函数符号叫做常量符号,例,:,N,S,，,F,sorts:,nat,fctns,:0,1:,nat,:,nat,nat,nat,2,.2,代数、基调和项,项,定义基调的目的是用于写代数项,项中可能有变量，因此需假定一个无穷的符号集合,V,，,其元素称为变量,类别指派,x,1,:,s,1,x,k,:,s,k,基调,S,，,F,和类别指派上类别,s,的代数项集合,Terms,s,(,),定义如下：,1,、如果,x,:,s,，,那么,x,Terms,s,(,),2,、如果,f,:,s,1,s,k,s,并且,M,i,Terms,(,)(,i,1,k,),，,那么,f M,1,M,k,Terms,s,(,),当,k,0,时，如果,f,:,s,，,那么,f,Terms,s,(,),s,i,2,.2,代数、基调和项,项的例子,0,0 1,Terms,nat,(,N,),0,x,Terms,nat,(,N,)，,其中,x,:,nat,代数项中无约束变元,N,x,M,就是简单地把,M,中,x,的每个出现都用,N,代替,记号,x,:,s,x,:,s,引理,2.1,若,M,Terms,s,(,x,:,s,),且,N,Terms,s,(,)，,那么,N,x,M,Terms,s,(,),证明 按,Terms,s,(,),中项的结构进行归纳,2,.2,代数、基调和项,例,用基调,stk,S,F,来写自然数和自然数栈表达式,sorts:,nat,stack,fctns,:0,1,2,:,nat,:,nat,nat,nat,empty,:,stack,push,:,nat,stack,stack,pop,:,stack,stack,top,:,stack,nat,push,2(,push,1(,push,0,empty,),是该基调的项,2,.2,代数、基调和项,2,.2.3 代数以及项在代数中的解释,基调的代数是为代数项提供含义的数学结构,是一个基调，则,代数,A,包含,对每个,s,S,，,正好有一个载体,A,s,一个解释映射,I,把函数,I,(,f,),:,A,A,A,s,指派给函数符号,f,:,s,1,s,k,s,F,把,I,(,f,),A,s,指派给常量符号,f,:,s,F,N,代数,N,写成,N,N,0,N,1,N,N,N,s,k,s,1,2,.2,代数、基调和项,代数,A,的环境,:,V,s,A,s,环境,满足,如果对每个,x,:,s,都有,(,x,),A,s,M,Terms,s,(,),的含义,A,M,是,A,x,(,x,),A,M,f,A,(,A,M,1,A,M,k,),若,f,:,s,是常量符号，则,A,f,f,A,若,A,清楚时，省略,A,而直接写成,M,不依赖于,时，,用,A,M,表示,M,在,A,中的含义,2,.2,代数、基调和项,例 若,(,x,),0,N,x,1,N,(,x,1,),N,(,(,x,),1,N,),N,(0,N,1,N,),1,N,2,.2,代数、基调和项,例,A,stk,N,N,0,A,1,A,A,A,empty,A,push,A,pop,A,top,A,empty,A,空序列,push,A,(,n,s,),n,:,s,pop,A,(,n,:,s,),s,pop,A,(,),top,A,(,n,:,s,),n,top,A,(,)0,A,若,把,x,:,nat,映射到自然数,3,，,把,s,:,stack,映射到,2,1,pop,(,push,x s,),pop,A,(,push,A,(,x,s,),pop,A,(,push,A,(3,2,1),pop,A,(3,2,1),2,1,2,.2,代数、基调和项,引理,2.2,令,A,是,代数，,M,Terms,s,(,),，,并且,是满足,的环境，那么,M,A,s,证明 根据,Terms,s,(,),中项的结构进行归纳,引理,2.3,令,x,1,x,k,是由出现在,M,Terms,s,(,),中的所有,变量构成的变量表，,1,和,2,是满足的两个环境,并,且对,i,1,k,有,1,(,x,i,),2,(,x,i,),那么,M,1,M,2,证明 基于项结构的归纳,2,.2,代数、基调和项,2,.2.4 代换引理,引理,2.4,令,M,Terms,s,(,x,:,s,),并且,N,Terms,s,(,)，,那,么,N,x,M,Terms,s,(,)。,并且对任何环境,，有,N,x,M,M,(,x,a,),，,其中,a,N,，它,是,N,在,下的含义,证明 根据项,M,的结构进行归纳,2,.3,等式、可靠性和完备性,代数规范,一个,基调+一组等式,调查什么样的代数满足这些等式强加的要求,使用等式证明系统可推导的新的等式,可靠性：,从规范可证明的等式在任何满足该规范的代数中都成立,完备性：,在满足规范的所有代数中都成立的等式都可从该规范证明,代数规范是描述,代数数据类型公理语义的工具,2,.3,等式、可靠性和完备性,2,.3.1 等式,公式,M,N,，,对某个,s,，,M,N,Terms,s,(,),若,满足，并且还有,M,N,，,则认为代数,A,在环境,下满足,M,N,，,写成,A,M,N,若,A,在任何环境下都满足该等式，则写成,A,M,N,若代数类,C,中的任何代数,A,都满足该等式，写成,C,M,N,若任何一个代数都满足,等式,M,N,，则写成,M,N,(,永真的、有效的,),2,.3,等式、可靠性和完备性,平凡的代数,若,A,满足上所有等式，就说代数,A,是平凡的,例,令有两个类别,a,和,b,，令,A,是一个代数，其中,A,a,0,1,并且,A,b,A,不可能满足,x,y,x,:,a,y,:,a,，,即下式,不成立,A,x,y,x,:,a,y,:,a,但是,A,x,y,x,:,a,y,:,a,z,:,b,无意义地,成立,2,.3,等式、可靠性和完备性,2,.3.2,项代数,项代数,Terms,(,),类别,s,的载体：,集合,Terms,s,(,),函数符号,f,:,s,1,s,k,s,的解释,I,(,f,)(,M,1,M,k,),f M,1,M,k,项代数,Terms,(,),的环境,也叫做一个代换,如果,S,是代换，则用,SM,表示同时把,M,中的各个变量,x,用,Sx,替换的结果,因此用,M,表示把代换,作用于,M,的结果,2,.3,等式、可靠性和完备性,例,类别,u,函数符号,f,:,u u,和,g,:,u,u,u,a,:,u,b,:,u,c,:,u,T,u,a,b,c,fa,fb,fc,gaa,gab,gac,gbb,g,(,f,(,fa,)(,f,(,gbc,),若环境,把变量,x,映射到,a,，,把,y,映射到,f b,，,则,T,g,(,f,x,)(,f y,),g,(,fa,)(,f,(,f,b,),2,.3,等式、可靠性和完备性,引理,2.5,令,M,Terms,(,)，,并且,是满足的项代数,Terms,(,),的环境，那么,M,M,证明,对项进行归纳证明,从,项代数可以知道，,只有,M,和,N,是语法上相同的项时，等式,M,N,才会永真,2,.3,等式、可靠性和完备性,2.3.3,语义蕴涵和等式证明系统,代数规范,Spec,E,:,基调,和一组等式,E,语义蕴涵：,E,M,N,满足,E,的所有代数,A,都满足等式,M,N,语义理论,E,：,如果,E,M,N,蕴涵,M,N,E,代数,A,的理论,Th,(,A,),在,A,中成立的所有等式的集合,这是一个,语义理论,2,.3,等式、可靠性和完备性,回顾,证明系统的可靠性,若等式,E,从一组假设,E,可证，则,E,语义上蕴涵,E,证明系统的完备性,若,E,语义上蕴涵等式,E,，则,E,从,E,可,证,下一步,先给出代数证明系统，然后讨论可靠性和完备性,1,、语义相等是个等价关系,，因此有,M,M,2,、在等式中增加类别指派,的规则,3,、等价代换,M,=,N,N,=,M,M,=,N,N,=,P,M,=,P,M,=,N,M,=,N,x,:,s,M,=,N,x,:,s,P,=,Q,P,/,x,M,=,Q,/,x,N,2,.3,等式、可靠性和完备性,x,不在中,P,Q,Terms,s,(,),2,.3,等式、可靠性和完备性,等式可证,若从,E,中的等式和公理(,ref,),及推理规则(,sym,)、,(,trans,)、(,subst,),和(,add,var,),可推出等式,M,N,，,则说该等式可证，写成,E,M,N,语法理论,如果,E,M,N,蕴涵,M,N,E,E,的语法理论,Th,(,E,),从,E,可证的所有等式的集合,2,.3,等式、可靠性和完备性,等式集合,E,是,语义一致的,若存在某个等式,M,N,，,它不是,E,的语义蕴涵,等式集合,E,是,语法一致的,若存在某个等式,M,N,，,它不能由,E,证明,2,.3,等式、可靠性和完备性,例,在基调,stk,S,F,上增加等式,top,(,push x s,)=,x,s,:,stack,x,:,nat,pop,(,push x s,)=,s,s,:,stack,x,:,nat,使用这些等式可以证明等式,top,(,push,3,empty,)=3,top,(,push,x s,)=,x,s,:,stack,x,:,nat,empty,=,empty,x,:,nat,top,(,push,x empty,)=,x,x,:,nat,3=3 ,top,(,push,3,empty,)=3 ,2,.3,等式、可靠性和完备性,导出规则,f:s,1,s,k,s,M,i,N,i,Terms,(,),M,和,N,中没有,x,Terms,s,(,),非空,M,=,N,N,=,P,P,=,Q,M,=,Q,M,1,=,N,1,M,k,=,N,k,f M,1,M,k,=,f N,1,N,k,M,=,N,x,:,s,M,=,N,s,i,2,.3,等式、可靠性和完备性,定理,2.6,（,可靠性,）,如果,E,M,N,，,那么,E,M,N,证明,可以根据该证明的长度进行归纳,归纳基础：长度为1的证明，它是公理或,E,的一个等式,归纳假设：,M,N,的最后一步是从,E,1,E,n,得到，那么，若,A,E,，,则,A,满足,E,1,E,n,要证明：若,A,满足最后一条规则的这些前提，则,A,满足,M,N,证明 根据证明,规则的集合，分情况进行分析,2,.3,等式、可靠性和完备性,命题,2.7,存在代数理论,E,和不含,x,的项,M,和,N,，,使得,E,M,=,N,x,:,s,，,但是,E,M,=,N,证明,令,基调有类别,a,和,b,，,函数符号,f,:,a,b,和,c,d,:,b,令,E,是包含能从,f x=,c,x,:,a,和,f x=,d,x,:,a,证明的所有等式,显然,c=,d,x,:,a,E,可以找到一个使等式,c,=,d,不成立的模型,a,和,b,对应的分别是空集和多于,2,个元素的集合,由可靠性，,c=,d,是不可能从,E,证明的,2,.3,等式、可靠性和完备性,例,栈代数规范,sorts:,nat,stack,fctns,:0,1,2,:,nat,+,:,nat,nat,nat,empty,:,stack,push,:,nat,stack,stack,pop,:,stack,stack,top,:,stack,nat,eqns,:s:,stack,;,x,:,nat,0+0=0,0+1=1,0 0=0,0 1=0,top,(,push x s,)=,x pop,(,push x s,)=,s,2,.3,等式、可靠性和完备性,等式,push,(,top s,)(,pop s,)=,s,s,:,stack,是不可证的,任何形式为,top empty,=,M,的等式都是不可证的，若,M,是类别为,nat,的项，并且,不含,empty,2,.3,等式、可靠性和完备性,2.3.4,完备性的形式,用于不同逻辑系统的三种不同形式的完备性,1,、最弱的形式,所有的永真公式都是可证的,2,、演绎完备性,每个语义蕴涵在证明系统中都是可推导的,3,、最小模型完备性,每个语法理论都是某个,“,最小,”,模型的语义理论,对代数来说，最小模型完备性意味着每个语法理论是某个代数,A,的,Th,(,A,),“,最小模型,”,是指它的理论包含的等式最少,2,.3,等式、可靠性和完备性,最小模型完备性不一定成立,考虑等式,E,x,=,y,x,:,a,y,:,a,z,:,b,1,、,a,的载体只含一个元素,，则,E,满足，此时,E,1,x,=,y,x,:,a,y,:,a,成立,2,、,b,的载体为空,，则,E,也,满足，此时,E,2,z,=,w,z,:,b,w,:,b,成立,E,1,和,E,2,都不是,E,的语义蕴涵,不存在代数，其理论正好就是由,E,的等式推论,组成的语法理论,2,.3,等式、可靠性和完备性,2.3.5,同余、商和演绎完备性,同余关系,：等价关系加上同余性,同余性：指函数保可证明的相等,性,对单类代数,A,=,A,f,1,A,f,2,A,同余关系是载体,A,上的等价关系，使得对每个,k,元函数,f,A,，,若,a,i,b,i,(,i,=1,k,)，,即,a,i,和,b,i,等价，则,f,A,(,a,1,a,k,),f,A,(,b,1,b,k,),对多类代数,A,=,A,s,I,同余关系是一簇等价关系,s,s,A,s,A,s,，,使得对每个,f,:,s,1,s,k,s,及变元序列,a,1,a,k,和,b,1,b,k,(,a,i,s,b,i,A,s,),有,f,A,(,a,1,a,k,),s,f,A,(,b,1,b,k,),i,i,2,.3,等式、可靠性和完备性,A,模的商的代数,A,把,A,中有,关系元素,a,a,压缩成,A,的一个元素,等价类,a,a,a,A,s,a,a,商代数,A,定义：,(,A,),s,是由,A,s,的所有等价类构成的集合,A,s,s,a,s,a,A,s,函数,f,A,由,A,的函数,f,A,确定,对适当载体的,a,1,a,k,，,f,A,(,a,1,a,k,)=,f,A,(,a,1,a,k,),2,.3,等式、可靠性和完备性,上面定义有意义的条件是,f,A,(,a,1,a,k,),必须只依赖于,a,1,a,k,，,而不能依赖于所选的代表,a,1,a,k,例,单类别代数,N,，,0,，,1,，,上的同余关系,“,模,k,等价,”,这个商代数是众所周知的整数模,k,的加结构。如果,k,等于5，那么3 4 2,2,.3,等式、可靠性和完备性,如果,是,A,的一个环境，是一个同余关系，那么,A,的环境,定义如下：,(,x,)=,(,x,),反过来，对于,A,的环境,，对应它的,A,的环境,有多种选择,引理,2.8,令是代数,A,上的同余关系，项,M,Terms,(,),并且,是满足的环境。那么项,M,在商代数,A,和环,境,下的含义(,A,),M,由下式决定,(,A,),M,=,A,M,2,.3,等式、可靠性和完备性,引理,2.9,令,E,是一组,等式集合，令,Terms,(,),是基调,上,的项集。由,E,的可证明性确定的关系,E,是,Terms,(,),上的同余关系,定理,2.10,（,完备性,）,如果,E,M,N,，,那么,E,M,N,完备性定理加上可靠性定理表明语法理论和语义理论相同,2,.3,等式、可靠性和完备性,2.3.6,非空类别和最小模型性质,没有空载体的代数有最小模型完备性,类别,s,非空：集合,Terms,s,(,),不是空集,对应的载体肯定非空,没有,空载体,时，可以增加推理规则(,nonempty,),定理,2.11,令,E,是封闭于规则,（,nonempty,）,的语法理论，那,么存在所有的载体都非空的代数,A,，,使得,E,Th,(,A,),M,=,N,x,:,s,M,=,N,2.4,同态和初始性,2.4.1,同态和同构,将同态和同构概念从单类代数推广到多类代数,同态是从一个代数到另一个代数的保结构的映射,从代数,A,到,B,的同态,h,:,A,B,一簇映射,h,=,h,s,|,s,S,，,使得对的每个函数符号,f,:,s,1,s,k,s,，,有,h,s,(,f,A,(,a,1,a,k,)=,f,B,(,h,s,(,a,1,),h,s,(,a,k,),1,k,2.4,同态和初始性,例,令,N,=,N,0,1,，,是模,k,的等价关系,则把,n,N,映射到它的等价类,n,是从,N,到,N,的一个同态，,因为,h,(0)=0,N,=0,h,(,n,+,m,)=,h,(,n,),N,h,(,m,)=,n,+,m,任何代数到它商代数的同态都用这种方式定义,2.4,同态和初始性,例,含义函数是从项代数,T,=,Terms,(,),到任意代数,A,的一个同态,h,:,T,A,。,如果,是,A,的一个满足,的环境，该同态的定义是,h,(,M,)=,A,M,这是一个同态，因为,h,(,f M,1,M,k,)=,A,f M,1,M,k,=,f,A,(,A,M,1,A,M,k,),=,f,A,(,h,(,M,1,),h,(,M,k,),2.4,同态和初始性,引理,2.13,令,h,:,A,B,是任意同态，并且,是满足类别指派,的任意,A,环境。那么对任何项,M,Terms,(,)，,有,h,(,A,M,)=,B,M,h,当,M,中不含变量时，,h,(,A,M,)=,B,M,证明,基于项的归纳,引理,2.14,如果,h,:,A,B,和,k,:,B,C,都是,代数的同态，那么,合成,k,h,:,A,C,也是,代数的同态,，(,k,h,),s,=,k,s,h,s,同构,一个双射的同态,写成,A,B,2.4,同态和初始性,2.4.2,初始代数,C,是一类,代数并且,A,C,，,若对每个,B,C,，,存在唯一的同态,h,:,A,B,，,则,A,在,C,中叫做,初始代数,初始代数是“典型”的,初始代数有尽可能少的非空载体,初始代数满足尽可能少的闭等式,A,B,3,B,2,B,1,2.4,同态和初始性,例,基调,0,类别,nat,，,函数符号0:,nat,和,S,:,nat,nat,令,C,是所有,0,代数构成的代数类,闭项代数,T,Terms,(,0,),是,C,的初始代数,它的载体是所有闭项,0,S,(0),S,k,(0),该代数的函数,S,把,S,k,(0),映射到,S,k,1,(0),该代数的元素少到能解释所有的函数符号,该代数满足项之间尽可能少的等式,2.4,同态和初始性,引理,2.15,假定,h,:,A,B,和,k,:,B,A,都是同态，并且,h,k,=,Id,B,，,k,h,=,Id,A,。,那么,A,和,B,同构,命题,2.16,若,A,和,B,在代数类,C,中都是初始代数，则,A,和,B,同构,命题,2.17,令,E,是一组,等式，且令,A,=,Terms,(,),E,是模,可证明的相等性的代数，则,A,对,E,来说是初始代数,由项代数和商的性质可知，从,E,可证明的等式在,A,中都成立,还要证明从,A,到任何满足,E,的代数有唯一的同态,2.4,同态和初始性,例,sorts:,nat,fctns,:0:,nat,S,:,nat,nat,:,nat,nat,nat,；,eqns,：,x,:,nat,y,:,nat,x,+0=,x,x,+(,Sy,)=,S,(,x,+,y,),可以证明如下事实：,S,k,0+,S,l,0=,S,k,+,l,0,对任何闭项,M,，,存在某个自然数,k,，,使得,M,=,S,k,0,2.4,同态和初始性,例,x,+0=,x,x,+(,Sy,)=,S,(,x,+,y,),可以证明如下事实：,等式,S,k,0=,S,l,0,是不可证的，除非,k,=,l,每个等价类正好包含一个形式为,S,k,0,的项,等价类集和形式为,S,k,0,的项集间有一个双射,若把闭项集合,0,S,0,S,k,0,作为载体，函数,S,映射,S,k,0,S,k,1,0，,映射(,S,k,0,S,l,0),S,k,l,0，,则得一个初始代数,这个初始代数和该基调的标准模型（有后继算子和加法的自然数）同构,2.4,同态和初始性,初始代数和其他代数的比较,1,、和有更多元素的代数比较,多余的元素不能,由项定义（有垃圾）,例,1,：整数代数,Z,例,2,：,A,=,A,nat,0,A,S,A,+,A,A,nat,=(0,N,)(1,Z,),0,A,=0,0,S,A,i,n,=,i,n,+1,i,n,+,A,j,m,=,max,(,i,j,),n,+,m,2.4,同态和初始性,初始代数和其他代数的比较,2,、和有较少元素的代数比较,一些不能证明为相等,的项在该代数中被等同（有混淆）,例：模,k,的自然数,2.4,同态和初始性,初始代数的一个重要特点,初始代数可能,会满足不能由,E,证明的额外的等式,例：自然数基调例子中，初始代数满足,等式,x,+,y,=,y,+,x,因为,E,M,=,S,k,0,和,E,N,=,S,l,0,蕴涵,E,M,+,N,=,S,k,+,l,0=,N,+,M,2.4,同态和初始性,自然数基调例子中，初始代数满足,等式,x,+,y,=,y,+,x,不满足交换律的代数,A,nat,是所有,f,:,X,X,的函数的集合（,X,至少有两个元素,）,0,A,是,X,上的恒等函数，,S,A,是,A,nat,上的恒等映射,+,A,是,A,nat,上的函数合成,A,=,A,nat,0,A,S,A,+,A,满足,E,+,A,没有交换性，因为函数合成没有交换性,2.4,同态和初始性,基项、基代换、基实例（项、等式）,如果,M,N,是,Terms,s,(,),的项之间的等式，并且,S,是一个,，,基代换，则把,SM,SN,称为,M,N,的,基实例,命题,2.18,令,E,是一组,等式，且,A,对,E,来说是初始代数，则,对任何,等式,M,N,，,下面三个条件等价,A,满足,M,N,A,满足,M,N,的每一个基实例,M,N,的每一个基实例都可以从,E,证明,2.5,代数数据类型,2.5.1,代数数据类型,本节讨论数据类型公理化方法的一般特征,程序设计中的很多数据类型,不存在标准的数学构造，如优先队列和符号表,没有单一和标准的计算机实现,通常是列出它们的操作并公理化地描述这些操作之间的关系,因此是公理化地定义而不是由数学构造来定义,困难之处：对于一个数据类型，,难以断定是否有了,“,足够,”,的公理,2.5,代数数据类型,数据抽象的一般原理,抽象数据类型由它的规范定义,使用这样数据类型的程序应该只依赖于由它的规范保证的性质，而不依赖于它的任何特定实现,一个数据类型的函数可以划分成,构造算子：产生该数据类型的一个新元素,运算算子：,是该数据类型上的函数，但不产生新的元素,观察算子：,应用于该数据类型的元素，但返回其它类型的元素，如自然数或布尔值,2.5,代数数据类型,2.5.2,初始代数语义和数据类型归纳,代数规范有几种不同的,“,语义,”,形式,宽松语义：,满足一个代数规范的所有代数所构成的代数类,初始代数语义：,满足一个代数规范的所有初始代数所构成的同构类,终结代数语义：,满足一个代数规范的所有,终结,代数所构成的同构类,生成语义：,满足一个代数规范的所有,生成,代数所构成的代数类,2.5,代数数据类型,初始代数的性质,没有垃圾,没有混淆,支持基于数据类型构造符的归纳,构造符集合,Spec,E,的函数符号集合的子集,F,0,，使得,Terms,(,),E,的每个等价类正好只含一个由,F,0,的函数符号所构成的基项,可以基于对构造符的归纳,来证明初始代数的性质,2.5,代数数据类型,sorts:,set,nat,bool,构造符,、运算符、,观察符,fctns,:,0,1,2,:,nat,+,:,nat,nat,nat,Eq,?:,nat,nat,bool,true,false,bool,empty,:,set,insert,:,nat,set,set,union,:,set,set,set,ismem,?:,nat,set,bool,cond,n,:,bool,nat,nat,nat,.,eqns,:,x,y,:,nat,s,s,:,set,u,v,:,bool,0+0=0,0+1=1,1+1=2,.,Eq,?,x x,=,true,Eq,?0 1,=,false,Eq,?0 2,=,false,.,ismem,?,x empty,=,false,ismem,?,x,(,insert y s,)=if,Eq,?,x y,then,true,else,ismem,?,x s,union empty s,=,s union,(,insert y s,),s,=,insert y,(,union s s,),cond,n,true x y,=,x,cond,n,false x y,=,y .,2.5,代数数据类型,终结代数,在一个代数类,C,中，如果从其中的每个,B,到其中某,个,A,，,都存在唯一的同态，那么代数,A,是终结代数,一个代数类中的所有终结代数都同构,若用终结代数作为语义，则称之为终结语义,如果所有载体都是单元素集合的代数也在,C,中，则这个代数一定是,C,的终结代数,2.5,代数数据类型,初始语义和终结语义,初始语义：不能证明为相等的就是不相等的,终结语义：不能证明为不相等的则是相等的,如果把某些,类别的解释固定，而其它类别的解释用用终结语义，则它是一个有用的方法,从初始语义角度看，前面给出的不是集合的规范,而是表的规范。因为不能证明,insert,x,(,insert,y,z,)=,insert,y,(,insert,x z,),x,:,nat,y,:,nat,z,:,set,insert,x,(,insert,x z,)=,insert,x,z,x,:,nat,z,:,set,若用终结,语义，且,bool,的解释固定,则为集合规范,2.5,代数数据类型,2.5.3,解释没有意义的项,表达式没有意义的情况,除法是一个部分函数，除数为零的表达式没意义,调用不终止的函数也构成一个没有意义的表达式,如果想在代数,规范中表示这些情况，必须在基调中增加表示错误的项（简称错误值）,怎样规定这些项的值？有三种可能：,什么也不规定,任意做一个决定,非常仔细地说明什么是所需要的,2.6,重写系统,2.6.1,基本定义,重写系统：用于代数项的归约系统,R,两种重要的应用,为代数项提供一种计算模型,自动定理证明,由一组叫做重写规则(,L,R,)的有向等式组成,限制：,Var,(,R,),Var,(,L,),由,R,确定的一步归约关系,R,SL,x,M,R,SR,x,M,关系,R,是,R,的自反传递闭包,2.6,重写系统,sorts:,nat,fctns,:0:,nat,:,nat,nat,+:,nat,nat,nat,在这个基调上的一些归约规则如下：,x,0,x,x,+(,x,)0,(,x,y,),z,x,+(,y,+,z,),实例：,(,x,y,)(,y,),x,+,(,y,+(,y,),x,0,x,2.6,重写系统,引理,2.19,（,归约保类别,）,令,R,是,上的重写系统，若,M,Terms,s,(,),且,M,R,N,，,则,N,Terms,s,(,),如果,N,M,P,蕴涵,N,P,，则关系,（,重写系统,）,是,合流的,若不存在一步归约的无穷序列,M,0,M,1,M,2,，则关系（,重写系统,）是终止的,不能再归约的项称为,范式,合流且终止的重写系统通常又叫做典范系统,2.6,重写系统,可变换性,若存在,M,M,1,M,2,M,3,M,k,N,，,则项,M,N,Terms,s,(,),是,可变换的，写成,M,R,N,归约的无向版本,箭头的方向并没有什么意义,对任何重写,系统，可变换性以及可证明的相等性（把重写规则看成等式）是一致的,2.6,重写系统,用自然数的有穷序列来表示项中的,位置,位置,n,=1,2,的子项是,hab,用,M,n,表示,M,在,位置,n,的子项,用,N,n,M,表示,M,在,n,的子项由,N,代换的结果,便于,引用子项的某个特定出现,f,g,g,x,x,h,a,b,a,b,f,(,gx,(,hab,)(,gba,),x,2.6,重写系统,2.6.2,合流性和可证明的相等性,记号,若,R,是一组重写规则，,E,R,用来表示对应的无向的,等式集合,定理,2.20,1,、,对任何重写系统,R,，,M,R,N,当且仅当,E,R,M,N,；,2,、对任何合流的重写系统,R,，,E,R,M,N,当且仅当,M,R,R,N,2.6,重写系统,2.6.3,终止性,良基关系,集合,A,上的一个关系,是,良基的,，如果不存在,A,上,元素的无穷递减序列,a,0,a,1,a,2,的话,如果,能在项和有良基关系的集合,A,的元素间建立起一个对应，那么可以利用它去证明不存在无穷的归约序列,M,0,M,1,M,2,有几种方式可把项映射到有良基关系的集合,1,、利用项的语法特点,2,、利用代数的语义结构（下面用这种方式）,2.6,重写系统,代数,A,=,A,s,1,A,s,2,f,1,A,f,2,A,是良基的，若,每个载,体,A,s,上有一个良基关系,s,对每个,n,元函数符号,f,，,如果,x,1,y,1,x,n,y,n,并且对某个,i,（1,i,n,）,有,x,i,y,i,，,那么,f,A,(,x,1,x,n,),f,A,(,y,1,y,n,),若,A,是良基代数，并且,M,和,N,都是类别,s,上的项，若,M,s,N,，,则写成,A,M,N,如果对任何环境,都有,A,M,N,，,那么写成,A,M,N,2.6,重写系统,定理,2.22,令,R,是,项上的一个重写系统，并且令,A,是一个,良基的,代数。如果对,R,中每条规则,L,R,都,有,A,L,R,，,那么,R,是终止的,例,x,x,载体,A,bool,N,0,1,(,x,y,)(,x,y,),A,(,x,y,)=,x,+,y,+1,(,x,y,)(,x,y,),A,(,x,y,)=,x,y,x,(,y,z,)(,x,y,)(,x,z,),A,(,x,)=2,x,(,y,z,),x,(,y,x,)(,z,x,),各重写规则的左部定义的值都大于其右部定义的值,2.6,重写系统,2.6.4,临界对,局部合流,关系,是局部合流的，若,N,M,P,蕴涵,N,P,局部合流关系严格弱于合流关系,例,a,b,b,a,a,a,0,b,b,0,a,0,a,b,b,0,2.6,重写系统,cond,B,(,cdr,(,cons,s l,),(,cons,(,car,l,)(,cdr,l,),规则如下：,cdr,(,cons,x l,),l,cons,(,car,l,)(,cdr,l,),l,不相交的归约,M,SL,SL,M,SR,SL,M,SL,SR,M,SR,SR,2.6,重写系统,cdr,(,cons,x,(,cons,(,car,l,)(,cdr,l,),),规则如下：,cdr,(,cons,x l,),l,cons,(,car,l,)(,cdr,l,),l,平凡的重迭,SL,SL,SL,SR,SR,SL,SL,SR,SR,SR,2.6,重写系统,cdr,(,cons,(,car,l,)(,cdr,l,),),规则如下：,cdr,(,cons,x l,),l,cons,(,car,l,)(,cdr,l,),l,非平凡的重迭,SL,SL,SL,SR,SR,?,2.6,重写系统,临界对,L,R,cdr,(,cons,x l,),l,L,R,cons,(,car,l,)(,cdr,l,),l,非平凡重迭是一个三元组,SL,，,SL,，,m,二元组,SR,，,SR,m,SL,叫做临界对,该例有两个临界对,第一个如下：,SL,是,cdr,(,cons,(,car,l,)(,cdr,l,),临界对是,cdr,l,cdr,l,2.6,重写系统,第二个如下：,L,R,cons,(,car,l,)(,cdr,l,),l,L,R,cdr,(,cons,x l,),l,SL,是,cons,(,car,(,cons x,l,)(,cdr,(,cons,x l,),临界对,是,cons x l,cons,(,car,(,cons x l,),l,若,f,(,gxy,),R,，,若,L,中有子项,f,(,h,),，则,f,(,h,),是不可能与,f,(,gxy,),合一,同一条规则,的两次使用可能引起重迭，如,f,(,f x,),af,(,f,(,f,x,),左部,完全相同的情况,：,L,R,和,L,R,2.6,重写系统,命题,一个重写系统,R,是局部合流的，当且仅当对每个临界对,M,N,有,M,R,R,N,证明,从左到右的蕴涵是简单明了的,另一个方向的证明仿照用于启发临界对定义的推理：不相交,、平凡的重迭、临界对的代换实例,如果一个有限的重写系统,R,是终止的，那么该命题就给出一个算法，可用于判定,R,是否局部合流,2.6,重写系统,2.6.5,左线性无重迭重写系统,无重迭：没有非平凡的临界对,无重迭,的重写系统不一定是合流的,例如：,S,Eq,?,x x,true,Eq,?,x,(,S x,),false,Eq,?,有两个不同的范式,Eq,?,true,Eq,?,Eq,?,(,S,),false,2.6,重写系统,左线性的规则,任何变量在规则的左部的出现不超过一次的话,左线性的系统,每一条规则都是左线性的,命题,如果,R,是左线性和无重迭的，那么,R,是合流的,例,car,(,cons x l,),x,cdr,(,co