《【教学课件】第3章泛代数和代数数据类型.ppt》由会员分享，可在线阅读，更多相关《【教学课件】第3章泛代数和代数数据类型.ppt（83页珍藏版）》请在三一办公上搜索。
1、第3章 泛代数和代数数据类型,PCF语言的三部分组成带函数和积类型的纯类型化演算自然数类型和布尔类型不动点算子第3章到第5章对这三部分进行透彻的研究本章研究像自然数类型和布尔类型这样的代数数据类型,3.1 引 言,代数数据类型包括一个或多个值集一组在这些集合上的函数基本限制是其函数不能有函数变元基本“类型”符号被称为“类别”泛代数（也叫做等式逻辑）定义和研究代数数据类型的一般数学框架本章研究泛代数和它在程序设计中定义常用数据类型时的作用,3.1 引 言,本章主要内容：代数项和它们在多类别代数中的解释等式规范（也叫代数规范）和等式证明系统等式证明系统的可靠性和完备性（公理语义和指称语义的等价）代
2、数之间的同态关系和初始代数数据类型的代数理论从代数规范导出的重写规则（操作语义）大多数逻辑系统中一些公共的议题将被覆盖,3.2 代数、基调和项,3.2.1 代数代数一个或多个集合，叫做载体一组特征元素和一阶函数，也叫做代数函数f:A1 Ak A例：N N,0,1,+,载体N是自然数集合特征元素0,1N，也叫做零元函数函数+,:N N N,3.2 代数、基调和项,多个载体的例子Apcf N,B,0,1,+,true,false,Eq?,下面开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要定义数据类型证明性质进行化简还必须讨论这种语法描述的语义A5pcf N5,B,0,1,2,
3、3,4,+5,true,false,Eq?,3.2 代数、基调和项,代数项的语法基调 S，FS是一个集合，其元素叫做类别函数符号f:s1 sk s的集合F，其中表达式s1 sk s叫做类型零元函数符号叫做常量符号例N S，Fsorts:natfctns:0,1:nat,:nat nat nat,3.2 代数、基调和项,定义基调的目的是用于写代数项考虑项中有变量的情况，需假定有一个无穷的符号集合V，其元素称为变量类别指派 x1:s1,xk:sk基调 S，F和类别指派上类别s的代数项集合Termss(,)如果x:s，那么x Termss(,)如果f:s1 sk s并且Mi Termssi(,)(i
4、 1,k)，那么f M1 Mk Termss(,)当k 0时，如果f:s，那么f Termss(,),3.2 代数、基调和项,例0,0 1 Termsnat(N,)0 x Termsnat(N,)，其中 x:nat,代数项中无约束变元，NxM就是简单地把M中x的每个出现都用N代替就是了记号,x:s x:s引理 如果M Termss(,x:s)并且N Termss(,)，那么NxM Termss(,)证明 按Termss(,)中项的结构进行归纳,3.2 代数、基调和项,例用基调stk S,F来写自然数和栈表达式sorts:nat,stackfctns:0,1,2,:nat,:nat nat na
5、tempty:stackpush:nat stack stackpop:stack stacktop:stack natpush 2(push 1(push 0 empty)是该基调的项,3.2 代数、基调和项,3.2.3 代数以及项在代数中的解释代数是为代数项提供含义的数学结构是一个基调，则代数A包含对每个s S，正好有一个载体As一个解释映射I 把函数I(f):As1 Ask As指派给函数符号 f:s1 sk s F把I(f)As指派给常量符号f:s F N代数N写成N N,0N,1N,N,N,3.2 代数、基调和项,代数A的环境:V s As环境 满足如果对每个x:s 都有(x)AsM
6、 Termss(,)的含义AMAx(x)AM f A(AM1,AMk)若f:s是常量符号，则Af f AA清楚时，省略A而直接写成M不依赖于时，用AM表示M在A中的含义,3.2 代数、基调和项,例 若(x)0N x 1 N(x,1)N(x),1N)N(0N,1N)1N,3.2 代数、基调和项,例 Astk N,N,0A,1A,A,A,emptyA,pushA,pop A,top A empty A,空序列push A(n,s)n:spop A(n:s)spop A()top A(n:s)ntop A()0 A若把x:nat映射到3A，把s:stack映射到2A,1A pop(push x s)
7、popA(pushA(x,s)popA(pushA(3A,2A,1A)popA(3A,2A,1A)2A,1A,3.2 代数、基调和项,引理 令A是一个代数，M Termss(,)，并且是满足的环境，那么M As证明 根据Termss(,)中项的结构进行归纳引理 令x1,xk是由出现在M Termss(,)中的所有变量构成的变量表，1和2是满足的两个环境,并且对i 1,k有1(xi)2(xi),那么M1 M2证明 基于项结构的归纳,3.2 代数、基调和项,3.2.4 代换引理引理 令M Termss(,x:s)并且 N Termss(,)，那么NxMTermss(,)。并且对任何环境，有 NxM
8、 M(x a)，其中a N是N在下的含义证明 根据项M的结构进行归纳,3.3 等式、可靠性和完备性,3.3.1 等式代数规范：一个基调+一组等式调查什么样的代数满足这些等式强加的要求使用等式证明系统可推导新的等式可靠性：从规范可证明的等式在任何满足该规范的代数中都成立完备性：在满足规范的所有代数中都成立的等式都可从该规范证明代数规范是描述代数数据类型公理语义的工具,3.3 等式、可靠性和完备性,空载体提出一个技术问题逻辑公式若A=，则公式x:A.F(x)为真若A=，则公式x:A.F(x)为假对任意的M,N Termss(,)，如果x:s 且As为空，那么M和N看成是相等的项只有一个类别时，假定
9、该类别非空是有意义的,3.3 等式、可靠性和完备性,等式公式M N 对某个s，M,N Termss(,)如果满足，那么若M N，就说代数A在环境下满足M N，写成A,M N若A在任何环境下都满足，写成 A M N如果一类代数C中的任何一个代数A都满足，写成 C M N任何一个代数都满足等式M N，写成 M N(永真的、有效的),3.3 等式、可靠性和完备性,如果A满足上的所有等式，就说代数A是平凡的例令有两个类别a和b，令A是一个代数，其中Aa0,1并且Ab。A不可能满足x yx:a,y:a，即下式不成立 A x yx:a,y:a但是A x yx:a,y:a,z:b无意义地成立,3.3 等式、
10、可靠性和完备性,项代数项代数Terms(,)类别s的载体：集合Termss(,)函数符号f:s1 sk s的解释I(f)(M1,Mk)f M1 Mk项代数Terms(,)的环境也叫做一个代换如果S是代换，则用SM表示同时把M中的各个变量x用Sx替换的结果因此用M表示把代换作用于M的结果,3.3 等式、可靠性和完备性,例类别u函数符号f:u u和g:u u u a:u,b:u,c:uTu 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(f a)(f(f b),3.3 等式、可靠性
11、和完备性,引理 令M Terms(,)，并且是满足的项代数Terms(,)的环境，那么M M证明 对项进行归纳证明从项代数可以知道，只有M和N是语法上相同的项时，等式M N才会永真,3.3 等式、可靠性和完备性,代数规范Spec,E:一个基调和一组等式E语义蕴涵：E M N满足E的所有代数A都满足等式M N语义理论：如果E M N蕴涵M N E代数A的理论Th(A)在A中成立的所有等式的集合这是一个语义理论,3.3 等式、可靠性和完备性,证明系统的可靠性：若一个等式从一组假设E是可证明的，那么E语义上蕴涵该等式证明系统的完备性：如果E语义上蕴涵一个等式，那么该等式可从E证明下面先给出代数证明系
12、统,3.3 等式、可靠性和完备性,语义相等是个等价关系，因此有M M在等式中增加类别指派的规则等价代换P,Q Termss(,),3.3 等式、可靠性和完备性,等式是可证明：如果从E中的等式和公理(ref)及推理规则(sym)、(trans)、(subst)和(add var)可以推出等式M N，那么就说该等式可证明，写成E M N 语法理论如果E M N蕴涵M N EE的语法理论Th(E)从E可证明的所有等式的集合,3.3 等式、可靠性和完备性,等式集合E是语义一致的如果存在某个等式M N，它不是E的语义蕴涵等式集合E是语法一致的如果存在某个等式M N，它不能由E证明,3.3 等式、可靠性和
13、完备性,例 在基调stk S,F上增加等式top(push x s)=xs:stack,x:natpop(push x s)=ss:stack,x:nat使用这些等式可以证明等式top(push 3 empty)=3,3.3 等式、可靠性和完备性,导出规则 f:s1 sk s Mi,NiTermssi(,)M和N中没有x，Termss(,)非空,3.3 等式、可靠性和完备性,定理（可靠性）如果E M N，那么E M N证明 可以根据该证明的长度进行归纳归纳基础：长度为1的证明，它是公理或E的一个等式归纳假设：M N的最后一步是从E1,En得到。那么，如果A E，则A满足E1,En要证明：如果A
14、满足最后一条规则的这些前提，那么A满足M N证明 根据证明规则的集合，分情况进行分析,3.3 等式、可靠性和完备性,命题 存在一个代数理论E和不含x的项M和N，使得E M=N,x:s，但是E M=N 证明 令基调有类别a和b，函数符号f:a b和c,d:b令E是包含能从 f x=cx:a和 f x=d x:a证明的所有等式显然c=d x:a E可以找到一个使等式c=d 不成立的模型由可靠性，c=d 是不可能从E证明的,3.3 等式、可靠性和完备性,例 栈代数规范sorts:nat,stackfctns:0,1,2,:nat+,:nat nat nat empty:stack push:nat
15、stack stack pop:stack stack top:stack nateqns:s:stack;x:nat0+0=0,0+1=1,0 0=0,0 1=0,top(push x s)=x pop(push x s)=s,3.3 等式、可靠性和完备性,等式push(top s)(pop s)=ss:stack是不可证明的任何形式为top empty=M的等式都是不可证明的，假定M是类别为nat的项，并且不含empty,3.3 等式、可靠性和完备性,3.3.4 完备性的形式用于不同逻辑系统的三种形式的完备性最弱的形式：所有的永真公式都是可证的演绎完备性：每个语义蕴涵在证明系统中都是可推导
16、的最小模型完备性：每个语法理论是某一个“最小”模型的语义理论对代数来说，最小模型完备性意味着每个语法理论是某个代数A的Th(A)“最小模型”是指它的理论包含的内容最少,3.3 等式、可靠性和完备性,最小模型完备性不一定成立，考虑等式E=def x=y x:a,y:a,z:b 情况1：a的载体只含一个元素，则E满足，此时E1=def x=y x:a,y:a 成立 情况2：b的载体为空，则E也满足，此时E2=def z=w z:b,w:b 成立E1和E2都不是E的语义蕴涵不存在一个代数，其理论正好就是由E的等式推论组成的语法理论,3.3 等式、可靠性和完备性,3.3.5 同余、商和演绎完备性同余关
17、系：等价关系加上同余性同余性：指函数保可证明的相等性对单类代数A=A,f1A,f2A,，同余关系是载体A上的等价关系，使得对每个k元函数fA，如果aibi(i=1,k)，即ai和bi等价，那么f A(a1,ak)fA(b1,bk)。对多类代数A=As,I，同余关系是一簇等价关系 s,s AsAs，使得对每个f:s1 sks及变元序列a1,ak和b1,bk(其中ai sibi Asi),有f A(a1,ak)s f A(b1,bk),3.3 等式、可靠性和完备性,A模的商的代数A把A中有关系的元素a a 压缩成A的一个元素等价类aa a As a a 商代数A定义：(A)s是由As的所有等价类构
18、成的集合Ass as a As函数fA由A的函数fA确定：对适当载体的a1,ak，f A(a1,ak)=f A(a1,ak),3.3 等式、可靠性和完备性,上面定义有意义的条件是f A(a1,ak)必须只依赖于a1,ak，而不能依赖于所选的代表a1,ak。例 单类别代数N，0，1，上的同余关系“模k等价”这个商代数是大家熟悉的整数模k加结构。如果k等于5，那么3 4 2,3.3 等式、可靠性和完备性,如果是A的一个环境，是一个同余关系，那么A的环境 定义如下：(x)=(x)反过来，对于A的环境，对应它的A的环境有多种选择引理 令是代数A上的同余关系，项MTerms(,)并且是满足的环境。那么项
19、M在商代数A 和环境下的含义(A)M由下式决定(A)M=AM,3.3 等式、可靠性和完备性,引理 令E是一组等式集合，令Terms(,)是基调上的项集。由E的可证明性确定的关系E,是Terms(,)上的同余关系定理（完备性）如果E M N，那么E M N完备性定理加上可靠性定理表明语法理论和语义理论相同,3.3 等式、可靠性和完备性,3.3.6 非空类别和最小模型性质类别s非空：集合Termss(,)不是空集对应的载体肯定非空没有空载体时，可以增加推理规则(nonempty)定理 令E是封闭于规则（nonempty）的语法理论，那么存在所有载体都非空的代数A，使得E Th(A)没有空载体的代数
20、有最小模型完备性,3.4 同态和初始性,3.4.1 同态和同构将同态和同构的概念从单类代数推广到多类代数 同态是从一个代数到另一个代数的保结构的映射（或叫做翻译）从代数A到B的同态h:A B一簇映射h=hs|s S，使得对的每个函数符号f:s1 sk s，有hs(f A(a1,ak)=(f B(hs1a1,hskak),3.4 同态和初始性,例 令N=N,0,1,，令是模k的等价关系。那么把nN映射到它的等价类n是从N到N的一个同态，因为h(0)=0N=0h(n+m)=h(n)N h(m)=n+m任何代数到它商代数的同态都用这种方式定义,3.4 同态和初始性,例 含义函数是从项代数T=Term
21、s(,)到任意代数A的一个同态h:T A。如果是A的一个满足的环境，该同态的定义是h(M)=AM这是一个同态，因为h(f M1 Mk)=Af M1 Mk=f A(AM1 AMk)=f A(h(M1)h(Mk),3.4 同态和初始性,引理 令h:A B是任意同态，并且是满足类别指派的任意A环境。那么对任何项M Terms(,)，有h(AM)=BMh当M中不含变量时，h(AM)=BM证明 基于项的归纳引理 如果h:A B和k:B C都是代数的同态，那么合成k h:A C也是代数的同态。(k h)s=ks hs)同构 一个双射的同态,写成A B,3.4 同态和初始性,3.4.2 初始代数C是一类代数
22、并且AC，若对每个BC，存在唯一的同态h:A B，那么A在C中叫做初始代数初始代数是“典型”的初始代数有尽可能少的非空载体初始代数满足尽可能少的闭等式,3.4 同态和初始性,例 基调0类别nat，函数符号0:nat和S:nat nat。令C是所有0代数构成的代数类闭项代数T Terms(0,)是C的初始代数它的载体是所有闭项0,S(0),S k(0),该代数的函数S把Sk(0)映射到Sk1(0)该代数的元素少到能解释所有的函数符号该代数满足项之间尽可能少的等式,3.4 同态和初始性,引理 假定h:A B和k:B A都是同态，并且h k=IdB，k h=IdA。那么A和B同构命题 如果A和B在代
23、数类C中都是初始代数，那么A和B是同构的命题 令E是一组等式，并且令A=Terms(,)E,是模可证明的相等性的代数。那么，A对E来说是初始代数由项代数和商的性质可知，从E可证明的等式在A中都成立还要证明从A到任何满足E的代数有唯一的同态,3.4 同态和初始性,例 基调1：类别nat；函数符号0:nat，S:nat nat和:nat nat nat；等式集合E：x+0=xx+(Sy)=S(x+y)Sk0+Sl0=Sk+l0对任何闭项M，存在某个自然数k，使得M=Sk0等式Sk0=Sl0是不可证明的，除非k=l每个等价类正好包含一个形式为Sk0的项等价类和形式为Sk0的项集间有一个双射载体看成由
24、闭项0,S0,Sk0,构成的集合，函数S映射Sk0 Sk10，映射(Sk0,Sl0)Skl0，得一个初始代数这个初始代数和该基调的标准模型（有后继算子和加法的自然数）同构,3.4 同态和初始性,该规范的初始代数可以和其它有更多或较少元素的代数相对照如果一个代数有更多元素的话，那么这些多余的元素不能由项定义。（有假货）整数代数ZA=Anat,0A,SA,+AAnat=(0 N)(1 Z)0A=0,0SAi,n=i,n+1i,n+A j,m=max(i,j),n+m如果一个代数有较少元素的话，那么就有一些不能被证明为相等的有区别的元素被等同。（出现混淆）模k的自然数,3.4 同态和初始性,初始代数
25、可能满足不能由E证明的额外的等式例 上面的自然数基调例子中，初始代数满足等式x+y=y+x 因为 E M=Sk0和E N=Sl0 蕴涵 E M+N=Sk+l0=N+M不满足交换性的代数Anat是所有f:X X的函数的集合（X至少有两个元素）0A是X上的恒等函数，SA是Anat上的恒等映射+A是Anat上的函数合成A=Anat 0A SA+A 满足E+A没有交换性，因为函数合成没有交换性,3.4 同态和初始性,基项、基代换、基实例（项、等式）如果M N是Termss(,)的项之间的等式，并且S是一个，基代换，那么就把SM SN称为M N的基实例命题 令E是一组等式，并且A对E来说是初始代数。对任
26、何等式M N，下面三个条件等价 A满足M NA满足M N的每一个基实例M N的每一个基实例都可以从E证明,3.5 代数数据类型,3.5.1 代数数据类型很多数据类型不存在标准的数学构造没有单一和标准的计算机实现列出它们的操作并描述这些操作的行为公理化地定义而不是由数学构造来定义对于一个数据类型，是否可以断定有了“足够”的公理本节讨论数据类型公理化方法的一般特征,3.5 代数数据类型,数据抽象的一般原理抽象数据类型由它的规范定义。使用这样数据类型的程序应该只依赖于由它的规范保证的性质，而不依赖于它的任何特定实现一个数据类型的函数可以划分成构造算子：产生该数据类型的一个新元素运算算子：是该数据类型
27、上的函数，但不产生新的元素观察算子：作用于该数据类型的元素，但返回某其它类型的元素，如自然数或布尔值,3.5 代数数据类型,初始代数语义和数据类型归纳代数规范有几种不同的“语义”形式宽松语义：满足一个代数规范的所有代数所构成的代数类初始代数语义：满足一个代数规范的所有初始代数所构成的同构类终结代数语义：满足一个代数规范的所有终结代数所构成的同构类生成语义：满足一个代数规范的所有生成代数所构成的代数类,3.5 代数数据类型,初始代数的性质没有假货没有混淆支持基于数据类型构造符的归纳构造符集合Spec,E的函数符号子集F0，使得Terms(,)E,的每个等价类正好只含一个由F0的函数符号所构成的基
28、项可以基于对构造符的归纳来证明初始代数的性质,3.5 代数数据类型,sorts:set,nat,bool构造符、运算符、观察符fctns:0,1,2,:nat+:nat nat nat Eq?:nat nat nattrue,false bool empty:setinsert:nat set set union:set set setismem?:nat set bool condn: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,.
29、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)condn true x y=x condn false x y=y.,3.5 代数数据类型,终结代数在一个代数类C中，如果从每个BC到AC，都存在唯一的同态，那么代数A是终结代数一个代数类中的所有终结代数都同构若用终结代数作为语义，则称之为终结语义如果所有载体都是单元素集合的代数也在C中，则这个代数一定是C的终结代数,3.5 代数数据类型
30、,初始语义和终结语义初始语义：不能证明为相等的就是不相等的终结语义：不能证明为不相等的则是相等的如果把某些类别的解释固定，而其它类别的解释用终结语义，则它是一个有用的方法从初始语义角度看，前面给出的不是集合的规范,而是表的规范。因为不能证明insert x(insert y z)=insert y(insert x z)x:nat,y:nat,z:setinsert x(insert x z)=insert x zx:nat,z:set若用终结语义，且bool的解释固定,则为集合规范,3.5 代数数据类型,解释没有意义的项表达式没有意义的情况除法是一个部分函数，除数为零的表达式没意义调用不终止
31、的函数也构成一个没有意义的表达式如果想在代数规范中表示这些情况，必须在基调中增加表示错误的项（简称错误值）怎样规定这些项的值？有三种可能：什么也不规定任意做一个决定非常仔细地说明什么是所需要的,3.6 重写系统,基本定义重写系统：用于代数项的归约系统两种重要的应用为代数项提供一种计算模型自动定理证明由一组叫做重写规则(LR)的有向等式组成限制：Var(R)Var(L)由R 确定的一步归约关系RSLxM R SRxM关系 R是R的自反传递闭包,3.6 重写系统,sorts:natfctns:0:nat:nat nat+:nat nat nat在这个基调上的一些归约规则如下：x 0 xx+(x)0
32、(x y)z x+(y+z)实例：(x y)(y)x+(y+(y)x 0 x,3.6 重写系统,引理（归约保类别）令R是上的重写系统.如果M Termss(,)，并且M R N，那么N Termss(,)关系（重写系统）是合流的，如果N M P蕴涵N P的话关系（重写系统）是终止的，如果不存在一步归约的无穷序列M0 M1 M2不能再归约的项称为范式合流并且终止的重写系统通常又叫做典范系统,3.6 重写系统,可变换性 如果存在M M1 M2 M3 Mk N 则项M,N Termss(,)是可变换的，写成M R N箭头的方向并没有什么意义对任何重写系统，可变换性和可证明的相等性是一致的,3.6 重
33、写系统,项中的一个位置：便于引用子项的某个特定出现位置n=1,2的子项是hab用M n表示M在位置n的子项用N n M表示M在n的子项由N代换的结果,3.6 重写系统,合流性和可证明的相等性记号 如果R是一组重写规则，ER用来表示对应的无向的等式集合定理 对任何重写系统R，MR N当且仅当ER M N对任何合流的重写系统R，ER M N当且仅当M R R N,3.6 重写系统,3.6.3 终止性良基关系：集合A上的一个关系是良基的，如果不存在A上元素的无穷递减序列a0 a1 a2 的话。如果能在项和有良基关系的集合A的元素间建立起一个对应，那么可以利用它去证明不存在无穷的归约序列M0 M1 M
34、2 有几种方式可把项映射到有良基关系的集合利用代数的语义结构,3.6 重写系统,代数A=As1,As2,f1A,f2A,是良基的，如果每个载体As上有一个良基关系s对每个n元函数符号f，如果x1 y1,xn yn并且对某个i（1 i n）有xi yi，那么f A(x1,xn)f A(y1,yn)若A是一个良基代数，并且M和N都是类别s上的项，如果M s N，那么写成A，M N如果对任何环境都有A，M N，那么写成A M N。,3.6 重写系统,定理 令R是项上的一个重写系统，并且令A是一个良基的代数。如果对R中每条规则L R有A L R，那么R是终止的例 x x 载体Abool N 0,1(x
35、 y)(x y)A(x,y)=x+y+1(x y)(x y)A(x,y)=x yx(y z)(x y)(x z)A(x)=2x(y z)x(y x)(z x)每条重写规则的左部定义的值都大于其右部定义的值,3.6 重写系统,3.6.4 临界对局部合流关系是局部合流的，如果N M P蕴涵N P 局部合流关系严格弱于合流关系例a b,b aa a0,b b0,3.6 重写系统,cond B(cdr(cons s l)(cons(car l)(cdr l)规则如下：cdr(cons x l)lcons(car l)(cdr l)l不相交的归约,3.6 重写系统,cdr(cons x(cons(car
36、 l)(cdr l)规则如下：cdr(cons x l)lcons(car l)(cdr l)l平凡的重迭,3.6 重写系统,cdr(cons(car l)(cdr l)规则如下：cdr(cons x l)lcons(car l)(cdr l)l非平凡的重迭,3.6 重写系统,临界对L R cdr(cons x l)lL 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,3.6 重写系统,第二个如下：L R cons(c
37、ar l)(cdr l)lL R cdr(cons x l)lSL是cons(car(cons x l)(cdr(cons x l)临界对是cons x l,cons(car(cons x l)l若f(gxy)R，L中有子项f z、f(gPQ)、f(h)。f(h)不可能与f(gxy)合一同一条规则的两次使用可能引起重迭，如f(f x)af(f(f x)左部完全相同的情况：L R和L R,3.6 重写系统,命题 一个重写系统R是局部合流的，当且仅当对每个临界对M,N有M R R N证明从左到右的蕴涵是简单明了的另一个方向的证明仿照用于启发临界对定义的推理：不相交、平凡的重迭、临界对的代换实例如果
38、一个有限的重写系统R是终止的，那么该命题就给出一个算法，可用于判定R是否局部合流,3.6 重写系统,左线性无重迭重写系统无重迭：没有非平凡的临界对无重迭的重写系统不一定是合流的例如：S Eq?x x trueEq?x(S x)falseEq?有两个不同的范式Eq?trueEq?Eq?(S)false,3.6 重写系统,左线性的规则：任何变量在规则的左部的出现不超过一次的话左线性的系统：每一条规则都是左线性的命题 如果R是左线性和无重迭的，那么R是合流的例 下面是一个左线性无重迭重写系统car(cons x l)xcdr(cons x l)lisempty?nil trueisempty?(co
39、ns x l)false 加入非左线性规则cons(car l)(cdr l)l 后不合流isempty?(cons(car l)(cdr l)有两个范式,3.6 重写系统,3.6.6 局部合流、终止和合流之间的联系命题 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的良基归纳 令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真。,3.6 重写系统,3.6.6 局部合流、终止和合流之间的联系命题 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的例if tr
40、ue then x else y xif false then x else y yif u then x else x x,3.6 重写系统,Knuth-Bendix完备化过程一组等式fx f y=f(x+y)(x+y)+z=x+(y+z)构造一个确定同样代数理论的终止且合流的重写系统先定向成一个重写系统 fx f y f(x+y)(x+y)+z x+(y+z),3.6 重写系统,产生一个临界对f(x+y)+z,f x+(f y+z)增加一条重写规则 fx f y f(x+y)(x+y)+z x+(y+z)f(x+y)+z f x+(f y+z)本例增加无数条重写规则f n(x+y)+z f nx+(f n y+z),习 题,第一次：3.3(a)，3.8第二次：3.11，3.14，3.15第三次：3.16(d),(e)，3.19第四次：3.22，3.23第五次：3.32(a)，3.33,
