第3章泛代数代数数据类型

1、第第3章章 泛代数和代数数据类型泛代数和代数数据类型 pcf语言的三部分组成语言的三部分组成带函数和积类型的纯类型化带函数和积类型的纯类型化 演算演算自然数类型和布尔类型自然数类型和布尔类型不动点算子不动点算子 第第3章到第章到第5章对章对这三这三部分进行透彻的研究部分进行透彻的研究 本章研究像自然数类型和布尔类型这样的代数本章研究像自然数类型和布尔类型这样的代数数据类型数据类型3.1 引引 言言代数数据类型代数数据类型包括包括 一个或多个值集一个或多个值集 一组在这些集合上的函数一组在这些集合上的函数 基本限制是其函数不能有函数变元基本限制是其函数不能有函数变元 基本基本“类型类型”符号符号

2、被称为被称为“类别类别”泛代数（也叫做等式逻辑）泛代数（也叫做等式逻辑） 定义和研究代数数据类型的一般数学框架定义和研究代数数据类型的一般数学框架 本章研究泛代数和它在程序设计中定义常用数本章研究泛代数和它在程序设计中定义常用数据类型时的作用据类型时的作用 3.1 引引 言言本章主要内容：本章主要内容： 代数项和它们在多类别代数中的解释代数项和它们在多类别代数中的解释 等式规范（也叫代数规范）和等式证明系统等式规范（也叫代数规范）和等式证明系统 等式证明系统的可靠性和完备性（公理语义和等式证明系统的可靠性和完备性（公理语义和指称语义的等价）指称语义的等价） 代数之间的同态关系和初始代数代数之间

3、的同态关系和初始代数 数据类型的代数理论数据类型的代数理论 从代数规范导出的重写规则（操作语义）从代数规范导出的重写规则（操作语义）大多数逻辑系统中一些公共的议题将被覆盖大多数逻辑系统中一些公共的议题将被覆盖3.2 代数、基调和项代数、基调和项3.2.1 代数代数 代数代数一个或多个集合一个或多个集合，叫做叫做载体载体一组特征元素和一组特征元素和一阶函数，也一阶函数，也叫做叫做代数函数代数函数f : a1 ak a 例例：n n, 0, 1, +, 载体载体n是自然数集合是自然数集合特征元素特征元素0, 1 n，也，也叫做零元函数叫做零元函数函数函数+, : n n n3.2 代数、基调和项代

4、数、基调和项 多个载体的例子多个载体的例子 apcf n, b, 0, 1, , +, true, false, eq ?, 下面开始逐步给出代数的一种语法描述，有穷下面开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要的语法表示在计算机科学中十分重要 定义数据类型定义数据类型 证明性质证明性质 进行化简进行化简 还必须讨论这种语法描述的语义还必须讨论这种语法描述的语义 a5pcf n5, b, 0, 1, 2, 3, 4, +5, true, false, eq ?, 3.2 代数、基调和项代数、基调和项3.2.2 代数项的语法代数项的语法 基调基调 s，f s是一个集合，

5、其元素叫做是一个集合，其元素叫做类别类别 函数符号函数符号f : s1 sk s的的集合集合f ，其中，其中表达式表达式s1 sk s叫做类型叫做类型 零元函数符号叫做常量符号零元函数符号叫做常量符号 例例 n s，f sorts : nat fctns : 0, 1 : nat , : nat nat nat 3.2 代数、基调和项代数、基调和项 定义基调的目的是用于写代数项定义基调的目的是用于写代数项 考虑项中有变量的情况，需假定有一个无穷的考虑项中有变量的情况，需假定有一个无穷的符号符号集合集合v，其元素称为其元素称为变量变量 类别指派类别指派 x1 : s1, , xk : sk 基调

6、基调 s，f 和类别指派和类别指派 上类别上类别s的代数项的代数项集合集合termss ( , )如果如果x : s ，那么，那么x termss ( , )如果如果f : s1 sk s并且并且mi termssi( , ) (i 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, 代数项中无约束变元，代数项中无约束变元， n x m就是简单地把

7、就是简单地把m中中x的每个出现都用的每个出现都用n代替就是了代替就是了 记号记号 , x : s x : s 引理引理 如果如果m termss ( , , x : s )并且并且n termss ( , )，那么，那么 n x m termss ( , )证明证明 按按termss( , )中项的结构进行归纳中项的结构进行归纳3.2 代数、基调和项代数、基调和项 例例 用基调用基调 stk s, f 来写自然数和栈表达式来写自然数和栈表达式sorts : nat, stackfctns : 0, 1, 2, : nat , : nat nat natempty : stackpush : n

8、at stack stackpop : stack stacktop : stack nat push 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 )

