泛代数和代数数据类型

泛代数和代数数据类型第一页，共八十五页，编辑于2023年，星期日2.1引言代数数据类型包括一个或多个值集一组在这些集合上的函数基本限制是其函数不能有函数变元基本“类型”(type)符号被称为“类别”(sort)泛代数（也叫做等式逻辑）定义和研究代数数据类型的一般数学框架本章研究泛代数和它在程序设计中定义常用数据类型时的作用第二页，共八十五页，编辑于2023年，星期日2.1引言本章主要内容：代数项和它们在多类别代数中的解释等式规范（也叫代数规范）和等式证明系统等式证明系统的可靠性和完备性（公理语义和指称语义的等价）代数之间的同态关系和初始代数数据类型的代数理论从代数规范导出的重写规则（操作语义） 包括了大多数逻辑系统中的一些公共议题第三页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项2.2.1代数代数一个或多个集合，叫做载体一组特征元素和一阶函数，也叫做代数函数

f:A1…

Ak

A例：N

N,0,1,+,

载体N是自然数集合特征元素0,1N，也叫做零元函数函数+,

:N

NN第四页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项多个载体的例子

APCF

N,B,0,1,…,+,true,false,Eq?,…下面逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要，可用来定义数据类型证明数据类型的性质还必须讨论这种语法描述的指称语义

满足一组等式的除了APCF外，可能还有：

A5PCFN5,B,0,1,2,3,4,+5,true,false,Eq?,…第五页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项2.2.2

代数项的语法基调

S，FS是一个集合，其元素叫做类别函数符号f:s1…

sk

s的集合F，其中表达式s1…

sk

s叫做f的类型零元函数符号叫做常量符号例:N

S，F sorts:nat fctns:0,1:nat ,:nat

nat

nat

第六页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项项定义基调的目的是用于写代数项项中可能有变量，因此需假定一个无穷的符号集合V，其元素称为变量类别指派

x1:s1,…,xk:sk基调S，F和类别指派上类别s的代数项集合Termss(,)定义如下：

1、如果x:s，那么xTermss(,)

2、如果f:s1…sk

s并且MiTerms(,)(i1,…,k)，那么fM1…MkTermss(,)

当k0时，如果f:s，那么f

Termss(,)si第七页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项项的例子0,01Termsnat(N,)0xTermsnat(N,)，其中

x:nat,…代数项中无约束变元NxM就是简单地把M中x的每个出现都用N代替记号 ,x:sx:s引理2.1若MTermss(,,x:s)且NTermss(,)，那么NxMTermss(,)证明按Termss(,)中项的结构进行归纳第八页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项例用基调stkS,F来写自然数和自然数栈表达式

sorts:nat,stack fctns:0,1,2,…:nat ,:natnatnat

empty:stack

push:natstackstack

pop:stackstack

top:stacknatpush2(push1(push0empty))是该基调的项第九页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项2.2.3代数以及项在代数中的解释基调的代数是为代数项提供含义的数学结构是一个基调，则代数A包含对每个sS，正好有一个载体As一个解释映射I

把函数I

(f)

:A…A

As指派给函数符号

f:s1…sk

sF

把I

(f)As指派给常量符号f:sFN代数N写成

N

N,

0N,

1N,

N,

N

sks1第十页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项代数A的环境:Vs

As环境满足如果对每个x:s都有(x)AsMTermss(,)的含义AM是

Ax(x)

AMfA

(AM1,…,AMk)若f:s是常量符号，则AffA若A清楚时，省略A而直接写成M不依赖于时，用AM表示M在A中的含义第十一页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项例若(x)

0N

x1N(x,1) N

((x),1N) N

(0N,1N) 1N

第十二页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项例Astk

N,N,0A,1A,…,A,A,emptyA, pushA,pop

A,top

A emptyA

,空序列 pushA(n,s)n::s

popA(n::s)s

popA(

)

topA(n::s)n topA(

)0A若把x:nat映射到自然数3，把s:stack映射到2,1

