泛代数和代数数据类型

1、泛代数和代数数据类型第1页，共85页，2022年，5月20日，10点24分，星期四2.1 引 言代数数据类型包括一个或多个值集一组在这些集合上的函数基本限制是其函数不能有函数变元基本“类型”(type)符号被称为“类别” (sort)泛代数（也叫做等式逻辑）定义和研究代数数据类型的一般数学框架本章研究泛代数和它在程序设计中定义常用数据类型时的作用 第2页，共85页，2022年，5月20日，10点24分，星期四2.1 引 言本章主要内容：代数项和它们在多类别代数中的解释等式规范（也叫代数规范）和等式证明系统等式证明系统的可靠性和完备性（公理语义和指称语义的等价）代数之间的同态关系和初始代数数据类

2、型的代数理论从代数规范导出的重写规则（操作语义）包括了大多数逻辑系统中的一些公共议题第3页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项2.2.1 代数代数一个或多个集合，叫做载体一组特征元素和一阶函数，也叫做代数函数f : A1 Ak A例：N N, 0, 1, +, 载体N是自然数集合特征元素0, 1N，也叫做零元函数函数+, : N N N第4页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项多个载体的例子 APCF N, B, 0, 1, , +, true, false, Eq ?, 下面逐步给出代数的一种语法描述，有穷的

3、语法表示在计算机科学中十分重要，可用来定义数据类型证明数据类型的性质还必须讨论这种语法描述的指称语义 满足一组等式的除了APCF外，可能还有： A5PCF N5, B, 0, 1, 2, 3, 4, +5, true, false, Eq ?, 第5页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项2.2.2 代数项的语法基调 S，FS是一个集合，其元素叫做类别函数符号f : s1 sk s的集合F ，其中表达式s1 sk s叫做f 的类型零元函数符号叫做常量符号例: N S，Fsorts : natfctns : 0, 1 : nat , : nat nat n

4、at 第6页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项项定义基调的目的是用于写代数项项中可能有变量，因此需假定一个无穷的符号集合V，其元素称为变量类别指派 x1 : s1, , xk : sk基调S，F和类别指派上类别s的代数项集合Termss (, )定义如下：1、如果x : s ，那么x Termss (, )2、如果f : s1 sk s并且Mi Terms (, ) (i 1, , k)，那么f M1 Mk Termss (, ) 当k 0时，如果f : s，那么f Termss (, )si第7页，共85页，2022年，5月20日，10点24分，星

5、期四2.2 代数、基调和项项的例子0, 0 1 Termsnat (N, )0 x Termsnat (N, )，其中 x : nat, 代数项中无约束变元NxM就是简单地把M中x的每个出现都用N代替记号, x : s x : s引理2.1若MTermss(, , x : s)且NTermss(, )，那么NxMTermss (, )证明 按Termss(, )中项的结构进行归纳第8页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项例用基调stk S, F来写自然数和自然数栈表达式sorts : nat, stackfctns : 0, 1, 2, : nat ,

6、 : nat nat nat empty : stack push : nat stack stack pop : stack stack top : stack natpush 2 (push 1 (push 0 empty) )是该基调的项第9页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项2.2.3 代数以及项在代数中的解释基调的代数是为代数项提供含义的数学结构是一个基调，则代数A包含对每个s S，正好有一个载体As一个解释映射I 把函数I (f ) : A A As 指派给函数符号 f : s1 sk s F把I (f ) As指派给常量符号f : s

7、F N代数N 写成N N, 0N, 1N, N, N sks1第10页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项代数A的环境 : V s As环境 满足如果对每个x : s 都有(x)AsM Termss(, )的含义AM是 Ax (x) AM fA (AM1, , AMk)若f : s是常量符号，则Af fA若A清楚时，省略A而直接写成M不依赖于时，用AM表示M在A中的含义第11页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项例 若(x) 0N x 1 N(x, 1) N (x), 1N) N (0N, 1N) 1N第12页