9、as指派给常量符号指派给常量符号f : s f n代数代数n写成写成n n, 0n, 1n, n, n 3.2 代数、基调和项代数、基调和项 代数代数a的环境的环境 : v s as 环境环境 满足满足 如果对每个如果对每个x : s 都有都有 (x) as m termss ( , )的含义的含义am ax (x) am f a (am1 , , amk ) 若若f : s是常量符号，则是常量符号，则af f a a清楚时，省略清楚时，省略a而直接写成而直接写成m 不依赖于不依赖于 时，时，用用am表示表示m在在a中的含义中的含义3.2 代数、基调和项代数、基调和项 例例 若若 (x) 0n

10、 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) popa(pusha( x ,s ) ) popa(pusha(3a, 2

11、a, 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), 那么那么m 1 m 2证明证明 基于项结构的归

12、纳基于项结构的归纳3.2 代数、基调和项代数、基调和项3.2.4 代换引理代换引理引理引理 令令m termss ( , , x : s )并且并且 n termss ( , )，那么，那么 n x m termss( , )。并。并且对任何环境且对任何环境 ，有，有 n x m m( x a )，其中其中a n 是是n在在 下的含义下的含义证明证明 根据项根据项m的结构进行归纳的结构进行归纳3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.1 等式等式代数规范：一个代数规范：一个基调基调 + + 一组等式一组等式 调查什么样的代数满足这些等式强加的要求调查什么样的代数满足这些等式强加的

13、要求 使用等式证明系统可推导新的等式使用等式证明系统可推导新的等式可靠性：可靠性：从规范可证明的等式在任何满足该规范从规范可证明的等式在任何满足该规范的代数中都成立的代数中都成立完备性：完备性：在满足规范的所有代数中都成立的等式在满足规范的所有代数中都成立的等式都可从该规范证明都可从该规范证明代数规范是描述代数规范是描述代数数据类型公理语义的工具代数数据类型公理语义的工具3.3 等式、可靠性和完备性等式、可靠性和完备性空载体提出一个技术问题空载体提出一个技术问题逻辑公式逻辑公式若若a = ，则公式，则公式 x:a. f(x) 为真为真若若a = ，则公式，则公式 x:a. f(x) 为假为假对

14、任意的对任意的m, n termss ( , )，如果，如果x : s 且且as 为空，那么为空，那么m和和n看成是相等的项看成是相等的项只有一个类别时，假定该类别非空是有意义只有一个类别时，假定该类别非空是有意义的的3.3 等式、可靠性和完备性等式、可靠性和完备性等式等式公式公式m n 对某个对某个s，m, n termss ( , ) 如果如果 满足满足 ，那么若，那么若m n ，就说代，就说代数数a在环境在环境 下满足下满足m n，写成，写成a, m n若若a在任何环境下都满足，写成在任何环境下都满足，写成 a m n 如果一类代数如果一类代数c中的任何一个代数中的任何一个代数a都满足，

15、写成都满足，写成 c m n 任何一个任何一个 代数都满足等式代数都满足等式m n，写成，写成 m n(永真的、有效的永真的、有效的 )3.3 等式、可靠性和完备性等式、可靠性和完备性 如果如果a满足满足 上的所有等式，就说上的所有等式，就说 代数代数a是平凡是平凡的的例例令令 有两个类别有两个类别a和和b，令，令a是一个是一个 代数，其代数，其中中aa 0,1并且并且ab。a不可能满足不可能满足x yx : a, y : a，即下式，即下式不成立不成立 a x yx : a, y : a但是但是a x yx : a, y : a, z : b无意义地无意义地成立成立 3.3 等式、可靠性和完

16、备性等式、可靠性和完备性3.3.2 项代数项代数项代数项代数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

17、 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 等式、可靠性和完备性等式、可靠性和完备性引理引理 令令m terms( , )，并且，并且 是满足是满足 的项的项代数代数terms( , )的环境，那么的环境，那么m m证明证明 对项进行归纳证明对项进行归纳证明从从项代数可以知道，项代数可以知道，只有只

18、有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是可证

19、明的，那么是可证明的，那么e语义上蕴涵该等式语义上蕴涵该等式证明系统的完备性：如果证明系统的完备性：如果e语义上蕴涵一个等语义上蕴涵一个等式，那么该等式可从式，那么该等式可从e证明证明下面先给出代数证明系统下面先给出代数证明系统3.3 等式、可靠性和完备性等式、可靠性和完备性语义相等是个等价关系语义相等是个等价关系，因此有，因此有m m在等式中增加类别指派在等式中增加类别指派的规则的规则等价代换等价代换p , q termss( , ) 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

20、 = p/x n 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

21、，它不是它不是e的语义蕴的语义蕴涵涵等式集合等式集合e是是语法一致的语法一致的 如果存在某个等式如果存在某个等式m n，它不能由，它不能由e证明证明 3.3 等式、可靠性和完备性等式、可靠性和完备性例例 在基调在基调 stk s, f 上增加等式上增加等式top (push x s ) = xs : stack, x : natpop (push x s ) = ss : stack, x : nat使用这些等式可以证明等式使用这些等式可以证明等式top (push 3 empty ) = 3top(push x s ) = xs : stack, x : nat, empty = empty

22、 x : nat top(push x empty ) = xx : nat3 = 3 top(push 3 empty ) = 3 3.3 等式、可靠性和完备性等式、可靠性和完备性导出规则导出规则 f : s1 sk s mi, ni termssi( , ) m和和n中没有中没有x，termss( , )非空非空m = n , n = p , p = q m = q m1 = n1 , , mk = nk f m1 mk = f n1 nk m = n , x : s m = n 3.3 等式、可靠性和完备性等式、可靠性和完备性定理定理（可靠性可靠性）如果）如果e m n ， 那么那么e

23、m n证明证明 可以根据该证明的长度进行归纳可以根据该证明的长度进行归纳 归纳基础：长度为归纳基础：长度为1的证明，它是公理或的证明，它是公理或e的一个的一个等式等式 归纳假设归纳假设： m n的最后一步的最后一步是从是从e1, , en得得到到。那么，。那么，如果如果a e，则，则a满足满足e1, , en 要证明：如果要证明：如果a满足最后一条规则的这些前提，满足最后一条规则的这些前提，那么那么a满足满足m n 证明证明 根据证明规则的集合，分情况进行分析根据证明规则的集合，分情况进行分析3.3 等式、可靠性和完备性等式、可靠性和完备性命题命题 存在一个代数理论存在一个代数理论e和不含和不

24、含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

25、, 2, : nat +, : nat nat nat empty : stack push : nat 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 ) = s3.3 等式、可靠性和完备性等式、可靠性和完备性等式等式push (top s) (pop s) = ss : stack是不可证是不可证明的明的任何形式为任何形式为top empty = m 的