pop(pushxs)popA(pushA(

x,s)) popA(pushA(3,2,1)) popA(3,2,1) 2,1第十三页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项引理2.2 令A是代数，MTermss(,)，并且是满足的环境，那么MAs证明根据Termss(,)中项的结构进行归纳引理2.3 令x1,…,xk是由出现在MTermss(,)中的所有变量构成的变量表，1和2是满足的两个环境,并且对i1,…,k有1(xi)2(xi),那么M1

M2证明基于项结构的归纳第十四页，共八十五页，编辑于2023年，星期日2.2

代数、基调和项2.2.4代换引理引理2.4 令MTermss(,,x:s)并且NTermss(,)，那么NxMTermss(,)。并且对任何环境，有 NxMM(x

a)， 其中aN，它是N在下的含义证明根据项M的结构进行归纳第十五页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性代数规范一个基调+一组等式调查什么样的代数满足这些等式强加的要求使用等式证明系统可推导的新的等式可靠性：从规范可证明的等式在任何满足该规范的代数中都成立完备性：在满足规范的所有代数中都成立的等式都可从该规范证明代数规范是描述代数数据类型公理语义的工具第十六页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性2.3.1等式公式MN，对某个s，M,NTermss(,)若满足，并且还有MN，则认为代数A在环境下满足MN，写成

A,

MN若A在任何环境下都满足该等式，则写成

A

MN若代数类C中的任何代数A都满足该等式，写成

C

MN若任何一个代数都满足等式MN，则写成

MN (永真的、有效的)第十七页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性平凡的代数若A满足上所有等式，就说代数A是平凡的例令有两个类别a和b，令A是一个代数，其中Aa{0,1}并且Ab

A不可能满足xy[x:a,y:a]，即下式不成立

A

xy[x:a,y:a]但是A

xy[x:a,y:a,z:b]无意义地成立第十八页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性2.3.2

项代数项代数Terms(,)类别s的载体：集合Termss(,)函数符号f:s1…sk

s的解释

I(f)(M1,…,Mk)fM1…Mk项代数Terms(,)的环境也叫做一个代换如果S是代换，则用SM表示同时把M中的各个变量x用Sx替换的结果因此用M表示把代换作用于M的结果第十九页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性例类别u函数符号f:uu和g:uuu{a:u,b:u,c:u}Tua,b,c,fa,fb,fc,gaa,gab,gac,gbb,…, g(f(fa))(f(gbc)),…}若环境把变量x映射到a，把y映射到fb，则

T

g(fx)(fy)g(fa)(f(fb))第二十页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性引理2.5 令MTerms(,)，并且是满足的项代数Terms(,)的环境，那么MM证明对项进行归纳证明从项代数可以知道，只有M和N是语法上相同的项时，等式MN才会永真第二十一页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性2.3.3语义蕴涵和等式证明系统代数规范Spec,E:基调和一组等式E语义蕴涵：E

MN满足E的所有代数A都满足等式MN语义理论E

：如果E

MN蕴涵MNE代数A的理论Th(A)在A中成立的所有等式的集合这是一个语义理论第二十二页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性回顾证明系统的可靠性 若等式E从一组假设E可证，则E语义上蕴涵E证明系统的完备性 若E语义上蕴涵等式E，则E从E可证下一步先给出代数证明系统，然后讨论可靠性和完备性第二十三页，共八十五页，编辑于2023年，星期日1、语义相等是个等价关系，因此有

MM2、在等式中增加类别指派的规则3、等价代换

M=NN=MM=NN=PM=PM=NM=N,x:sM=N,x:sP=QP/xM=Q/xN2.3

等式、可靠性和完备性x不在中P,QTermss(,)第二十四页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性等式可证 若从E中的等式和公理(ref)及推理规则(sym)、(trans)、(subst)和(addvar)可推出等式MN，则说该等式可证，写成

E

MN语法理论

如果E

MN蕴涵MNE

E的语法理论Th(E)