8、，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项例 Astk N, N, 0A, 1A, , A, A, emptyA, pushA, pop A, top AemptyA , 空序列pushA(n, s) n : spopA(n : s) spopA( ) topA(n : s) ntopA( ) 0A若把x:nat映射到自然数3，把s:stack映射到2, 1 pop(push x s) popA(pushA( x , s ) ) popA(pushA(3, 2, 1 ) ) popA( 3, 2, 1 ) 2, 1 第13页，共85页，2022年，5月20日

9、，10点24分，星期四2.2 代数、基调和项引理2.2 令A是代数，MTermss(, )，并且是满足的环境，那么M As证明 根据Termss(, )中项的结构进行归纳引理2.3 令x1, , xk是由出现在MTermss(, )中的所有变量构成的变量表，1和2是满足的两个环境, 并且对i1, , k有1(xi) 2(xi), 那么M1 M2证明 基于项结构的归纳第14页，共85页，2022年，5月20日，10点24分，星期四2.2 代数、基调和项2.2.4 代换引理引理2.4令MTermss(, , x:s)并且N Termss(, )，那么NxMTermss(, )。并且对任何环境，有

10、NxM M (x a)，其中a N，它是N在下的含义证明 根据项M的结构进行归纳第15页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性代数规范一个基调 + 一组等式调查什么样的代数满足这些等式强加的要求使用等式证明系统可推导的新的等式可靠性：从规范可证明的等式在任何满足该规范的代数中都成立完备性：在满足规范的所有代数中都成立的等式都可从该规范证明代数规范是描述代数数据类型公理语义的工具第16页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性2.3.1 等式公式 M N ，对某个s，M, N Termss (, ) 若满足

11、，并且还有M N，则认为代数A在环境下满足M N ，写成A, M N 若A在任何环境下都满足该等式，则写成 A M N 若代数类C中的任何代数A都满足该等式，写成 C M N 若任何一个代数都满足等式M N ，则写成 M N(永真的、有效的 )第17页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性平凡的代数若A满足上所有等式，就说代数A是平凡的例令有两个类别a和b，令A是一个代数，其中Aa0,1并且Ab A不可能满足x y x : a, y : a，即下式不成立 A x y x : a, y : a但是A x y x : a, y : a, z : b无意

12、义地成立 第18页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性2.3.2 项代数项代数Terms(, )类别s的载体：集合Termss(, )函数符号f : s1 sk s的解释I (f ) (M1, , Mk) f M1 Mk项代数Terms(, )的环境也叫做一个代换如果S是代换，则用SM表示同时把M中的各个变量x用Sx替换的结果因此用M表示把代换作用于M的结果第19页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性例类别u函数符号f : u u和g : u u u a : u, b : u, c : uTu a,

13、 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)第20页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性引理2.5 令MTerms(, )，并且是满足的项代数Terms(, )的环境，那么M M证明 对项进行归纳证明从项代数可以知道，只有M和N是语法上相同的项时，等式M N 才会永真第21页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性2.3.3 语

14、义蕴涵和等式证明系统代数规范Spec , E : 基调和一组等式E语义蕴涵：E M N 满足E的所有代数A都满足等式M N 语义理论E ：如果E M N 蕴涵M N E代数A的理论Th(A)在A中成立的所有等式的集合这是一个语义理论第22页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性回顾证明系统的可靠性若等式E从一组假设E可证，则E语义上蕴涵E证明系统的完备性若E 语义上蕴涵等式E，则E从E可证下一步先给出代数证明系统，然后讨论可靠性和完备性第23页，共85页，2022年，5月20日，10点24分，星期四1、语义相等是个等价关系，因此有M M 2、在等式

15、中增加类别指派的规则3、等价代换M = N N = M M = N N = P M = P M = N M = N , x : sM = N , x : s P = Q P/xM = Q/xN 2.3 等式、可靠性和完备性x不在中P , Q Termss(, )第24页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性等式可证若从E中的等式和公理(ref)及推理规则(sym)、(trans)、(subst) 和(add var) 可推出等式M N ，则说该等式可证，写成 E M N 语法理论如果E M N 蕴涵 M N E E的语法理论Th(E)从E可证的所有