26、等式都是不可证明的，假定的等式都是不可证明的，假定m是类别为是类别为nat的项，并且不含的项，并且不含empty3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.4 完备性的形式完备性的形式用于不同逻辑系统的三种形式的完备性用于不同逻辑系统的三种形式的完备性最弱的形式：所有的永真公式都是可证的最弱的形式：所有的永真公式都是可证的演绎完备性：演绎完备性：每个语义蕴涵在证明系统中都每个语义蕴涵在证明系统中都是可推导的是可推导的最小模型完备性：最小模型完备性：每个语法理论是某一个每个语法理论是某一个“最小最小”模型的语义理论模型的语义理论 对代数来说，最小模型完备性意味着每个语法理对代数来说，

27、最小模型完备性意味着每个语法理论是某个代数论是某个代数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 成立成

28、立e1和和e2都不是都不是e的语义蕴涵的语义蕴涵 不存在一个代数，其理论正好就是由不存在一个代数，其理论正好就是由e的等式推的等式推论组成的语法理论论组成的语法理论 3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.5 同余、商和演绎完备性同余、商和演绎完备性同余关系同余关系：等价关系加上同余性：等价关系加上同余性同余性：指函数保可证明的相等同余性：指函数保可证明的相等性性对单类代数对单类代数a = a, f1a, f2a, ，同余关系是载体，同余关系是载体a上上的 等 价 关 系 ， 使 得 对 每 个的 等 价 关 系 ， 使 得 对 每 个 k 元 函 数元 函 数 fa， 如 果

