中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第2章 泛代数和代数数据类型

很容易证明这是一个导出规则。因为Terms(区，「)非空，则存在某个P∈Tems(区，「)，使 得P=P[T]。结合假设M=N[T,x:,用(subs)可以证明[Px]M=[PxN[T]。因为变量x 在M和N中不出现，代换没有影响，因此M=N[T]。 0 本节主要定理如下： 定理2.6（可靠性）如果￡卜E,那么￡卡E。 证明可以根据该证明的长度进行归纳，即根据￡外E的证明长度来证明￡卡E。 归纳基础是长度为1的证明，它是公理或￡的一个等式。不管哪一种情况，很容易看出， 任何满足￡的代数一定满足该等式。 对于归纳步骤，假定证明E的最后一步是从E1,,En得到，并且E1,,En是由更短的 证明得到。从归纳假设可以假定，如果A卡8，那么A满足E,,En。要证明的是，如果A 满足最后一条规则的这些前提，那么A满足E。这就导致根据证明规则的集合，对各种情况 进行分析。下面仅给出对代换规则的证明。 假定AFM=N[C,x:S,并且AFP=Q[C]。必须证明AF[Px]M=[QxN[]。令是 满足r的任意一个环境，必须证明[PxM7=I[Q/xWMn 令a=[P]n=[gn,并且注意x→a满足T,x:s。由代换引理： Px]Mn=M(x→ad) 并且 I[Ox]WMn=WM(x→a) 因为A=M=N[C,x:s,因此 M(x→a)=M(x→a) 从而Px]Mn和[Q/xWMn相等。这就完成了本定理的证明。 ◇ 使用这个定理，通过下面的命题可以说明为什么在等式中掌握变量的情况是重要的。 命题2.7存在一个代数理论￡和不含x的项M和N,使得ErM=W[T,x:s,但是ErM=V [r] 证明令Σ是一个基调，它有类别a和b,函数符号f:a→b和c,d:b。令￡是包含能从 fx=cx:a和fx=d[x:a证明的所有等式，并且考虑等式c=d[x:a。很清楚，从￡的等 式通过传递性可以得到它。但是从下面的语义讨论可以看到，等式c=d[不可证。 考虑一个Σ代数，其对应a的载体是空集，但是c和d分别指称对应b的非空载体上的 两个不同元素。等式fx=c[x:a和∫x=d[x:a在这个模型中为真，因为x没有任何可能 的值。然而，等式c-d[☑在此模型中不成立。因此，由等式证明系统的可靠性，c=d[) 是不可能从￡证明的。 0 可靠性定理不仅表明证明系统是语义正确的，而且可以知道，如果能找出一个代数满足 ￡而不满足某个等式E,即￡从语义上并不蕴涵E,那么从￡不可能证明E。在不知等式E 是否由等式集合￡语义蕴涵时，可以作两种尝试：从￡证明E,或者找出一个满足￡而不满 足E的代数。根据完备性定理，原则上这两者之间总有一个是可能的。但是应该认识到， 在寻找一个证明和寻找一个代数以表明不存在这样的证明这两者之间有一个重要区别。它就 是，存在一种有效的方法，它能枚举所有的证明，因而如果E从￡可证，那么最终会找到 一个证明：但是不存在这样的方法，用它可以找到一个代数以表明不存在这样的证明。 例2.10栈代数规范如表2.1。满足这个规范的一个代数Ak在例2.4己经给出。 表2.1栈代数规范 sorts: nat,stack fetns: 0,1,2,.:nal +,*:nal×nal→nal empty stack 11

11 很容易证明这是一个导出规则。因为 Termss (, )非空，则存在某个 PTermss (, )，使 得 P = P []。结合假设 M = N [, x : s]，用(subst)可以证明[Px]M = [Px]N []。因为变量 x 在 M 和 N 中不出现，代换没有影响，因此 M = N []。 ￾ 本节主要定理如下： 定理 2.6 （可靠性）如果  E，那么  E。 证明 可以根据该证明的长度进行归纳，即根据  E 的证明长度来证明  E。 归纳基础是长度为 1 的证明，它是公理或 的一个等式。不管哪一种情况，很容易看出， 任何满足 的代数一定满足该等式。 对于归纳步骤，假定证明 E 的最后一步是从 E1, …, En 得到，并且 E1, …, En 是由更短的 证明得到。从归纳假设可以假定，如果  ，那么 满足 E1, …, En。要证明的是，如果 满足最后一条规则的这些前提，那么 满足 E。这就导致根据证明规则的集合，对各种情况 进行分析。下面仅给出对代换规则的证明。 假定  M = N [, x : s]，并且  P = Q []。必须证明  [Px]M = [Qx]N []。令是 满足的任意一个环境，必须证明[Px]M = [Qx]N。 令 a = P = Q，并且注意[x  a]满足, x : s。由代换引理： [Px]M = M([x  a]) 并且 [Qx]N = N([x  a]) 因为  M = N [, x : s]，因此 M([x  a]) = N([x  a]) 从而[Px]M和[Qx]N相等。这就完成了本定理的证明。 ￾ 使用这个定理，通过下面的命题可以说明为什么在等式中掌握变量的情况是重要的。 命题2.7 存在一个代数理论 和不含x的项M和N，使得  M=N , x : s，但是  M=N 。 证明 令是一个基调，它有类别 a 和 b，函数符号 f : a  b 和 c, d : b。令是包含能从 f x = c [x : a]和 f x = d [x : a]证明的所有等式，并且考虑等式 c = d [x : a]。很清楚，从 的等 式通过传递性可以得到它。但是从下面的语义讨论可以看到，等式 c = d[]不可证。 考虑一个代数，其对应 a 的载体是空集，但是 c 和 d 分别指称对应 b 的非空载体上的 两个不同元素。等式 f x = c [x : a]和 f x = d [x : a]在这个模型中为真，因为 x 没有任何可能 的值。然而，等式 c = d []在此模型中不成立。因此，由等式证明系统的可靠性，c = d [] 是不可能从证明的。 ￾ 可靠性定理不仅表明证明系统是语义正确的，而且可以知道，如果能找出一个代数满足  而不满足某个等式 E，即 从语义上并不蕴涵 E，那么从 不可能证明 E。在不知等式 E 是否由等式集合 语义蕴涵时，可以作两种尝试：从 证明 E，或者找出一个满足 而不满 足 E 的代数。根据完备性定理，原则上这两者之间总有一个是可能的。但是应该认识到， 在寻找一个证明和寻找一个代数以表明不存在这样的证明这两者之间有一个重要区别。它就 是，存在一种有效的方法，它能枚举所有的证明，因而如果 E 从 可证，那么最终会找到 一个证明；但是不存在这样的方法，用它可以找到一个代数以表明不存在这样的证明。 例 2.10 栈代数规范如表 2.1。满足这个规范的一个代数stk在例 2.4 已经给出。 表 2.1 栈代数规范 sorts : nat, stack fctns : 0, 1, 2, … : nat +,  : nat  nat  nat empty : stack

push:nal×stack→stack pop:sack→stack top:stack-→nal eqns s stack,x nat 0+0=0,0+1=1, 0*0=0,0*1=0, top (push xs)=x pop (push xs)=s 很容易看出，等式 push (top s)(pop s)=s [s stack] 是不可能从这个规范证明的，只要把s映射到空串就可以看出该等式在Ak中不成立。一个 更加复杂的事实是，任何形式为 top empty=M[] 的等式都不可证，假定M是类别为nal的项，并且不含empy(包括M推导出的项也不含 empy)。该事实的证明要点如下： (1)对任何neN,定义代数L,它们和A几乎一样，区别仅是op(e)=n(那么， Ak=4o)。显然，它们都是该规范的代数。 (2)对类别nal任何不含empy的项M,总能找到一个环境n(把s1ack类别的变量映 射到足够长的串)，使得对所有的i和j,AM7=AM7。 (3)对类别nal任何不含empy的项M,令n是使得对所有的n,AnlMn=AkMn的 环境。由于A.IM独立于n,而Atop emptyln依赖于n,因此肯定存在某个n,使得An1op emp例n≠AnIM7。于是top empty=MT]是不可能从栈公理证明的。 0 2.3.4完备性的形式 在研究完备性证明的技术前，首先讨论可以用于不同逻辑系统的三种不同的完备性。 (1)最弱的形式是，仅所有的永真公式可证。对于代数来说，永真公式是（阳）公理 的所有实例。这种完备性太弱，以至没有什么意义。 (2)处于中间的形式叫做演绎完备性(deductive completeness),它是指每个语义蕴涵 都可证。对代数而言，这是指每当E卡M=TT口，就有ErM=N[T]。 (3)更强形式的完备性叫做最小模型完备性(least model completeness),它是指对每 个语法理论，都有某个“最小”模型，其语义理论等于该语法理论。对代数来说，最小模型 完备性意味着对每个语法理论，都存在某个代数A,T(A)等于该语法理论。可能会引起混 淆的地方是，“最小模型”是指它的理论包含的内容最少，而不是指它们载体的规模最小。 通常，当逻辑公式可以表示“分离”的信息时，最小模型完备性不成立。空载体引入了 一种形式的分离。 考虑等式 E≌x=y[x:a,y:a,z:b] 只有两种模型可使E满足。一种模型是α的载体为空或只含一个元素，只含一个元素 的目的是迫使x和y只能取同样的值。在这种模型中，E兰x=y[x:a,y:d成立。另一种模 型是b的载体为空，它使得E无意义地成立。在这种模型中，E2兰z=m::b,w:b]成立。 显然，E1和E2都不是从E可证的，所以不存在一个代数，其理论正好就是由E的等式推论 组成的语法理论，这就意味着最小模型不存在。 12

12 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 很容易看出，等式 push (top s) (pop s) = s [s : stack] 是不可能从这个规范证明的，只要把 s 映射到空串就可以看出该等式在stk中不成立。一个 更加复杂的事实是，任何形式为 top empty = M [] 的等式都不可证，假定 M 是类别为 nat 的项，并且不含 empty（包括 M 推导出的项也不含 empty）。该事实的证明要点如下： （1）对任何 n，定义代数n，它们和stk几乎一样，区别仅是 An top () = n（那么， stk = 0）。显然，它们都是该规范的代数。 （2）对类别 nat 任何不含 empty 的项 M，总能找到一个环境（把 stack 类别的变量映 射到足够长的串），使得对所有的 i 和 j，iM = jM。 （3）对类别 nat 任何不含 empty 的项 M，令是使得对所有的 n，nM = stkM的 环境。由于nM独立于 n，而ntop empty依赖于 n，因此肯定存在某个 n，使得ntop empty  nM。于是 top empty = M[]是不可能从栈公理证明的。 ￾ 2.3.4 完备性的形式 在研究完备性证明的技术前，首先讨论可以用于不同逻辑系统的三种不同的完备性。 （1）最弱的形式是，仅所有的永真公式可证。对于代数来说，永真公式是（ref）公理 的所有实例。这种完备性太弱，以至没有什么意义。 （2）处于中间的形式叫做演绎完备性（deductive completeness），它是指每个语义蕴涵 都可证。对代数而言，这是指每当 M  N，就有  M  N 。 （3）更强形式的完备性叫做最小模型完备性（least model completeness），它是指对每 个语法理论，都有某个“最小”模型，其语义理论等于该语法理论。对代数来说，最小模型 完备性意味着对每个语法理论，都存在某个代数，Th()等于该语法理论。可能会引起混 淆的地方是，“最小模型”是指它的理论包含的内容最少，而不是指它们载体的规模最小。 通常，当逻辑公式可以表示“分离”的信息时，最小模型完备性不成立。空载体引入了 一种形式的分离。 考虑等式 E  x = y [ x : a, y : a, z : b ] 只有两种模型可使 E 满足。一种模型是 a 的载体为空或只含一个元素，只含一个元素 的目的是迫使 x 和 y 只能取同样的值。在这种模型中，E1  x = y [x : a, y : a]成立。另一种模 型是 b 的载体为空，它使得 E 无意义地成立。在这种模型中，E2  z = w [z : b, w : b]成立。 显然，E1 和 E2 都不是从 E 可证的，所以不存在一个代数，其理论正好就是由 E 的等式推论 组成的语法理论，这就意味着最小模型不存在

2.3.5同余、商和演绎完备性 本节主要结论是可以有空载体的多类代数的演绎完备性定理。该定理的证明要用到同余 关系和商代数，因此首先研究它们。另外，由于本书主要讨论演绎完备性，因此下面简称完 备性。 同余关系是指等价关系加上同余性，而同余性则是指函数保可证的相等性。 对于一个单类代数A=4,4,,),同余关系是载体A上的一个等价关系，使得对每 个k元函数f,如果arb=l,,),即a和b,等价，那么f(a,,ak)）~八(b1,,bk)。 对于多类Σ代数A=({4,工)，同余关系是一簇等价关系~={，~s二4x4,每个类别 一个，使得对每个f:s1××5张→s及变元序列a,,a和b1,,bs(其中a~,b,∈A), 有f(a,,ak)~sf八(b1,,bk)。 给定A上的任意同余关系、，可以构造叫做A模~的商的代数AW~。A~直观的含义是把A 中有关系的元素a~a'压缩成AW的一个元素。 aeA的等价类[a定义为 [a={a'∈|a~a} 等价类的另一种记号是al~。 Σ商代数W~定义如下： (1)(4W~)是由A的所有等价类构成的集合 A-,={[a.|a∈A (2)函数由A的函数f确定。对适当载体的a1,,ak, f([a],...,[a)=[fa (a1...,a)] 这个定义是否有意义并不完全明显。有意义的条件是f心(a],,[a)必须只依赖于[a],, [a,而不能依赖于所选的代表a,,ak。这个问题作为习题。 例如，对于单类别代数W,0,1,+)上的同余关系“模k等价”，很容易看出，这个商 代数是大家熟悉的整数模k加结构。如果k等于5，那么[3]+[4]=[2]。 项M在商代数W~中的含义取决于M在A中的含义。若M不含变量，则M在商代数W~ 中的含义是M在A中的含义所在的等价类。若M含变量，则含义当然还和环境有关。 如果是A的一个环境，~是一个同余关系，那么W~的环境定义如下： (x)=[7x)1 反过来，对于A/~的环境，对应它的A的环境有多种选择。对于变量x,任意选择n(x)∈刀 (x),那么？=川。使用A和4W~的这种对应，描述商代数中项的含义的引理如下： 引理2.8令~是Σ代数A上的一个同余关系，项Me Termst(∑，「)并且n是一个满足T的环境。 那么项M在商代数W和环境n下的含义(AW~)M由 (A/-)[M=[AIMn 给出。 证明基于M的结构进行归纳。归纳基础很容易从？的定义得出。对于归纳步骤，有 (A/-)f M..Miln=f((A-)Miln,..(A-)Mn) =fW(AM小l,,[A[MAl)) =[f (A[Mi]n,...A[Mn)] [AIf M,...,M 0 证明完备性定理前的最后一步是：任何一组等式确定项代数上的一个同余关系。先定义 3

13 2.3.5 同余、商和演绎完备性 本节主要结论是可以有空载体的多类代数的演绎完备性定理。该定理的证明要用到同余 关系和商代数，因此首先研究它们。另外，由于本书主要讨论演绎完备性，因此下面简称完 备性。 同余关系是指等价关系加上同余性，而同余性则是指函数保可证的相等性。 对于一个单类代数= A, f1 , f2 ,…，同余关系是载体 A 上的一个等价关系，使得对每 个 k 元函数 f ，如果 aibi (i =1,…, k)，即 ai 和 bi 等价，那么 f  (a1, …, ak )  f (b1, …, bk )。 对于多类代数 = As ,  ，同余关系是一簇等价关系  s, s  As As ，每个类别 一个，使得对每个 f : s1  …  sk  s 及变元序列 a1, …, ak和 b1, …, bk（其中 ai i ~ s bi  i s A ）， 有 f  (a1, …, ak ) s f (b1, …, bk )。 给定上的任意同余关系，可以构造叫做模的商的代数。直观的含义是把 中有关系的元素 a  a 压缩成的一个元素。 a  As 的等价类[a]定义为 [a]  a  As  a  a  等价类的另一种记号是 a。 商代数定义如下： （1）() s 是由 As 的所有等价类构成的集合 As s  [ ] s a   a  As } （2）函数 f 由 的函数 f 确定。对适当载体的 a1,…, ak， f  ([a1], …, [ak]) = [f  (a1, …, ak)] 这个定义是否有意义并不完全明显。有意义的条件是 f  ([a1], …, [ak])必须只依赖于[a1], …, [ak]，而不能依赖于所选的代表 a1, …, ak。这个问题作为习题。 例如，对于单类别代数，0，1，上的同余关系“模 k 等价”，很容易看出，这个商 代数是大家熟悉的整数模 k 加结构。如果 k 等于 5，那么3  4  2。 项 M 在商代数中的含义取决于 M 在中的含义。若 M 不含变量，则 M 在商代数 中的含义是 M 在 中的含义所在的等价类。若 M 含变量，则含义当然还和环境有关。 如果是的一个环境，是一个同余关系，那么的环境 定义如下：  (x) = [(x)] 反过来，对于的环境，对应它的 的环境有多种选择。对于变量 x，任意选择 (x)  (x)，那么=。使用 和的这种对应，描述商代数中项的含义的引理如下： 引理 2.8 令是代数上的一个同余关系，项 MTerms(, )并且是一个满足的环境。 那么项 M 在商代数 和环境下的含义()M由 ()M = M 给出。 证明 基于 M 的结构进行归纳。归纳基础很容易从 的定义得出。对于归纳步骤，有 ()f M1 … Mk = f  (()M1, …, ()Mk) = f  ([M1], …, [Mk]) = [f  (M1, …, Mk)] = [f M1, …, Mk] ￾ 证明完备性定理前的最后一步是：任何一组等式确定项代数上的一个同余关系。先定义

项集Terms(Σ，「)上一个关系如下： MsrN当且仅当E上M=N[] 引理2.9令￡是一组Σ等式集合，令Trms(Σ，「)是基调Σ上的项集。由￡的可证明性确 定的关系~gr是Trms(②，「)上的一个同余关系。 证明很容易看出，在各个类别上，~sr是一个等价关系，因为有公理()以及推理规则 (sm)和(trans)。为了简化记号，用T表示项代数Tems(Σ，「)。很容易从导出规则(cong)得出， 如果M~8rN:(1≤i≤)，那么 f(M,...M)rf(N1,...,N) ◇ 定理2.10（完备性）令￡是一个Σ等式的集合，并且E是一个等式。如果￡卡E,那么 EHE。 证明用反证法。假定等式M6-N[口]不能从￡证明，若能找到一个代数满足￡，但是不 满足该等式，则完备性得证。所找的代数就是商代数A=ms(②，「o~,。,因而要证明A 满足￡的所有等式，但不满足Mo=No[To]。 为简单起见，用~和T分别表示~，，和项代数Trms(②，「o)。 要想证明A不满足M=Wo[「o],只要能找到一个环境使得M和No在该环境下的解释不 相同就可以了。令n是T的一个环境，它把变量都映射到自己。由引理2.5，TM就是M6。 由引理2.8 A[Moln=[Mo] 对No也一样。由假设知道[M6]≠[No],因此在环境n中，M=NoTo不成立。 剩下要证明A卡￡。假定M=N[T]∈E。由引理2.8知道，对项代数T的一个环境，A的 环境可以写成n。具体来说，假设给定A的某个环境介，那么对每个变量x,选择某个P∈(x) 并且让x)=P,这样就有n=介。因此，只要证明对每个满足「的T的环境n,AMn=An 就可以了。 对满足「的任何T的环境n,由引理2.8，AMn=[T[M。再由引理2.5得 A[Mn=[T[Mn.=[nM. 同样，ANn.=[nN。使用规则(e0和subs),可以证明E卜仁W[T](见习题2.14)。它 意味着[M=[WM,从而M和N在A中有同样的含义。这就证明了定理。 0 完备性定理加上先前的可靠性定理表明，语法理论和语义理论是相同的。 2.3.6非空类别和最小模型完备性 先精确定义什么是非空类别。一个类别s是Σ非空的，如果基调Σ包含类别s的一个常量 符号，或者有函数符号f:1××Sk→s并且类别s1,,Sk都是非空的。 如果s是∑非空的，那么至少有一个项ME Terms(Σ，☑)，从而在任何Σ代数中s的载体不 可能为空，因为至少能命名s的一个元素PeTerms(E,「)，并且P肯定能解释为s载体上的 一个元素。 没有空载体的代数有最小模型完备性。删除空载体有两种办法： (1)假定没有代数有任何空载体，并加上一个删除多余变量的推理规则到2.3.3节的证 明系统。这种方式是将讨论范围限制到没有任何空载体的代数，而不管基调中是否有空类别。 (2)基调中每个类别都有不含变量的项。这种方式由所有类别都非空来要求所有载体 都非空。 在这两种情况下，在证明定理2.10时用的构造本质上同样可以用于证明最小模型完备 性。 g

14 项集 Terms(, )上一个关系如下： M,  N 当且仅当   M = N [] 引理 2.9 令 是一组等式集合，令 Terms(, )是基调上的项集。由 的可证明性确 定的关系, 是 Terms(, )上的一个同余关系。 证明 很容易看出，在各个类别上，, 是一个等价关系，因为有公理(ref)以及推理规则 (sym)和(trans)。为了简化记号，用 表示项代数 Terms(, )。很容易从导出规则(cong)得出， 如果 Mi ,  Ni (1 i  k) ，那么 f  (M1, …, Mk) ,  f  (N1, …, Nk) ￾ 定理 2.10 （完备性）令 是一个等式的集合，并且 E 是一个等式。如果E，那么  E。 证明 用反证法。假定等式 M0= N0 [0]不能从 证明，若能找到一个代数满足，但是不 满足该等式，则完备性得证。所找的代数就是商代数 =Terms(, 0) 0 ~ ,  ，因而要证明 满足 的所有等式，但不满足 M 0= N 0 [0]。 为简单起见，用和 分别表示 0 ~ ,  和项代数 Terms(, 0)。 要想证明不满足 M0=N0 [0]，只要能找到一个环境使得 M0 和 N0 在该环境下的解释不 相同就可以了。令是 的一个环境，它把变量都映射到自己。由引理 2.5， M0就是 M0。 由引理 2.8 M0 = [M 0] 对 N0 也一样。由假设知道[M0]  [N0]，因此在环境中，M0= N0 [0]不成立。 剩下要证明 。假定 M = N []。由引理 2.8 知道，对项代数 的一个环境， 的 环境可以写成。具体来说，假设给定 的某个环境ˆ ，那么对每个变量 x，选择某个 P ˆ (x) 并且让(x)P，这样就有 ˆ 。因此，只要证明对每个满足的 的环境，M = N 就可以了。 对满足的任何 的环境，由引理 2.8，M = [ M]。再由引理 2.5 得 M = [ M] = [M] 同样，N = [N]。使用规则(ref)和(subst)，可以证明  M=N []（见习题 2.14）。它 意味着[M] = [N]，从而 M 和 N 在中有同样的含义。这就证明了定理。 ￾ 完备性定理加上先前的可靠性定理表明，语法理论和语义理论是相同的。 2.3.6 非空类别和最小模型完备性 先精确定义什么是非空类别。一个类别 s 是非空的，如果基调包含类别 s 的一个常量 符号，或者有函数符号 f : s1  …  sk  s 并且类别 s1, …, sk都是非空的。 如果 s 是非空的，那么至少有一个项 MTermss (, )，从而在任何代数中 s 的载体不 可能为空，因为至少能命名 s 的一个元素 PTermss (, )，并且 P 肯定能解释为 s 载体上的 一个元素。 没有空载体的代数有最小模型完备性。删除空载体有两种办法： （1）假定没有代数有任何空载体，并加上一个删除多余变量的推理规则到 2.3.3 节的证 明系统。这种方式是将讨论范围限制到没有任何空载体的代数，而不管基调中是否有空类别。 （2）基调中每个类别都有不含变量的项。这种方式由所有类别都非空来要求所有载体 都非空。 在这两种情况下，在证明定理 2.10 时用的构造本质上同样可以用于证明最小模型完备 性

覆盖这两种非空情况的一个完备性定理的陈述要用到下面的推理规则： M=NT,x:s] x不在M和N中 (nonempty) M=NI] 该规则允许将等式中不出现的变量的类别指派在环境中删除。如果知道s的载体非空，那么 很容易看出该规则可靠。具体说，如果作为前提的等式在某个代数A中得到满足，并且是 满足「，x:s的一个环境，那么存在满足「的一个环境川，对于T中的所有变量，和是一样 的。由引理2.3，项M和N在川下有同样的含义，就像在n下那样，所以该规则可靠。 下面的定理是通过该规则来给出最小模型完备性。 定理2.11令e是封闭于规则(nonempty)的语法理论，那么存在所有载体都非空的代数 A,使得E=Th(A) 这里封闭于规则(nonempty)是指，任何能用规则(nonempty)推出的等式都在￡中。 证明假定￡是封闭于规则(nonempty)的语法理论。为了避免有关变量名字的技术细节， 假定有形式为x:s的序对的无穷集合「，并且Σ的每个类别都有无穷多个变量。假定所关心 的项都属于某个Tems(Σ，「)，「c「。这并不失一般性，因为「有足够多的变量，重新命名 一个变量不会影响一个代数是否满足一个等式。很容易看出，项代数Tms(Σ，「)的定义不依 赖于T是否有限，因而可以令T是项代数ms(E,「)。令~是T上的一个二元关系，使得对 某个有穷的r∈「，MN当且仅当E上M=N[T]。很容易检查，~是T上的一个同余关系。 剩下要证明的是，对商代数A=T/人有￡=Th(A)。证明的步骤本质上同于定理2.10的证明 步骤。 在所有类别都非空（从而所有载体也都非空）的情况下，可以用这个定理来证明2.3.3 节没有规则(nonempt')的证明系统的最小模型完备性。因为当所有的类别都非空时，可以像 例2.9中描述的那样，由代换规则删除等式中多余变量，因此(nonempty)成为一个导出规则。 推论2.12如果Σ是每个类别都Σ非空的基调，那么对Σ每个语法理论￡，存在一个代数A, 使得E=Th(A)。 2.4同态和初始性 2.4.1同态和同构 同态是从一个代数到另一个代数的保结构的映射，本节将同态和同构的概念从单类代数 推广到多类代数，并用同态来定义初始代数。 对多类代数来说，从Σ代数A到B的同态h:A→B是一簇映射h={h|s∈S},使得 对Σ的每个函数符号f:S1×..×k→s,有 h'(f(aa)=f (h"a..h"a) 直观上，同态看成是从A的值到B的值的“翻译”。 例2.11令W=W0,1,+),令~是模k的等价关系。那么把ne映射到它的等价类[n 是从N到的一个同态，因为 h(0)=0w4=[01. h(n+m)=h(n)h(m)=[n+ml 通常，任何代数到它商代数的同态都用这种方式定义。 0 例2.12含义函数是从项代数T=Tems(Σ，「)到任意代数A的一个同态h:T→A。如果 是A的一个满足「的环境，该同态的定义是 小

15 覆盖这两种非空情况的一个完备性定理的陈述要用到下面的推理规则： [ , : ] [ ] M N xs M N     x 不在 M 和 N 中 (nonempty) 该规则允许将等式中不出现的变量的类别指派在环境中删除。如果知道 s 的载体非空，那么 很容易看出该规则可靠。具体说，如果作为前提的等式在某个代数 中得到满足，并且是 满足, x : s 的一个环境，那么存在满足的一个环境，对于中的所有变量，和是一样 的。由引理 2.3，项 M 和 N 在下有同样的含义，就像在下那样，所以该规则可靠。 下面的定理是通过该规则来给出最小模型完备性。 定理 2.11 令 是封闭于规则(nonempty)的语法理论，那么存在所有载体都非空的代数 ，使得  Th ()。 这里封闭于规则(nonempty)是指，任何能用规则(nonempty)推出的等式都在 中。 证明 假定 是封闭于规则(nonempty)的语法理论。为了避免有关变量名字的技术细节， 假定有形式为 x : s 的序对的无穷集合，并且的每个类别都有无穷多个变量。假定所关心 的项都属于某个 Terms(, )，  。这并不失一般性，因为有足够多的变量，重新命名 一个变量不会影响一个代数是否满足一个等式。很容易看出，项代数 Terms(, )的定义不依 赖于是否有限，因而可以令是项代数 Terms(, )。令是 上的一个二元关系，使得对 某个有穷的  ，MN 当且仅当  M = N []。很容易检查，是 上的一个同余关系。 剩下要证明的是，对商代数 =  有  Th ( )。证明的步骤本质上同于定理 2.10 的证明 步骤。 ￾ 在所有类别都非空（从而所有载体也都非空）的情况下，可以用这个定理来证明 2.3.3 节没有规则(nonempty)的证明系统的最小模型完备性。因为当所有的类别都非空时，可以像 例 2.9 中描述的那样，由代换规则删除等式中多余变量，因此(nonempty)成为一个导出规则。 推论 2.12 如果是每个类别都非空的基调，那么对每个语法理论，存在一个代数， 使得  Th ()。 2.4 同态和初始性 2.4.1 同态和同构 同态是从一个代数到另一个代数的保结构的映射，本节将同态和同构的概念从单类代数 推广到多类代数，并用同态来定义初始代数。 对多类代数来说，从代数 到 的同态 h :    是一簇映射 h = {hs | s  S }，使得 对的每个函数符号 f : s1  …  sk  s，有 ( ( , ..., )) ( , ..., ) 1 1 1 k B s s k s A h f a a f h a h ak  直观上，同态看成是从 的值到 的值的“翻译”。 例 2.11 令 = , 0, 1, ，令是模 k 的等价关系。那么把 n映射到它的等价类[n] 是从 到的一个同态，因为 h (0) = 0  = [0] h (n + m) = h (n)   h (m) = [n + m] 通常，任何代数到它商代数的同态都用这种方式定义。 ￾ 例 2.12 含义函数是从项代数 = Terms(, )到任意代数 的一个同态 h :   。如果 是 的一个满足的环境，该同态的定义是