16、等式的集合第25页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性等式集合E是语义一致的若存在某个等式M N ，它不是E的语义蕴涵等式集合E是语法一致的若存在某个等式M N ，它不能由E证明第26页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性例 在基调stk S, F上增加等式top (push x s ) = x s : stack, x : natpop (push x s ) = s s : stack, x : nat 使用这些等式可以证明等式top (push 3 empty ) = 3top(push x

17、s ) = x s : stack, x : nat empty = empty x : nat top(push x empty ) = x x : nat3 = 3 top(push 3 empty ) = 3 第27页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性导出规则 f : s1 sk s Mi, NiTerms (, ) 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 si第28页，共85页，2

18、022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性定理2.6（可靠性）如果E M N ，那么E M N 证明 可以根据该证明的长度进行归纳归纳基础：长度为1的证明，它是公理或E的一个等式归纳假设：M N 的最后一步是从E1, , En得到，那么，若A E，则A满足E1, , En要证明：若A满足最后一条规则的这些前提，则A满足M N 证明 根据证明规则的集合，分情况进行分析第29页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性命题2.7存在代数理论E和不含x的项M和N，使得E M =N , x : s，但是E M =N 证明令基调有类别

19、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证明的第30页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性例栈代数规范sorts : nat, stackfctns : 0, 1, 2, : nat +, : nat nat nat empty : stack push: nat stack stack pop : stac

20、k 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第31页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性等式push (top s) (pop s) = s s : stack是不可证的任何形式为top empty = M 的等式都是不可证的，若M是类别为nat的项，并且不含empty第32页，共85页，2022年，5月20日，10点24分，星期四2.3

21、等式、可靠性和完备性2.3.4 完备性的形式用于不同逻辑系统的三种不同形式的完备性1、最弱的形式所有的永真公式都是可证的2、演绎完备性每个语义蕴涵在证明系统中都是可推导的3、最小模型完备性每个语法理论都是某个“最小”模型的语义理论对代数来说，最小模型完备性意味着每个语法理论是某个代数A的Th(A) “最小模型”是指它的理论包含的等式最少第33页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性最小模型完备性不一定成立考虑等式E x = y x : a, y : a, z : b 1、a的载体只含一个元素，则E满足，此时E1 x = y x : a, y : a

22、 成立 2、b的载体为空，则E也满足，此时E2 z = w z : b, w : b 成立 E1和E2都不是E的语义蕴涵 不存在代数，其理论正好就是由E的等式推论组成的语法理论第34页，共85页，2022年，5月20日，10点24分，星期四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 同余关系是一

23、簇等价关系 s, s AsAs，使得对每个f : s1 sks及变元序列a1, , ak和b1, , bk(ai s bi As ),有fA(a1, , ak ) s fA(b1, , bk )ii第35页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性 A模的商的代数A 把A中有关系元素a a 压缩成A的一个元素等价类aa a As a a 商代数A定义：(A)s是由As的所有等价类构成的集合Ass as a As函数fA由A的函数fA确定对适当载体的a1, ak，fA (a1, , ak) = fA(a1, , ak)第36页，共85页，2022年，5月

24、20日，10点24分，星期四2.3 等式、可靠性和完备性上面定义有意义的条件是fA(a1, , ak)必须只依赖于a1, , ak，而不能依赖于所选的代表a1, , ak例单类别代数N，0，1，上的同余关系“模k等价”这个商代数是众所周知的整数模k的加结构。如果k等于5，那么3 4 2第37页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性如果是A的一个环境，是一个同余关系，那么A的环境 定义如下： (x) = (x)反过来，对于A的环境，对应它的A的环境有多种选择引理2.8令是代数A上的同余关系，项MTerms(, )并且是满足的环境。那么项M在商代数A和