29、， 如 果ai bi(i=1, k)，即，即ai和和bi等价，那么等价，那么f a(a1, , ak ) fa (b1, , bk )。对多类对多类 代数代数a = as , i ，同余关系是一簇等价关，同余关系是一簇等价关系系 s , s as as，使得对每个，使得对每个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的

30、一个元素的一个元素等价类等价类aa a as a a 商代数商代数a定义：定义：(a)s是由是由as的所有等价类构成的集合的所有等价类构成的集合ass a s 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，上的同余关系上的同余

31、关系“模模k等价等价” 这个商代数是大家熟悉的整数模这个商代数是大家熟悉的整数模k加结构。如果加结构。如果k等于等于5，那么，那么 3 4 2 3.3 等式、可靠性和完备性等式、可靠性和完备性如果如果 是是a的一个环境，的一个环境， 是一个同余关系，是一个同余关系，那么那么a的环境的环境 定义如下：定义如下： (x) = (x) 反过来，对于反过来，对于a的环境的环境 ，对应它的，对应它的a的环的环境境 有多种选择有多种选择引 理引 理 令令 是是 代 数代 数 a 上 的 同 余 关 系 ， 项上 的 同 余 关 系 ， 项m terms( , )并且并且 是满足是满足 的环境。那么项的环境

32、。那么项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 非

33、空类别和最小模型性质非空类别和最小模型性质类别类别s非空：集合非空：集合termss( , )不是空集不是空集对应的载体肯定非空对应的载体肯定非空没有没有空载体空载体时，可以增加推理规则时，可以增加推理规则(nonempty)定理定理 令令e是封闭于规则是封闭于规则（nonempty）的语法的语法理论，那么存在所有载体都非空的代数理论，那么存在所有载体都非空的代数a，使，使得得e th (a) 没有空载体的代数有最小模型完备性没有空载体的代数有最小模型完备性m = n , x : s m = n 3.4 同态和初始性同态和初始性3.4.1 同态和同构同态和同构将同态和同构的概念从单类代数推广到

34、多类将同态和同构的概念从单类代数推广到多类代数代数 同态是从一个代数到另一个代数的保结构的同态是从一个代数到另一个代数的保结构的映射（或叫做翻译）映射（或叫做翻译）从从 代数代数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的等价关系。那的等价关系。那么把么把n n映射到它的等价类映射到它的等价类n 是从是从n到

35、到n的一个同态，因为的一个同态，因为h (0) = 0n = 0 h (n + m) = h (n) n h (m) = n + m 任何代数到它商代数的同态都用这种方式定任何代数到它商代数的同态都用这种方式定义义3.4 同态和初始性同态和初始性例例 含义函数是从项代数含义函数是从项代数t = terms( , )到任意代到任意代数数a的一个同态的一个同态h : t a。如果。如果 是是a的一个的一个满足满足 的环境，该同态的定义是的环境，该同态的定义是h(m) = am 这是一个同态，因为这是一个同态，因为h (f m1 mk ) = af m1 mk = f a(am1 amk ) = f

36、 a(h (m1 ) h (mk ) )3.4 同态和初始性同态和初始性引理引理 令令h : a b是任意同态，并且是任意同态，并且 是满足是满足类别指派类别指派 的任意的任意a环境。那么对任何项环境。那么对任何项m terms( , )，有，有h (am ) = bm h当当m中不含变量时，中不含变量时，h (am) =bm证明证明 基于项的归纳基于项的归纳引理引理 如果如果h : a b和和k : b c都是都是 代数的代数的同态，那么合成同态，那么合成k h : a c也是也是 代数的同代数的同态。态。 ( (k h)s = ks hs) 同构同构 一个双射的同态一个双射的同态, 写成写

37、成a b3.4 同态和初始性同态和初始性3.4.2 初始代数初始代数c是一类是一类 代数并且代数并且a c，若对每个，若对每个b c，存，存在唯一的同态在唯一的同态h : a b，那么，那么a在在c中叫做中叫做初初始代数始代数 初始代数是初始代数是“典型典型”的的 初始代数有尽可能少的非空载体初始代数有尽可能少的非空载体 初始代数满足尽可能少的闭等式初始代数满足尽可能少的闭等式ab3b2b13.4 同态和初始性同态和初始性例例 基调基调 0 类别类别nat， 函数符号函数符号0 : nat和和s : nat nat。 令令c是所有是所有 0代数构成的代数类代数构成的代数类 闭项代数闭项代数t