从E可证的所有等式的集合第二十五页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性等式集合E是语义一致的若存在某个等式MN，它不是E的语义蕴涵等式集合E是语法一致的若存在某个等式MN，它不能由E证明第二十六页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性例在基调stkS,F上增加等式

top(pushxs)=x[s:stack,x:nat] pop(pushxs)=s[s:stack,x:nat]使用这些等式可以证明等式

top(push3empty)=3top(pushxs)=x[s:stack,x:nat]empty=empty[x:nat]top(pushxempty)=x[x:nat] 3=3[]

top(push3empty)=3[]第二十七页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性导出规则

f:s1…sks Mi,NiTerms(,)

M和N中没有x,Termss(,)非空M=NN=PP=QM=QM1

=N1

…

Mk

=Nk

fM1

…Mk=fN1

…NkM=N,x:sM=Nsi第二十八页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性定理2.6（可靠性） 如果E

MN

，那么E

MN证明可以根据该证明的长度进行归纳归纳基础：长度为1的证明，它是公理或E的一个等式归纳假设：MN的最后一步是从E1,…,En得到，那么，若A

E，则A满足E1,…,En要证明：若A满足最后一条规则的这些前提，则A满足MN证明根据证明规则的集合，分情况进行分析第二十九页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性命题2.7 存在代数理论E和不含x的项M和N，使得E

M=N,x:s，但是E

M=N证明令基调有类别a和b，函数符号f:ab和c,d:b令E是包含能从

fx=

c[x:a]和

fx=

d[x:a]证明的所有等式显然c=

d[x:a]

E可以找到一个使等式c=d[]不成立的模型

a和b对应的分别是空集和多于2个元素的集合由可靠性，c=

d[]是不可能从E证明的第三十页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性例栈代数规范sorts:nat,stackfctns:0,1,2,…:nat +,:natnatnat

empty:stack

push:natstackstack pop:stackstack

top:stacknateqns: [s:stack;x:nat] 0+0=0,0+1=1,…00=0,01=0,…

top(pushxs)=xpop(pushxs)=s第三十一页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性等式

push(tops)(pops)=s[s:stack]是不可证的任何形式为

topempty=M[]的等式都是不可证的，若M是类别为nat的项，并且不含empty第三十二页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性2.3.4完备性的形式用于不同逻辑系统的三种不同形式的完备性1、最弱的形式 所有的永真公式都是可证的2、演绎完备性 每个语义蕴涵在证明系统中都是可推导的3、最小模型完备性每个语法理论都是某个“最小”模型的语义理论对代数来说，最小模型完备性意味着每个语法理论是某个代数A的Th(A)

“最小模型”是指它的理论包含的等式最少第三十三页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性最小模型完备性不一定成立考虑等式

E

x=y[x:a,y:a,z:b]1、a的载体只含一个元素，则E满足，此时

E1

x=y[x:a,y:a]成立

2、b的载体为空，则E也满足，此时

E2

z=w[z:b,w:b]成立E1和E2都不是E的语义蕴涵不存在代数，其理论正好就是由E的等式推论组成的语法理论第三十四页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性2.3.5同余、商和演绎完备性同余关系：等价关系加上同余性同余性：指函数保可证明的相等性对单类代数A=A,f1A,f2A,… 同余关系是载体A上的等价关系，使得对每个k元函数fA，若aibi(i=1,…,k)，即ai和bi等价，则fA(a1,…,ak)fA(b1,…,bk)对多类代数A=As,

I

同余关系是一簇等价关系s,sAsAs，使得对每个f:s1…sks及变元序列a1,…,ak和b1,…,bk(aisbiAs

),有fA(a1,…,ak)sfA(b1,…,bk)ii第三十五页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性

A模的商的代数A 把A中有关系元素aa压缩成A的一个元素等价类[a] [a]aAs

aa商代数A定义：(A)s是由As的所有等价类构成的集合

AssasaAs}函数fA由A的函数fA确定 对适当载体的a1,…,ak，