25、环境下的含义(A)M由下式决定(A )M = AM第38页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性引理2.9令E是一组等式集合，令Terms(, )是基调上的项集。由E的可证明性确定的关系E, 是Terms(, )上的同余关系定理2.10（ 完备性）如果E M N ，那么E M N 完备性定理加上可靠性定理表明语法理论和语义理论相同第39页，共85页，2022年，5月20日，10点24分，星期四2.3 等式、可靠性和完备性2.3.6 非空类别和最小模型性质没有空载体的代数有最小模型完备性 类别s非空：集合Termss(, )不是空集对应的载体肯定非空

26、没有空载体时，可以增加推理规则(nonempty)定理2.11令E是封闭于规则（nonempty）的语法理论，那么存在所有的载体都非空的代数A，使得ETh(A) M = N , x : s M = N 第40页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性2.4.1 同态和同构将同态和同构概念从单类代数推广到多类代数 同态是从一个代数到另一个代数的保结构的映射从代数A到B的同态h : A B一簇映射h = hs | s S ，使得对的每个函数符号f : s1 sk s，有hs(f A(a1, , ak) ) = f B(hs (a1), , hs (ak) )1k

27、第41页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性例令N = N, 0, 1, ，是模k的等价关系,则把nN映射到它的等价类n是从N到N的一个同态，因为h(0) = 0N = 0h(n + m) = h(n) N h(m) = n + m任何代数到它商代数的同态都用这种方式定义第42页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性例含义函数是从项代数T = Terms(, )到任意代数A的一个同态h : T A。如果是A的一个满足的环境，该同态的定义是h(M) = AM这是一个同态，因为h (f M1 Mk ) = A f M1

28、Mk = fA(AM1, AMk) = fA(h (M1), , h (Mk) )第43页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性引理2.13令h :AB是任意同态，并且是满足类别指派的任意A环境。那么对任何项MTerms(, )，有h(AM) = BMh当M中不含变量时，h(AM) =BM证明 基于项的归纳引理2.14如果h :AB和k :B C都是代数的同态，那么合成kh :AC也是代数的同态， (k h)s = ks hs同构 一个双射的同态, 写成A B第44页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性2.4.2 初

29、始代数 C是一类代数并且AC，若对每个BC，存在唯一的同态h : AB，则A在C中叫做初始代数初始代数是“典型”的初始代数有尽可能少的非空载体初始代数满足尽可能少的闭等式AB3B2B1第45页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性例 基调0类别nat，函数符号0 : nat和S : nat nat令C是所有0代数构成的代数类闭项代数T Terms(0, )是C 的初始代数它的载体是所有闭项0, S(0), , Sk(0), 该代数的函数S把Sk(0)映射到Sk1(0)该代数的元素少到能解释所有的函数符号该代数满足项之间尽可能少的等式第46页，共85页，20

30、22年，5月20日，10点24分，星期四2.4 同态和初始性引理2.15假定h : AB和k : BA都是同态，并且h k = IdB，k h = IdA。那么A和B同构命题2.16若A和B在代数类C中都是初始代数，则A和B同构命题2.17令E是一组等式，且令A=Terms(, )E, 是模可证明的相等性的代数，则A对E来说是初始代数由项代数和商的性质可知，从E可证明的等式在A中都成立还要证明从A到任何满足E的代数有唯一的同态第47页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性例sorts:natfctns:0 : natS : nat nat : nat na

31、t nat；eqns：x : nat, y : natx + 0 = xx + (Sy) = S(x + y)可以证明如下事实：Sk0 + Sl0 = Sk + l0对任何闭项M，存在某个自然数k，使得M = Sk0第48页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性例x + 0 = xx + (Sy) = S (x + y)可以证明如下事实：等式Sk0 = Sl0是不可证的，除非k = l每个等价类正好包含一个形式为Sk0的项等价类集和形式为Sk0的项集间有一个双射若把闭项集合0, S0, , Sk0, 作为载体，函数S映射Sk0 Sk10，映射(Sk0, S

32、l0) Skl0，则得一个初始代数这个初始代数和该基调的标准模型（有后继算子和加法的自然数）同构第49页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性初始代数和其他代数的比较1、和有更多元素的代数比较多余的元素不能由项定义（有垃圾）例1：整数代数Z例2：A = Anat, 0A, SA, +AAnat = (0 N) (1 Z)0A = 0, 0SAi, n = i, n +1i, n +A j, m = max(i, j), n+m第50页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性初始代数和其他代数的比较2、和有较少元素的代数比