38、terms( 0, )是是c的初始代数的初始代数它的载体是所有闭项它的载体是所有闭项0, s (0), , s k(0), 该代数的函数该代数的函数s把把sk(0)映射到映射到sk 1(0)该代数的元素少到能解释所有的函数符号该代数的元素少到能解释所有的函数符号该代数满足项之间尽可能少的等式该代数满足项之间尽可能少的等式3.4 同态和初始性同态和初始性引理引理 假定假定h : a b和和k : b a都是同态，并都是同态，并且且h k=idb，k h =ida。那么。那么a和和b同构同构命题命题 如果如果a和和b在代数类在代数类c中都是初始代数，中都是初始代数，那么那么a和和b是同构的是同构的

39、命题命题 令令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 (

40、x + y)sk0 + sl0 = sk + l0对任何闭项对任何闭项m，存在某个自然数，存在某个自然数k，使得，使得m = sk0 等式等式sk0 = sl0是不可证明的，除非是不可证明的，除非k = l 每个等价类正好包含一个形式为每个等价类正好包含一个形式为sk0的项的项 等价类和形式为等价类和形式为sk0的项集间有一个双射的项集间有一个双射载体看成由闭项载体看成由闭项0, s0, , sk0, 构成的集合，函数构成的集合，函数s映射映射sk0 sk10， 映射映射(sk0, sl0) skl0，得一个初始代数，得一个初始代数这个初始代数和该基调的标准模型（有后继算子和加法的这个初始代数

41、和该基调的标准模型（有后继算子和加法的自然数）自然数） 同构同构3.4 同态和初始性同态和初始性该规范的初始代数可以和其它有更多或较少元素的该规范的初始代数可以和其它有更多或较少元素的代数相对照代数相对照 如果一个代数有更多元素的话，那么这些多余的元素不能如果一个代数有更多元素的话，那么这些多余的元素不能由项定义。（有假货）由项定义。（有假货）整数代数整数代数za = anat, 0a, sa, +a anat = ( 0 n) (1 z)0a = 0, 0 sa i, n = i, n +1 i, n +a j, m = max(i, j), n +m 如果一个代数有较少元素的话，那么就有一

42、些不能被证明如果一个代数有较少元素的话，那么就有一些不能被证明为相等的有区别的元素被等同。（出现混淆）为相等的有区别的元素被等同。（出现混淆）模模k的自然数的自然数3.4 同态和初始性同态和初始性初始代数可能满足不能由初始代数可能满足不能由e证明的额外的等式证明的额外的等式例例 上面的自然数基调例子中，初始代数满足上面的自然数基调例子中，初始代数满足等式等式x + y = y + x 因为因为 e m = sk0和和e n = sl0 蕴涵蕴涵 e m + n = sk+l0 = n + m不满足交换性的代数不满足交换性的代数anat是所有是所有f : x x的函数的集合（的函数的集合（x至少

43、有两个元素至少有两个元素）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来说是初来

44、说是初始代数。对任何始代数。对任何 等式等式m n，下面三个条，下面三个条件等价件等价 a满足满足m na满足满足m n的每一个基实例的每一个基实例m n的每一个基实例都可以从的每一个基实例都可以从e证明证明3.5 代数数据类型代数数据类型3.5.1 代数数据类型代数数据类型很多数据类型很多数据类型 不存在标准的数学构造不存在标准的数学构造 没有单一和标准的计算机实现没有单一和标准的计算机实现 列出它们的操作并描述这些操作的行为列出它们的操作并描述这些操作的行为 公理化地定义而不是由数学构造来定义公理化地定义而不是由数学构造来定义 对于一个数据类型，是否可以断定有了对于一个数据类型，是否可以断

45、定有了“足够足够”的公理的公理本节讨论数据类型公理化方法的一般特征本节讨论数据类型公理化方法的一般特征3.5 代数数据类型代数数据类型数据抽象的一般原理数据抽象的一般原理 抽象数据类型由它的规范定义。使用这样数据类抽象数据类型由它的规范定义。使用这样数据类型的程序应该只依赖于由它的规范保证的性质，型的程序应该只依赖于由它的规范保证的性质，而不依赖于它的任何特定实现而不依赖于它的任何特定实现 一个数据类型的函数可以划分成一个数据类型的函数可以划分成构造算子：产生该数据类型的一个新元素构造算子：产生该数据类型的一个新元素运算算子：运算算子：是该数据类型上的函数，但不产生新是该数据类型上的函数，但不