fA([a1],…,[ak])=[fA(a1,…,ak)]第三十六页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性上面定义有意义的条件是fA([a1],…,[ak])必须只依赖于[a1],…,[ak]，而不能依赖于所选的代表a1,…,ak例单类别代数N，0，1，上的同余关系“模k等价”这个商代数是众所周知的整数模k的加结构。如果k等于5，那么342第三十七页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性如果是A的一个环境，是一个同余关系，那么A的环境定义如下：

(x)=[(x)]反过来，对于A的环境，对应它的A的环境有多种选择引理2.8 令是代数A上的同余关系，项MTerms(,)并且是满足的环境。那么项M在商代数A和环境下的含义(A)M由下式决定 (A)M=AM第三十八页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性引理2.9 令E是一组等式集合，令Terms(,)是基调上的项集。由E的可证明性确定的关系E,是Terms(,)上的同余关系定理2.10（完备性） 如果E

MN

，那么E

MN完备性定理加上可靠性定理表明语法理论和语义理论相同第三十九页，共八十五页，编辑于2023年，星期日2.3

等式、可靠性和完备性2.3.6非空类别和最小模型性质没有空载体的代数有最小模型完备性类别s非空：集合Termss(,)不是空集对应的载体肯定非空没有空载体时，可以增加推理规则(nonempty)定理2.11 令E是封闭于规则（nonempty）的语法理论，那么存在所有的载体都非空的代数A，使得ETh(A)M=N,x:sM=N第四十页，共八十五页，编辑于2023年，星期日2.4同态和初始性2.4.1同态和同构将同态和同构概念从单类代数推广到多类代数同态是从一个代数到另一个代数的保结构的映射从代数A到B的同态h:AB一簇映射h={hs

|sS}，使得对的每个函数符号f:s1…sks，有

hs(fA(a1,…,ak))=fB(hs

(a1),…,hs

(ak))1k第四十一页，共八十五页，编辑于2023年，星期日2.4同态和初始性例 令N=N,0,1,，是模k的等价关系,则把nN映射到它的等价类[n]是从N到N的一个同态，因为

h(0)=0N=[0]

h(n+m)=h(n)N

h(m)=[n+m]任何代数到它商代数的同态都用这种方式定义第四十二页，共八十五页，编辑于2023年，星期日2.4同态和初始性例 含义函数是从项代数T

=Terms(,)到任意代数A的一个同态h:

T

A。如果是A的一个满足的环境，该同态的定义是

h(M)=AM这是一个同态，因为

h(fM1…Mk)=A

fM1…Mk

=fA(AM1,…,AMk) =fA(h(M1),…,h(Mk))第四十三页，共八十五页，编辑于2023年，星期日2.4同态和初始性引理2.13 令h:AB是任意同态，并且是满足类别指派的任意A环境。那么对任何项MTerms(,)，有

h(AM)=BMh 当M中不含变量时，h(AM)=BM证明基于项的归纳引理2.14 如果h:AB和k:BC都是代数的同态，那么合成kh:AC也是代数的同态，(k

h)s=ks

hs同构 一个双射的同态,写成AB第四十四页，共八十五页，编辑于2023年，星期日2.4同态和初始性2.4.2初始代数

C是一类代数并且AC，若对每个BC，存在唯一的同态h:AB，则A在C中叫做初始代数初始代数是“典型”的初始代数有尽可能少的非空载体初始代数满足尽可能少的闭等式AB3B2B1第四十五页，共八十五页，编辑于2023年，星期日2.4同态和初始性例基调0类别nat，函数符号0:nat和S:natnat令C是所有0代数构成的代数类闭项代数TTerms(0,)是C

的初始代数 它的载体是所有闭项0,S(0),…,Sk(0),… 该代数的函数S把Sk(0)映射到Sk1(0) 该代数的元素少到能解释所有的函数符号 该代数满足项之间尽可能少的等式第四十六页，共八十五页，编辑于2023年，星期日2.4同态和初始性引理2.15 假定h:AB和k:BA都是同态，并且hk=IdB，kh=IdA。那么A和B同构命题2.16若A和B在代数类C中都是初始代数，则A和B同构命题2.17 令E是一组等式，且令A=Terms(,)E,是模可证明的相等性的代数，则A对E来说是初始代数由项代数和商的性质可知，从E可证明的等式在A中都成立还要证明从A到任何满足E的代数有唯一的同态第四十七页，共八十五页，编辑于2023年，星期日2.4同态和初始性例sorts:

natfctns: 0:nat

S:natnat :natnatnat；eqns： [x:nat,y:nat]

x+0=x

x+(Sy)=S(x+y)可以证明如下事实：Sk0+Sl0=Sk+l0对任何闭项M，存在某个自然数k，使得M=Sk0第四十八页，共八十五页，编辑于2023年，星期日2.4同态和初始性例

x+0=x

x+(Sy)=S(x+y)可以证明如下事实：等式Sk0=Sl0是不可证的，除非k=l每个等价类正好包含一个形式为Sk0的项等价类集和形式为Sk0的项集间有一个双射若把闭项集合{0,S0,…,Sk0,…}作为载体，函数S映射Sk0

Sk＋10，映射(Sk0,Sl0)

Sk＋l0，则得一个初始代数这个初始代数和该基调的标准模型（有后继算子和加法的自然数）同构第四十九页，共八十五页，编辑于2023年，星期日2.4同态和初始性初始代数和其他代数的比较1、和有更多元素的代数比较多余的元素不能由项定义（有垃圾）例1：整数代数Z例2： A=Anat,0A,SA,+A Anat=(0N)({1}Z) 0A=0,0

SAi,n=i,n+1 i,n+A

j,m=max(i,j),n+m第五十页，共八十五页，编辑于2023年，星期日2.4同态和初始性初始代数和其他代数的比较2、和有较少元素的代数比较一些不能证明为相等的项在该代数中被等同（有混淆）例：模k的自然数第五十一页，共八十五页，编辑于2023年，星期日2.4同态和初始性初始代数的一个重要特点初始代数可能会满足不能由E证明的额外的等式例：自然数基调例子中，初始代数满足等式

x+y=y+x 因为E

M=Sk0和E

N=Sl0蕴涵

E

M+N=Sk+l0=N+M第五十二页，共八十五页，编辑于2023年，星期日2.4同态和初始性自然数基调例子中，初始代数满足等式

x+y=y+x不满足交换律的代数Anat是所有f:XX的函数的集合（X至少有两个元素）0A是X上的恒等函数，SA是Anat上的恒等映射+A是Anat上的函数合成

A

=Anat0ASA+A满足E+A没有交换性，因为函数合成没有交换性第五十三页，共八十五页，编辑于2023年，星期日2.4同态和初始性基项、基代换、基实例（项、等式）如果MN是Termss(,)的项之间的等式，并且S是一个，基代换，则把SMSN称为MN的基实例命题2.18 令E是一组等式，且A对E来说是初始代数，则对任何等式MN，下面三个条件等价

A满足MN

A满足MN的每一个基实例

MN的每一个基实例都可以从E证明第五十四页，共八十五页，编辑于2023年，星期日2.5代数数据类型2.5.1代数数据类型 本节讨论数据类型公理化方法的一般特征 程序设计中的很多数据类型不存在标准的数学构造，如优先队列和符号表没有单一和标准的计算机实现通常是列出它们的操作并公理化地描述这些操作之间的关系因此是公理化地定义而不是由数学构造来定义困难之处：对于一个数据类型，难以断定是否有了“足够”的公理第五十五页，共八十五页，编辑于2023年，星期日2.5代数数据类型数据抽象的一般原理抽象数据类型由它的规范定义 使用这样数据类型的程序应该只依赖于由它的规范保证的性质，而不依赖于它的任何特定实现一个数据类型的函数可以划分成 构造算子：产生该数据类型的一个新元素

运算算子：是该数据类型上的函数，但不产生新的元素

观察算子：应用于该数据类型的元素，但返回其它类型的元素，如自然数或布尔值第五十六页，共八十五页，编辑于2023年，星期日2.5代数数据类型2.5.2