33、较一些不能证明为相等的项在该代数中被等同（有混淆）例：模k的自然数第51页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性初始代数的一个重要特点初始代数可能会满足不能由E证明的额外的等式例：自然数基调例子中，初始代数满足等式x + y = y + x因为 E M = Sk0和E N = Sl0 蕴涵E M + N = Sk+l0 = N + M第52页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性自然数基调例子中，初始代数满足等式x + y = y + x不满足交换律的代数Anat是所有f : X X的函数的集合（X至少有两个元素）0A

34、是X上的恒等函数，SA是Anat上的恒等映射+A是Anat上的函数合成 A = Anat 0A SA +A满足E+A没有交换性，因为函数合成没有交换性第53页，共85页，2022年，5月20日，10点24分，星期四2.4 同态和初始性基项、基代换、基实例（项、等式）如果M N 是Termss(, )的项之间的等式，并且S是一个，基代换，则把SM SN 称为M N 的基实例命题2.18令E是一组等式，且A对E来说是初始代数，则对任何等式M N ，下面三个条件等价 A满足M N A满足M N 的每一个基实例 M N 的每一个基实例都可以从E证明第54页，共85页，2022年，5月20日，10点24

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

36、元素运算算子：是该数据类型上的函数，但不产生新的元素观察算子：应用于该数据类型的元素，但返回其它类型的元素，如自然数或布尔值第56页，共85页，2022年，5月20日，10点24分，星期四2.5 代数数据类型 初始代数语义和数据类型归纳代数规范有几种不同的“语义”形式宽松语义：满足一个代数规范的所有代数所构成的代数类初始代数语义：满足一个代数规范的所有初始代数所构成的同构类终结代数语义：满足一个代数规范的所有终结代数所构成的同构类生成语义：满足一个代数规范的所有生成代数所构成的代数类第57页，共85页，2022年，5月20日，10点24分，星期四2.5 代数数据类型初始代数的性质没有垃圾没有混

37、淆支持基于数据类型构造符的归纳构造符集合Spec , E的函数符号集合的子集F0，使得Terms(,)E,的每个等价类正好只含一个由F0的函数符号所构成的基项可以基于对构造符的归纳来证明初始代数的性质第58页，共85页，2022年，5月20日，10点24分，星期四2.5 代数数据类型sorts:set, nat, bool 构造符、运算符、观察符fctns:0, 1, 2, : nat+ : nat nat nat Eq? : nat nat booltrue, false bool empty : setinsert : nat set set union : set set setisme

38、m? : 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, . . . 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

39、) s = insert y (union s s) condn true x y = x condn false x y = y . . .第59页，共85页，2022年，5月20日，10点24分，星期四2.5 代数数据类型终结代数在一个代数类C中，如果从其中的每个B到其中某个A，都存在唯一的同态，那么代数A是终结代数一个代数类中的所有终结代数都同构若用终结代数作为语义，则称之为终结语义如果所有载体都是单元素集合的代数也在C中，则这个代数一定是C的终结代数第60页，共85页，2022年，5月20日，10点24分，星期四2.5 代数数据类型初始语义和终结语义初始语义：不能证明为相等的就是不相等

40、的终结语义：不能证明为不相等的则是相等的如果把某些类别的解释固定，而其它类别的解释用用终结语义，则它是一个有用的方法从初始语义角度看，前面给出的不是集合的规范,而是表的规范。因为不能证明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的解释固定,则为集合规范第61页，共85页，2022年，5月20日，10点24分，星期四2.5 代数数据类型 解释没有意义的项表达式没有意义的情况除法是一个部分函