46、产生新的元素的元素观察算子：观察算子：作用于该数据类型的元素，但返回某作用于该数据类型的元素，但返回某其它类型的元素，如自然数或布尔值其它类型的元素，如自然数或布尔值3.5 代数数据类型代数数据类型3.5.2 初始代数语义和数据类型归纳初始代数语义和数据类型归纳代数规范有几种不同的代数规范有几种不同的“语义语义”形式形式宽松语义：宽松语义：满足一个代数规范的所有代数所构成满足一个代数规范的所有代数所构成的代数类的代数类初始代数语义：初始代数语义：满足一个代数规范的所有初始代满足一个代数规范的所有初始代数所构成的同构类数所构成的同构类终结代数语义：终结代数语义：满足一个代数规范的所有满足一个代数

47、规范的所有终结终结代代数所构成的同构类数所构成的同构类生成语义：生成语义：满足一个代数规范的所有满足一个代数规范的所有生成生成代数所代数所构成的代数类构成的代数类3.5 代数数据类型代数数据类型初始代数的性质初始代数的性质没有假货没有假货没有混淆没有混淆 支持基于数据类型构造符的归纳支持基于数据类型构造符的归纳构造符集合构造符集合s p e c , e 的 函 数 符 号 子 集的 函 数 符 号 子 集 f0， 使 得， 使 得terms( ,)e,的每个等价类正好只含一个由的每个等价类正好只含一个由f0的函数符号所构成的基项的函数符号所构成的基项 可以基于对构造符的归纳来证明初始代数的性质

48、可以基于对构造符的归纳来证明初始代数的性质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

49、 = 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 ) condn true x y = x condn false x y = y . . .3.5 代数数据类型代数数据类型终结代数终结

50、代数在一个代数类在一个代数类c中，如果从每个中，如果从每个b c到到a c，都，都存在唯一的同态，那么代数存在唯一的同态，那么代数a是终结代数是终结代数 一个代数类中的所有终结代数都同构一个代数类中的所有终结代数都同构 若用终结代数作为语义，则称之为终结语义若用终结代数作为语义，则称之为终结语义如果所有载体都是单元素集合的代数也在如果所有载体都是单元素集合的代数也在c中，中，则这个代数一定是则这个代数一定是c的终结代数的终结代数3.5 代数数据类型代数数据类型初始语义和终结语义初始语义和终结语义 初始语义初始语义：不能证明为相等的就是不相等的不能证明为相等的就是不相等的 终结语义终结语义：不能

51、证明为不相等的则是相等的不能证明为不相等的则是相等的 如果把某些类别的解释固定，而其它类别的解释如果把某些类别的解释固定，而其它类别的解释用终结语义，则它是一个有用的方法用终结语义，则它是一个有用的方法从初始语义角度看，前面给出的不是集合的规范从初始语义角度看，前面给出的不是集合的规范,而是表的规范。因为不能证明而是表的规范。因为不能证明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 若用终结语义，且若用终结语义，

52、且bool的解释固定的解释固定, ,则为集合规范则为集合规范3.5 代数数据类型代数数据类型3.5.3 解释没有意义的项解释没有意义的项表达式没有意义的情况表达式没有意义的情况 除法是一个部分函数，除数为零的表达式没意义除法是一个部分函数，除数为零的表达式没意义 调用不终止的函数也构成一个没有意义的表达式调用不终止的函数也构成一个没有意义的表达式 如果想在代数规范中表示这些情况，必须在基调如果想在代数规范中表示这些情况，必须在基调中增加表示错误的项（简称错误值）中增加表示错误的项（简称错误值）怎样规定这些项的值？有三种可能：怎样规定这些项的值？有三种可能：什么也不规定什么也不规定任意做一个决定