初始代数语义和数据类型归纳代数规范有几种不同的“语义”形式宽松语义：满足一个代数规范的所有代数所构成的代数类初始代数语义：满足一个代数规范的所有初始代数所构成的同构类终结代数语义：满足一个代数规范的所有终结代数所构成的同构类生成语义：满足一个代数规范的所有生成代数所构成的代数类第五十七页，共八十五页，编辑于2023年，星期日2.5代数数据类型初始代数的性质没有垃圾没有混淆支持基于数据类型构造符的归纳构造符集合Spec,E的函数符号集合的子集F0，使得Terms(,)E,的每个等价类正好只含一个由F0的函数符号所构成的基项可以基于对构造符的归纳来证明初始代数的性质第五十八页，共八十五页，编辑于2023年，星期日2.5代数数据类型sorts: set,nat,bool 构造符、运算符、观察符fctns: 0,1,2,…:nat +:natnatnat

Eq?:natnatbool true,falsebool

empty:set insert:natsetset

union:setsetset ismem?:natsetbool

condn

:boolnatnatnat

...eqns: [x,y:nat,s,s:set,u,v:bool]0+0=0,0+1=1,1+1=2,...

Eq?xx=true

Eq?01

=false,Eq?02

=false,...

ismem?xempty=false

ismem?x(insertys)=ifEq?xythentrueelseismem?xsunionemptys=s union(insertys)s=inserty(unionss)

condn

truexy=x condn

falsexy=y...第五十九页，共八十五页，编辑于2023年，星期日2.5代数数据类型终结代数 在一个代数类C中，如果从其中的每个B到其中某个A，都存在唯一的同态，那么代数A是终结代数一个代数类中的所有终结代数都同构若用终结代数作为语义，则称之为终结语义如果所有载体都是单元素集合的代数也在C中，则这个代数一定是C的终结代数第六十页，共八十五页，编辑于2023年，星期日2.5代数数据类型初始语义和终结语义初始语义：不能证明为相等的就是不相等的终结语义：不能证明为不相等的则是相等的如果把某些类别的解释固定，而其它类别的解释用用终结语义，则它是一个有用的方法从初始语义角度看，前面给出的不是集合的规范,而是表的规范。因为不能证明insert

x(insert

y

z)=inserty(insertxz)[x:nat,y:nat,z:set]insert

x(insert

xz)=insert

xz[x:nat,z:set]若用终结语义，且bool的解释固定,则为集合规范第六十一页，共八十五页，编辑于2023年，星期日2.5代数数据类型2.5.3

解释没有意义的项表达式没有意义的情况除法是一个部分函数，除数为零的表达式没意义调用不终止的函数也构成一个没有意义的表达式如果想在代数规范中表示这些情况，必须在基调中增加表示错误的项（简称错误值）怎样规定这些项的值？有三种可能： 什么也不规定 任意做一个决定 非常仔细地说明什么是所需要的第六十二页，共八十五页，编辑于2023年，星期日2.6重写系统2.6.1