41、数，除数为零的表达式没意义调用不终止的函数也构成一个没有意义的表达式如果想在代数规范中表示这些情况，必须在基调中增加表示错误的项（简称错误值）怎样规定这些项的值？有三种可能：什么也不规定任意做一个决定非常仔细地说明什么是所需要的第62页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统 基本定义重写系统：用于代数项的归约系统R两种重要的应用为代数项提供一种计算模型自动定理证明由一组叫做重写规则(LR)的有向等式组成限制：Var(R) Var(L)由R确定的一步归约关系RSLxM R SRxM关系R是R的自反传递闭包第63页，共85页，2022年，5月20日，10点24分，

42、星期四2.6 重写系统sorts : natfctns : 0 : 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第64页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统引理2.19（归约保类别）令R是上的重写系统，若M Termss(, )且MRN，则N Termss(, ) 如果N M P蕴涵N P，则关系（重写系统）是合流的若不存在一步归约的无穷序列M0M1 M2，则关系（重写系统）是终止的

43、不能再归约的项称为范式合流且终止的重写系统通常又叫做典范系统第65页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统可变换性 若存在M M1 M2 M3 Mk N，则项M, N Termss(, )是可变换的，写成M R N归约的无向版本箭头的方向并没有什么意义对任何重写系统，可变换性以及可证明的相等性（把重写规则看成等式）是一致的第66页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统用自然数的有穷序列来表示项中的位置位置n = 1, 2的子项是hab用M n表示M在位置n的子项用N nM表示M在n的子项由N代换的结果便于引用子项的某个特定出现

44、fggxxhababf (gx(hab)(gba) x第67页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统 合流性和可证明的相等性记号若R是一组重写规则，ER用来表示对应的无向的等式集合定理2.201、对任何重写系统R，M RN 当且仅当ER M N；2、对任何合流的重写系统R，ER M N 当且仅当M R R N第68页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统2.6.3 终止性良基关系集合A上的一个关系是良基的，如果不存在A上元素的无穷递减序列a0 a1 a2 的话如果能在项和有良基关系的集合A的元素间建立起一个对应，那么可以利用它

45、去证明不存在无穷的归约序列M0 M1 M2 有几种方式可把项映射到有良基关系的集合1、利用项的语法特点2、利用代数的语义结构（下面用这种方式）第69页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统代数A = As1, As2, , f1A, f2A, 是良基的，若每个载体As上有一个良基关系s对每个n元函数符号f，如果x1 y1, , xn yn并且对某个i（1 i n）有xi yi，那么fA(x1, , xn) fA(y1, , yn)若A是良基代数，并且M和N都是类别s上的项，若M s N，则写成A, M N如果对任何环境都有A, M N，那么写成A M N第70

46、页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统定理2.22令R是项上的一个重写系统，并且令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) 各重写规则的左部定义的值都大于其右部定义的值第71页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统2.6.4 临界对局部合流 关

47、系是局部合流的，若N M P 蕴涵N P 局部合流关系严格弱于合流关系例a bb aa a0b b0a0abb0第72页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统cond B (cdr(cons s l) (cons(car l)(cdr l) )规则如下：cdr(cons x l) lcons(car l)(cdr l) l不相交的归约MSLSLMSRSLMSLSRMSRSR第73页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统cdr(cons x(cons(car l)(cdr l)规则如下：cdr(cons x l) lcons(c

48、ar l)(cdr l) l平凡的重迭SLSLSLSRSRSLSLSRSRSR第74页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统cdr(cons(car l)(cdr l)规则如下：cdr(cons x l) lcons(car l)(cdr l) l非平凡的重迭SLSLSLSRSR?第75页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统临界对L R cdr(cons x l) lL R cons(car l)(cdr l) l非平凡重迭是一个三元组SL，SL，m二元组SR，SR mSL叫做临界对该例有两个临界对第一个如下：SL是cdr(cons(car l)(cdr l)临界对是cdr l, cdr l第76页，共85页，2022年，5月20日，10点24分，星期四2.6 重写系统第二个如下：L R cons(car l)(cdr l) lL R cdr(cons x l) lSL是cons(car (cons x l)(cdr(cons x l)临界对是cons