53、任意做一个决定非常仔细地说明什么是所需要的非常仔细地说明什么是所需要的3.6 重写系统重写系统3.6.1 基本定义基本定义重写系统：用于代数项的归约系统重写系统：用于代数项的归约系统两种重要的应用两种重要的应用 为代数项提供一种计算模型为代数项提供一种计算模型 自动定理证明自动定理证明由一组叫做重写规则由一组叫做重写规则( (lr) )的有向等式组成的有向等式组成 限制：限制：var(r) var(l)由由r r 确定的一步归约关系确定的一步归约关系rsl xm r sr x m 关系关系 r是是r的自反传递闭包的自反传递闭包3.6 重写系统重写系统sorts : natfctns : 0 :

54、 nat : nat nat + : nat nat nat在这个基调上的一些归约规则如下：在这个基调上的一些归约规则如下：x 0 xx + ( x) 0(x y ) z x + (y + z)实例：实例：(x y ) ( y) x + (y + ( y) x 0 x 3.6 重写系统重写系统引理（引理（归约保类别归约保类别 ） 令令r r是是 上的重写系统上的重写系统. .如果如果m termss ( , )，并且，并且m r n，那，那么么n termss ( , ) 关系关系 （重写系统重写系统）是是合流的合流的，如果，如果n m p蕴涵蕴涵n p的话的话关系关系 （重写系统重写系统）是

55、终止的，如果不存在）是终止的，如果不存在一步归约的无穷序列一步归约的无穷序列m0 m1 m2不能再归约的项称为不能再归约的项称为范式范式合流并且终止的重写系统通常又叫做典范系合流并且终止的重写系统通常又叫做典范系统统3.6 重写系统重写系统可变换性可变换性 如果存在如果存在m m1 m2 m3 mk n 则项则项m, n termss ( , )是是可变换的，写成可变换的，写成m r n 箭头的方向并没有什么意义箭头的方向并没有什么意义 对任何重写系统，可变换性和可证明的相等性是对任何重写系统，可变换性和可证明的相等性是一致的一致的3.6 重写系统重写系统项中的一个项中的一个位置：便于位置：便

56、于引用子项的某个特定引用子项的某个特定出现出现 位置位置n = 1, 2的子项是的子项是hab 用用m n表示表示m在在位置位置n的子项的子项 用用 n n m表示表示m在在n的子项的子项由由n代换的结果代换的结果fggxxhababf (gx(hab)(gba) x3.6 重写系统重写系统3.6.2 合流性和可证明的相等性合流性和可证明的相等性记号记号 如果如果r是一组重写规则，是一组重写规则，er用来表示对应用来表示对应的无向的等式集合的无向的等式集合定理定理 对任何重写系统对任何重写系统r，mr n当且仅当当且仅当er m n对任何合流的重写系统对任何合流的重写系统r，er m n当当且

57、仅当且仅当m r r n 3.6 重写系统重写系统3.6.3 终止性终止性良基关系：集合良基关系：集合a上的一个关系上的一个关系 是是良基的良基的，如果不存在如果不存在a上元素的无穷递减序列上元素的无穷递减序列a0 a1 a2 的话。的话。如果能在项和有良基关系的集合如果能在项和有良基关系的集合a的元素间建的元素间建立起一个对应，那么可以利用它去证明不存立起一个对应，那么可以利用它去证明不存在无穷的归约序列在无穷的归约序列m0 m1 m2 有几种方式可把项映射到有良基关系的集合有几种方式可把项映射到有良基关系的集合 利用代数的语义结构利用代数的语义结构3.6 重写系统重写系统代数代数a = a

58、s1, 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是是 项上的

59、一个重写系统，并且令项上的一个重写系统，并且令a是一个良基的是一个良基的 代数。如果对代数。如果对r中每条规则中每条规则l r有有a l r，那么，那么r是终止的是终止的例例 x x 载体载体abool n 0, 1 (x 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 临界对临界对局部合流局部合流关系关

60、系是局部合流的，如果是局部合流的，如果n m p蕴涵蕴涵n p 局部合流关系严格弱于合流关系局部合流关系严格弱于合流关系 例例a b, b aa a0, b b0a0abb03.6 重写系统重写系统cond b (cdr(cons s l) (cons(car l )(cdr l ) )规则如下：规则如下：cdr(cons x l) lcons(car l )(cdr l ) l 不相交的归约不相交的归约mslsl msrsl mslsr msrsr 3.6 重写系统重写系统cdr(cons x(cons(car l )(cdr l )规则如下：规则如下：cdr(cons x l) lcons