基本定义重写系统：用于代数项的归约系统R两种重要的应用为代数项提供一种计算模型自动定理证明由一组叫做重写规则(LR)的有向等式组成限制：Var(R)Var(L)由R确定的一步归约关系R [SLx]MR[SRxM关系R是R的自反传递闭包第六十三页，共八十五页，编辑于2023年，星期日2.6重写系统sorts:natfctns:0:nat :natnat +:natnatnat在这个基调上的一些归约规则如下：

x0x

x+(x)0 (xy)zx+(y+z)实例：(xy)(y)x+(y+(y))x0x第六十四页，共八十五页，编辑于2023年，星期日2.6重写系统引理2.19（归约保类别） 令R是上的重写系统，若MTermss(,)且MRN，则NTermss(,)如果N

M

P蕴涵N

P，则关系（重写系统）是合流的若不存在一步归约的无穷序列M0M1M2…，则关系（重写系统）是终止的不能再归约的项称为范式合流且终止的重写系统通常又叫做典范系统第六十五页，共八十五页，编辑于2023年，星期日2.6重写系统可变换性

若存在M

M1

M2

M3…Mk

N，则项M,NTermss(,)是可变换的，写成M↔R

N归约的无向版本箭头的方向并没有什么意义对任何重写系统，可变换性以及可证明的相等性（把重写规则看成等式）是一致的第六十六页，共八十五页，编辑于2023年，星期日2.6重写系统用自然数的有穷序列来表示项中的位置位置n

=1,2的子项是hab用Mn表示M在位置n的子项用NnM表示M在n的子项由N代换的结果 便于引用子项的某个特定出现fggxxhababf(gx(hab))(gba)x第六十七页，共八十五页，编辑于2023年，星期日2.6重写系统2.6.2

合流性和可证明的相等性记号 若R是一组重写规则，ER用来表示对应的无向的等式集合定理2.20 1、对任何重写系统R，MRN当且仅当ER

MN；

2、对任何合流的重写系统R，ER

MN当且仅当MR

R

N第六十八页，共八十五页，编辑于2023年，星期日2.6重写系统2.6.3终止性良基关系 集合A上的一个关系是良基的，如果不存在A上元素的无穷递减序列a0

a1

a2

…的话如果能在项和有良基关系的集合A的元素间建立起一个对应，那么可以利用它去证明不存在无穷的归约序列M0M1M2…有几种方式可把项映射到有良基关系的集合

1、利用项的语法特点

2、利用代数的语义结构（下面用这种方式）第六十九页，共八十五页，编辑于2023年，星期日2.6重写系统代数A=As1,As2,…,f1A,f2A,…是良基的，若每个载体As上有一个良基关系s对每个n元函数符号f，如果x1y1,…,xn

yn并且对某个i（1in）有xi

yi，那么

fA(x1,…,xn)

fA(y1,…,yn)若A是良基代数，并且M和N都是类别s上的项，若Ms

N，则写成

A,M

N如果对任何环境都有A,M

N，那么写成AM

N第七十页，共八十五页，编辑于2023年，星期日2.6重写系统定理2.22 令R是项上的一个重写系统，并且令A是一个良基的代数。如果对R中每条规则LR都有A

L

R，那么R是终止的例

xx 载体AboolN0,1

(xy)(xy) A(x,y)=x+y+1 (xy)(xy) A(x,y)=xy

x(yz)(xy)(xz) A(x)=2x (yz)x(yx)(zx)各重写规则的左部定义的值都大于其右部定义的值第七十一页，共八十五页，编辑于2023年，星期日2.6重写系统2.6.4临界对局部合流关系是局部合流的，若NMP蕴涵N

P

局部合流关系严格弱于合流关系例 ab

ba aa0

bb0a0abb0第七十二页，共八十五页，编辑于2023年，星期日2.6重写系统condB(cdr(conssl))

(cons(carl)(cdrl))规则如下：cdr(consxl)

lcons(carl)(cdrl)

l不相交的归约MSLSLMSRSLMSLSRMSRSR第七十三页，共八十五页，编辑于2023年，星期日2.6重写系统cdr(consx(cons(carl)(cdrl)))规则如下：cdr(consxl)

lcons(carl)(cdrl)

l平凡的重迭SLSLSLSRSRSLSLSRSRSR第七十四页，共八十五页，编辑于2023年，星期日2.6重写系统cdr(cons(carl)(cdrl))规则如下：cdr(consxl)

lcons(carl)(cdrl)

l非平凡的重迭SLSLSLSRSR???第七十五页，共八十五页，编辑于2023年，星期日2.6重写系统临界对LR cdr(consxl)

lL

R

cons(carl)(cdrl)

l非平凡重迭是一个三元组SL，SL，m二元组SR，SRmSL叫做临界对该例有两个临界对第一个如下：SL是cdr(cons(carl)(cdrl))临界对是cdrl,cdrl第七十六页，共八十五页，编辑于2023年，星期日2.6重写系统第二个如下：LR c