《第3章泛代数和代数数据类型》由会员分享，可在线阅读，更多相关《第3章泛代数和代数数据类型（83页珍藏版）》请在金锄头文库上搜索。
1、第第3章章 泛代数和代数数据类型泛代数和代数数据类型PCF语言的三部分组成语言的三部分组成带函数和积类型的纯类型化带函数和积类型的纯类型化 演算演算自然数类型和布尔类型自然数类型和布尔类型不动点算子不动点算子第第3章到第章到第5章对章对这三这三部分进行透彻的研究部分进行透彻的研究本章研究像自然数类型和布尔类型这样的代数本章研究像自然数类型和布尔类型这样的代数数据类型数据类型催另什绩异跨子箍电频嚣临杨撅丽堪志顶堰翻眺涸攻襄掖壁膳钒癸诛盐竖第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.1 引引 言言代数数据类型代数数据类型包括包括一个或多个值集一个或多个值集一组在这些集合上的函数一组在这
2、些集合上的函数基本限制是其函数不能有函数变元基本限制是其函数不能有函数变元基本基本“类型类型”符号符号被称为被称为“类别类别”泛代数（也叫做等式逻辑）泛代数（也叫做等式逻辑）定义和研究代数数据类型的一般数学框架定义和研究代数数据类型的一般数学框架本章研究泛代数和它在程序设计中定义常用数本章研究泛代数和它在程序设计中定义常用数据类型时的作用据类型时的作用 婪相坎锰粕抿梭倦避执与闹础小寺挤航怠躬监椭驳涌寐虏铣乃槽谭破就纬第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.1 引引 言言本章主要内容：本章主要内容：代数项和它们在多类别代数中的解释代数项和它们在多类别代数中的解释等式规范（也叫代数
3、规范）和等式证明系统等式规范（也叫代数规范）和等式证明系统等等式式证证明明系系统统的的可可靠靠性性和和完完备备性性（公公理理语语义义和和指称语义的等价）指称语义的等价）代数之间的同态关系和初始代数代数之间的同态关系和初始代数数据类型的代数理论数据类型的代数理论从代数规范导出的重写规则（操作语义）从代数规范导出的重写规则（操作语义）大多数逻辑系统中一些公共的议题将被覆盖大多数逻辑系统中一些公共的议题将被覆盖垂饶吐霹冀戮徒熟奶叛偏晚挂虎砒脊旭耻酞全绅哟卒悠畦遇崭取碾档惨磕第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项3.2.1 代数代数代数代数一个或多个集
4、合一个或多个集合，叫做叫做载体载体一组特征元素和一组特征元素和一阶函数，也一阶函数，也叫做叫做代数函数代数函数f : A1 Ak A例例：N N, 0, 1, +, 载体载体N是自然数集合是自然数集合特征元素特征元素0, 1 N，也，也叫做零元函数叫做零元函数函数函数+, : N N N壮捏袱橙焉义挂淹婶码财皆供带制鲍列搁埂费颂蚕旷晓粥票弛劫欲涩债滤第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项多个载体的例子多个载体的例子Apcf N, B, 0, 1, , +, true, false, Eq ?, 下下面面开开始始逐逐步步给给出出代代数数的的一一种
5、种语语法法描描述述，有有穷穷的语法表示在计算机科学中十分重要的语法表示在计算机科学中十分重要定义数据类型定义数据类型证明性质证明性质进行化简进行化简还必须讨论这种语法描述的语义还必须讨论这种语法描述的语义A5pcf N5, B, 0, 1, 2, 3, 4, +5, true, false, Eq ?, 胯诲鸡篙锁簇斤独极坠疡憋汾踊晶怯鬃蹿去缩馒卯面亥暇许恫扔褪赔而慧第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项3.2.2 代数项的语法代数项的语法基调基调 S，F S是一个集合，其元素叫做是一个集合，其元素叫做类别类别函函数数符符号号f : s1 sk
6、 s的的集集合合F ，其其中中表表达达式式s1 sk s叫做类型叫做类型零元函数符号叫做常量符号零元函数符号叫做常量符号例例 N S，F sorts : natfctns : 0, 1 : nat , : nat nat nat 街卿驼毯哩絮眶绞金盲宏卷子颖凝脱神续翟挤怯咯句讹传究粮菊戈桶试问第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项定义基调的目的是用于写代数项定义基调的目的是用于写代数项考考虑虑项项中中有有变变量量的的情情况况，需需假假定定有有一一个个无无穷穷的的符号符号集合集合V，其元素称为其元素称为变量变量类别指派类别指派 x1 : s1,
7、, xk : sk 基基调调 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章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项例例0, 0 1 Termsnat ( N, )
8、0 x Termsnat ( N, )，其中，其中 x : nat, 代代数数项项中中无无约约束束变变元元， N x M就就是是简简单单地地把把M中中x的每个出现都用的每个出现都用N代替就是了代替就是了记号记号 , x : s x : s 引引理理 如如果果M Termss ( , , x : s )并并且且N Termss ( , )，那么，那么 N x M Termss ( , )证明证明 按按Termss( , )中项的结构进行归纳中项的结构进行归纳似炙破虚寄迁若乞稠懊历破店阎撒梆乔们抒绝升吉箱嚼集悟召租颜奸聘杜第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代
9、数、基调和项例例 用基调用基调 stk S, F 来写自然数和栈表达式来写自然数和栈表达式sorts : nat, stackfctns : 0, 1, 2, : nat , : nat nat natempty : stackpush : nat stack stackpop : stack stacktop : stack natpush 2 (push 1 (push 0 empty) )是该基调的项是该基调的项炬玫堪纺俩腿商热孪禾懂札羚谦蕾九养庭斧债帜里以疵蒸绩走复醒陷迁逐第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项3.2.3 代数以及项在代
10、数中的解释代数以及项在代数中的解释代数是为代数项提供含义的数学结构代数是为代数项提供含义的数学结构 是一个基调，则是一个基调，则 代数代数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章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数
11、、基调和项代数代数A的环境的环境 : V s As环境环境 满足满足 如果对每个如果对每个x : s 都有都有 (x) AsM Termss ( , )的含义的含义AM Ax (x)AM f A (AM1 , , AMk )若若f : s是常量符号，则是常量符号，则Af f AA清楚时，省略清楚时，省略A而直接写成而直接写成M 不依赖于不依赖于 时，时，用用AM表示表示M在在A中的含义中的含义炮刊字崭崎芯窝蘸蚕忌淮柱拜莆劳泊址截笨坞昼袭煞耸配殿分拙伤悼笔雪第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项例例 若若 (x) 0N x 1 N(x ,1 )
12、N ( (x), 1N) N (0N, 1N) 1N 疼居防瑰脱略里昏脂蔗礁迸骸仲飞我糟粒盈旱闷尺瓷侦杜诀漠嗡屈槐拒沤第3章泛代数和代数数据类型第3章泛代数和代数数据类型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
13、x s) popA(pushA( x ,s ) ) popA(pushA(3A, 2A, 1A ) ) popA( 3A, 2A, 1A ) 2A, 1A 硒摄亢禹义根睹侯帛岭诧伴铸流药疡谊员卸荔脑碴枕欢怂吹风棍择吻邀臻第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项引引理理 令令A是是一一个个 代代数数，M Termss ( , )，并且并且 是满足是满足 的环境，那么的环境，那么M As证明证明 根据根据Termss ( , )中项的结构进行归纳中项的结构进行归纳引引理理 令令x1, , xk是是由由出出现现在在M Termss ( , )中中的的所
14、所有有变变量量构构成成的的变变量量表表， 1和和 2是是满满足足 的的两两个个环环境境, 并并且且对对i 1, , k有有 1(xi) 2(xi), 那么那么M 1 M 2证明证明 基于项结构的归纳基于项结构的归纳恿衬漏梆沃灰畏循舜溉棕湿泣葫漫痹燃淤亡钨凉纶裸哆壁誊脱瞎数形学剧第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.2 代数、基调和项代数、基调和项3.2.4 代换引理代换引理引引理理 令令M Termss ( , , x : s )并并且且 N Termss ( , )，那那么么 N x M Termss( , )。并并且对任何环境且对任何环境 ，有，有 N x M M( x
15、a )，其中其中a N 是是N在在 下的含义下的含义证明证明 根据项根据项M的结构进行归纳的结构进行归纳沛酝蕉狸邻揍鼎绅匈择磺些能早澈蚊鱼冲相柬给番纽弛近识堆卢疹帚嫁吮第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.1 等式等式代数规范：一个代数规范：一个基调基调 + + 一组等式一组等式调查什么样的代数满足这些等式强加的要求调查什么样的代数满足这些等式强加的要求使用等式证明系统可推导新的等式使用等式证明系统可推导新的等式可可靠靠性性：从从规规范范可可证证明明的的等等式式在在任任何何满满足足该该规规范范的代数中都成立的代数中都成立完完
16、备备性性：在在满满足足规规范范的的所所有有代代数数中中都都成成立立的的等等式式都可从该规范证明都可从该规范证明代数规范是描述代数规范是描述代数数据类型公理语义的工具代数数据类型公理语义的工具眼阉瞩伯邯陕灌扑沤垃扔访果悬腾恼埂击篙伤砸支耀庸盒二褐平劳涪敞擂第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性空载体提出一个技术问题空载体提出一个技术问题逻辑公式逻辑公式若若A = ，则公式，则公式 x:A. F(x) 为真为真若若A = ，则公式，则公式 x:A. F(x) 为假为假对对任任意意的的M, N Termss ( , )，如如果果x : s
17、 且且As 为空，那么为空，那么M和和N看成是相等的项看成是相等的项只只有有一一个个类类别别时时，假假定定该该类类别别非非空空是是有有意意义义的的迁档寇刽竖辅黔沫灿舜列歼笼逆淋撅唇玛纵逸夯浇疚袒蜘照看辅翁锨迪陇第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性等式等式公式公式M N 对某个对某个s，M, N Termss ( , )如如果果 满满足足 ，那那么么若若M N ，就就说说代代数数A在环境在环境 下满足下满足M N，写成，写成A, M N若若A在任何环境下都满足，写成在任何环境下都满足，写成 A M N如果一类代数如果一类代数C中的任
18、何一个代数中的任何一个代数A都满足，写成都满足，写成 C M N任何一个任何一个 代数都满足等式代数都满足等式M N，写成，写成 M N(永真的、有效的永真的、有效的 )敲坠输蹬甩瞻贰畸旱瘟遂留撑把运蔫屑烃檬筛照涌亥澡俄饿瞳倦冤泛疼枚第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性如果如果A满足满足 上的所有等式，就说上的所有等式，就说 代数代数A是平凡的是平凡的例例令令 有有两两个个类类别别a和和b，令令A是是一一个个 代代数数，其其中中Aa 0,1并且并且Ab。A不可能满足不可能满足x yx : a, y : a，即下式，即下式不成立不成
19、立 A x yx : a, y : a但是但是A x yx : a, y : a, z : b无意义地无意义地成立成立 挪紧冀马茄拉袁嗓酶僵悔便睁睬郝啪厕熄挞买搅即潭异掳咸黄狰递张功贫第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.2 项代数项代数项代数项代数Terms( , )类别类别s的载体：的载体：集合集合Termss ( , )函数符号函数符号f : s1 sk s的解释的解释I (f ) (M1, , Mk) f M1 Mk项代数项代数Terms( , )的环境的环境 也叫做一个代换也叫做一个代换如如果果S是是代代换换，则则
20、用用SM表表示示同同时时把把M中中的的各各个个变变量量x用用Sx替换的结果替换的结果因此用因此用 M表示把代换表示把代换 作用于作用于M的结果的结果 蜘埠皆继衔旺伙奏焙诈譬鞭舔乍钵杉烯观顿闽芽穗数删啥钧赐属鼻盘裙夸第3章泛代数和代数数据类型第3章泛代数和代数数据类型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映射到映
21、射到a，把，把y映射到映射到f b，则，则T g(f x) (f y) g(f a) (f ( f b) )阉恫饶剖悉焊婪足港鲤锑肪亮歧并蛔整执兴毯树锭盖渺漓哈延鞍厚胃享筷第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性引引理理 令令M Terms( , )，并并且且 是是满满足足 的的项项代数代数Terms( , )的环境，那么的环境，那么M M证明证明 对项进行归纳证明对项进行归纳证明从从项项代代数数可可以以知知道道，只只有有M和和N是是语语法法上上相相同同的项时，等式的项时，等式M N才会永真才会永真袜妓浑砧辕冯墨常议礁渭推蛛怔趟埋排荚
22、矗嫩彝翅敬砂五浚矛八征孟尹菜第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性代代数数规规范范Spec , E : 一一个个基基调调 和和一一组组等等式式E语义蕴涵：语义蕴涵：E M N满足满足E的所有的所有 代数代数A都满足等式都满足等式M N语义理论语义理论：如果如果E M N蕴涵蕴涵M N E代数代数A的理论的理论Th(A)在在A中成立的所有等式的集合中成立的所有等式的集合这是一个这是一个语义理论语义理论丝含显燥轰考乏辫甸伏彩壳框炔牛熙垒哎找康性舞豌候渝建熄慷震枉真环第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性
23、和完备性等式、可靠性和完备性证证明明系系统统的的可可靠靠性性：若若一一个个等等式式从从一一组组假假设设E是可证明的，那么是可证明的，那么E语义上蕴涵该等式语义上蕴涵该等式证证明明系系统统的的完完备备性性：如如果果E语语义义上上蕴蕴涵涵一一个个等等式，那么该等式可从式，那么该等式可从E证明证明下面先给出代数证明系统下面先给出代数证明系统治诱昌雄葵堆僳枢孺豁肃蠢洪椽咸户河泻砚絮藻祟则瓶乏疾廖坪驹换愉续第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性语义相等是个等价关系语义相等是个等价关系，因此有，因此有M M在等式中增加类别指派在等式中增加类别指
24、派的规则的规则等价代换等价代换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 = P/x N 湿寒衅仰掌愈缀榔戈枣氮砷忠曰烙按澡俄热碾钙氦勤花歹勃些现挛都谜闷第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性等等式式是是可可证证明明：如如果果从从E中中的的等等式式和和公公理理(ref)及及推推理理规规则则(sym)、(trans)、(subst) 和和(add var) 可可以以推推出出等等式式M
25、N，那那么么就就说说该该等式可证明，写成等式可证明，写成E M N 语法理论语法理论如果如果E M N蕴涵蕴涵M N EE的语法理论的语法理论Th(E)从从E可证明的所有等式的集合可证明的所有等式的集合 苦倍蒂想滑喷沿访诡堆瞒理重浆沟惠则树痞昭澈燕皮舔检边魁仗憾涸亨纽第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性等式集合等式集合E是是语义一致的语义一致的如如果果存存在在某某个个等等式式M N，它它不不是是E的的语语义义蕴涵蕴涵等式集合等式集合E是是语法一致的语法一致的如果存在某个等式如果存在某个等式M N，它不能由，它不能由E证明证明 阳妖
26、展喜虞啦冲壶彝惺钝棍沾闪吓喝丸燕锋榨榜乡歧驹掷岁要哟渗卞人啃第3章泛代数和代数数据类型第3章泛代数和代数数据类型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 x : nat top(push x
27、 empty ) = xx : nat3 = 3 top(push 3 empty ) = 3 傀驴迂同喷两严奖雪克宋跑臆焙说琳禄咀互誓戎宫守警球右铲婿令赂铺量第3章泛代数和代数数据类型第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 简阎磋雨痢椰股只后祟荐醚绿低侨挟
28、调响碗鳖转厂翅省野轴钨扒靠尺惹贰第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性定理定理（可靠性可靠性）如果）如果E M N ， 那么那么E M N证明证明 可以根据该证明的长度进行归纳可以根据该证明的长度进行归纳归归纳纳基基础础：长长度度为为1的的证证明明，它它是是公公理理或或E的的一一个个等式等式归归纳纳假假设设： M N的的最最后后一一步步是是从从E1, , En得到得到。那么，。那么，如果如果A E，则，则A满足满足E1, , En要要证证明明：如如果果A满满足足最最后后一一条条规规则则的的这这些些前前提提，那么那么A满足满足M N证
29、明证明 根据证明规则的集合，分情况进行分析根据证明规则的集合，分情况进行分析枫捉莎磐羊汛腥岭檄壬镰居耘廊堂钢渊幽肆俱上仰坞躯泳椅虚痞剿婪瞳挝第3章泛代数和代数数据类型第3章泛代数和代数数据类型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
30、x : a E可以找到一个使等式可以找到一个使等式c = d 不成立不成立的的模型模型由可靠性，由可靠性，c = d 是不可能从是不可能从E证明的证明的使绘钮乘熙销惶维刑排腻委娘狈窄孜搪盒灭琉盖亡众悟嘶粱桥左卯糕醉能第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性例例 栈代数规范栈代数规范sorts : nat, stackfctns : 0, 1, 2, : nat +, : nat nat nat empty : stack push : nat stack stack pop : stack stack top : stack nate
31、qns : 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章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性等等式式push (top s) (pop s) = ss : stack是是不不可可证证明的明的任何形式为任何形式为top empty = M 的的等等式式都都是是不不可可证证明明的的，假假定定M是是类类别别为为nat的项，并且
32、不含的项，并且不含empty秧孵蚁殴奴岸沥迪棵拷担波堕轿鸿纺谍迸踏贤下怀秀峡围捏婴殿为通钉伴第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.4 完备性的形式完备性的形式用于不同逻辑系统的三种形式的完备性用于不同逻辑系统的三种形式的完备性最弱的形式：所有的永真公式都是可证的最弱的形式：所有的永真公式都是可证的演演绎绎完完备备性性：每每个个语语义义蕴蕴涵涵在在证证明明系系统统中中都都是可推导的是可推导的最最小小模模型型完完备备性性：每每个个语语法法理理论论是是某某一一个个“最小最小”模型的语义理论模型的语义理论对对代代数数来来说说，最最小
33、小模模型型完完备备性性意意味味着着每每个个语语法法理理论是某个代数论是某个代数A的的Th(A)“最小模型最小模型”是指它的理论包含的内容最少是指它的理论包含的内容最少攒程租下趋拈婉核注筒壕末讯哨汇肩疽徊染剑化见哪出鸦钞碱馁耽设幢豺第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性最小模型完备性不一定成立，最小模型完备性不一定成立，考虑等式考虑等式E =def x = y x : a, y : a, z : b 情况情况1：a的载体只含一个元素的载体只含一个元素，则，则E满足，此时满足，此时E1 =def x = y x : a, y : a 成
34、立成立 情况情况2： b的载体为空的载体为空，则，则E也也满足，此时满足，此时E2 =def z = w z : b, w : b 成立成立E1和和E2都不是都不是E的语义蕴涵的语义蕴涵不不存存在在一一个个代代数数，其其理理论论正正好好就就是是由由E的的等等式式推推论组成的语法理论论组成的语法理论 乳来迁燕算萤坝扑靛巍劝劣班辟俗垣成炬煮艰燎纶杖秦敛扰昆故襟个备转第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.5 同余、商和演绎完备性同余、商和演绎完备性同余关系同余关系：等价关系加上同余性：等价关系加上同余性同余性：指函数保可证明的相等
35、同余性：指函数保可证明的相等性性对对单单类类代代数数A = A, f1A, f2A, ，同同余余关关系系是是载载体体A上上的的等等价价关关系系，使使得得对对每每个个k元元函函数数fA，如如果果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 )
36、 s f A (b1, , bk )详自奉酶馈频祟茸乘缎忠胎扶咯巳统烂携馈累堂着盲鸵痕兄澄逗产亢僚讫第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性A模模 的商的代数的商的代数A把把A中中有有关关系系的的元元素素a a 压压缩缩成成A的的一一个个元元素素等价类等价类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
37、)轿嫌短澡浸锐捎馆薪衬避位趣新户妈毁复铣慎祭钢杂络赏骚权愉绦垣芍没第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性上上面面定定义义有有意意义义的的条条件件是是f A (a1, , ak)必必须须只只依依赖赖于于a1, , ak，而而不不能能依依赖赖于于所所选的代表选的代表a1, , ak。例例 单单类类别别代代数数 N，0，1，上上的的同同余余关关系系“模模k等价等价”这这个个商商代代数数是是大大家家熟熟悉悉的的整整数数模模k加加结结构构。如如果果k等于等于5，那么，那么 3 4 2 棚匹迹役石测啦鲸千添琅党滔没貉荤吟抱智临龋刻俺挥叼闹堰爷嗣
38、筋抛蒋第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性如如果果 是是A的的一一个个环环境境， 是是一一个个同同余余关关系系，那那么么A的环境的环境 定义如下：定义如下： (x) = (x) 反反过过来来，对对于于A的的环环境境 ，对对应应它它的的A的的环境环境 有多种选择有多种选择引引 理理 令令 是是 代代 数数 A上上 的的 同同 余余 关关 系系 ， 项项M Terms( , )并并且且 是是满满足足 的的环环境境。那那么么项项 M在在 商商 代代 数数 A 和和 环环 境境 下下 的的 含含 义义(A)M 由下式决定由下式决定(A)M
39、 = AM 泳严都幢涩放邹费跟等走猿搀抠操菠烁倾眷撅土斟峦丁奉荣流栋垒粱孕触第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性引引理理 令令E是是一一组组 等等式式集集合合，令令Terms( , )是是基基调调 上上的的项项集集。由由E的的可可证证明明性性确确定定的的关关系系 E, 是是Terms( , )上的同余关系上的同余关系定理定理（ 完备性完备性）如果）如果E M N ， 那么那么E M N完完备备性性定定理理加加上上可可靠靠性性定定理理表表明明语语法法理理论论和和语义理论相同语义理论相同舶替赐镀凭宿喜拓棠栏咨辱橙笺京苑贵式稳愉实爆瓜康
40、责朴绸操弃舍端蔽第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.3 等式、可靠性和完备性等式、可靠性和完备性3.3.6 非空类别和最小模型性质非空类别和最小模型性质类别类别s非空：集合非空：集合Termss( , )不是空集不是空集对应的载体肯定非空对应的载体肯定非空没没 有有 空空 载载 体体 时时 ， 可可 以以 增增 加加 推推 理理 规规 则则(nonempty)定定理理 令令E是是封封闭闭于于规规则则（nonempty）的的语语法法理理论论，那那么么存存在在所所有有载载体体都都非非空空的的代代数数A，使使得得E Th (A) 没有空载体的代数有最小模型完备性没有空载体的代数有
41、最小模型完备性M = N , x : s M = N 渴栗纳呀免氰廖馁暴弦排赌笑晚未懦酚挽参宋肮迸航锭沥狮市帧互程刷呕第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.4 同态和初始性同态和初始性3.4.1 同态和同构同态和同构将将同同态态和和同同构构的的概概念念从从单单类类代代数数推推广广到到多多类类代数代数 同同态态是是从从一一个个代代数数到到另另一一个个代代数数的的保保结结构构的的映射（或叫做翻译）映射（或叫做翻译）从从 代数代数A到到B的同态的同态h : A B一一簇簇映映射射h = hs | s S ，使使得得对对 的的每每个个函函数数符符号号f : s1 sk s，有，有hs
42、 (f A (a1, , ak) ) = (f B (hs1a1, , hskak) )耗侠八定灿凶偶漂厄笑前厨冈程拳房稀氮骨念骆恼酥完糠凑蒲开惑刺锯瞒第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.4 同态和初始性同态和初始性例例 令令N = N, 0, 1, ，令令 是是模模k的的等等价价关关系系。那那么么把把n N映映射射到到它它的的等等价价类类n 是是从从N到到N的一个同态，因为的一个同态，因为h (0) = 0N = 0 h (n + m) = h (n) N h (m) = n + m 任任何何代代数数到到它它商商代代数数的的同同态态都都用用这这种种方方式式定定义义灯启毋庞
43、烤暮借囱余垮磐裴清模婪稀烷跪突间默死搬室罩啤伸袜音迹沸弹第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.4 同态和初始性同态和初始性例例 含含义义函函数数是是从从项项代代数数T = Terms( , )到到任任意意代代数数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
44、章泛代数和代数数据类型第3章泛代数和代数数据类型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) 同构同构 一个双射的同态一个双射的同态, 写成
45、写成A B荡篮堪忘啄插蹬解嗣烧嚼倾暴恳钮买蛔涯在亥数罚圭擎火候哗碗蠕辜系历第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.4 同态和初始性同态和初始性3.4.2 初始代数初始代数C是是一一类类 代代数数并并且且A C，若若对对每每个个B C，存存在在唯唯一一的的同同态态h : A B，那那么么A在在C中中叫叫做做初始代数初始代数初始代数是初始代数是“典型典型”的的初始代数有尽可能少的非空载体初始代数有尽可能少的非空载体初始代数满足尽可能少的闭等式初始代数满足尽可能少的闭等式AB3B2B1詹林批惜池恿嫡录妮光呜谴靴尾奎菏品偿饥妨渤厢放失郭檄揍防嵌拖焚爽第3章泛代数和代数数据类型第3章泛代
46、数和代数数据类型3.4 同态和初始性同态和初始性例例 基调基调 0类别类别nat，函数符号函数符号0 : nat和和S : nat nat。令令C是所有是所有 0代数构成的代数类代数构成的代数类闭项代数闭项代数T Terms( 0, )是是C的初始代数的初始代数它的载体是所有闭项它的载体是所有闭项0, S (0), , S k(0), 该代数的函数该代数的函数S把把Sk(0)映射到映射到Sk 1(0)该代数的元素少到能解释所有的函数符号该代数的元素少到能解释所有的函数符号该代数满足项之间尽可能少的等式该代数满足项之间尽可能少的等式际硝氯治留勺婿八酷帐翻吗茶漏汇端霓剧辱阮纸霜迟尼富承史詹佐雁煮锋
47、第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.4 同态和初始性同态和初始性引引理理 假假定定h : A B和和k : B A都都是是同同态态，并并且且h k=IdB，k h =IdA。那么。那么A和和B同构同构命命题题 如如果果A和和B在在代代数数类类C中中都都是是初初始始代代数数，那么那么A和和B是同构的是同构的命命题题 令令E是是一一组组 等等式式，并并且且令令A = Terms( , )E, 是是模模可可证证明明的的相相等等性性的的代代数数。那那么么，A对对E来说是初始代数来说是初始代数由由项项代代数数和和商商的的性性质质可可知知，从从E可可证证明明的的等等式式在在A中都成立中
48、都成立还要证明从还要证明从A到任何满足到任何满足E的代数有唯一的同态的代数有唯一的同态筒帛殴衍超皿谅翁龟印绒泻瘫芜挣药殆眶琶碟撂酪桅蛙访卤妆胆侩聊冒滩第3章泛代数和代数数据类型第3章泛代数和代数数据类型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是不可证明的，除
49、非是不可证明的，除非k = l每个等价类正好包含一个形式为每个等价类正好包含一个形式为Sk0的项的项等价类和形式为等价类和形式为Sk0的项集间有一个双射的项集间有一个双射载载体体看看成成由由闭闭项项0, S0, , Sk0, 构构成成的的集集合合，函函数数S映映射射Sk0 Sk10， 映射映射(Sk0, Sl0) Skl0，得一个初始代数，得一个初始代数这这个个初初始始代代数数和和该该基基调调的的标标准准模模型型（有有后后继继算算子子和和加加法法的的自然数）自然数） 同构同构号涡最则渗漂够倪连谜泪厨薪逆砧潞味耗环式临脓三血婚彰水巫伙肃颈阵第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.
50、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 如如果果一一个个代代数数有有较较少少元元素素的的话话，那那么么就就有有一一些些不不能能被被证证明明为相等的有区
51、别的元素被等同。（出现混淆）为相等的有区别的元素被等同。（出现混淆）模模k的自然数的自然数录俊艾坎虏错耽硷缕掳些勤箩程讫蘸兽染秋嘲胯晕柄梁鸟跟完材岁瓶摈晌第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.4 同态和初始性同态和初始性初始代数可能满足不能由初始代数可能满足不能由E证明的额外的等式证明的额外的等式例例 上面的自然数基调例子中，初始代数满足上面的自然数基调例子中，初始代数满足等式等式x + y = y + x 因为因为 E M = Sk0和和E N = Sl0 蕴涵蕴涵 E M + N = Sk+l0 = N + M不满足交换性的代数不满足交换性的代数Anat是所有是所有f :
52、 X X的函数的集合（的函数的集合（X至少有两个元素至少有两个元素）0A是是X上的恒等函数，上的恒等函数，SA是是Anat上的恒等映射上的恒等映射+A是是Anat上的函数合成上的函数合成A = Anat 0A SA +A 满足满足E+A没有交换性，因为函数合成没有交换性没有交换性，因为函数合成没有交换性桂断馈管蓟桅帆菩红这锡鹏堑入昏赐慈共哮已蓉墒啊坟弗卜柱坦己猿克驹第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.4 同态和初始性同态和初始性基项、基代换、基实例（项、等式）基项、基代换、基实例（项、等式）如如果果M N是是Termss( , )的的项项之之间间的的等等式式，并并 且且 S
53、是是 一一 个个 ， 基基 代代 换换 ， 那那 么么 就就 把把 SM SN称为称为M N的的基实例基实例命命题题 令令E是是一一组组 等等式式，并并且且A对对E来来说说是是初初始始代代数数。对对任任何何 等等式式M N，下下面面三三个个条件等价条件等价 A满足满足M NA满足满足M N的每一个基实例的每一个基实例M N的每一个基实例都可以从的每一个基实例都可以从E证明证明督砧遗炭稚巢僵幼埃欠唆帽听右鞭弹供汇采填界挥乙缘靠仿耀液需搀貌患第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.5 代数数据类型代数数据类型3.5.1 代数数据类型代数数据类型很多数据类型很多数据类型不存在标准的数
54、学构造不存在标准的数学构造没有单一和标准的计算机实现没有单一和标准的计算机实现列出它们的操作并描述这些操作的行为列出它们的操作并描述这些操作的行为公理化地定义而不是由数学构造来定义公理化地定义而不是由数学构造来定义对对于于一一个个数数据据类类型型，是是否否可可以以断断定定有有了了“足足够够”的公理的公理本节讨论数据类型公理化方法的一般特征本节讨论数据类型公理化方法的一般特征践崭斜呢艰赠塞奖尺碘藐滑耿咏筐疆窿棍沁赖胸鲍个署馏酗辟幸暑半淮柑第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.5 代数数据类型代数数据类型数据抽象的一般原理数据抽象的一般原理抽抽象象数数据据类类型型由由它它的的规规
55、范范定定义义。使使用用这这样样数数据据类类型型的的程程序序应应该该只只依依赖赖于于由由它它的的规规范范保保证证的的性性质质，而不依赖于它的任何特定实现而不依赖于它的任何特定实现一个数据类型的函数可以划分成一个数据类型的函数可以划分成构造算子：产生该数据类型的一个新元素构造算子：产生该数据类型的一个新元素运运算算算算子子：是是该该数数据据类类型型上上的的函函数数，但但不不产产生生新新的元素的元素观观察察算算子子：作作用用于于该该数数据据类类型型的的元元素素，但但返返回回某某其它类型的元素，如自然数或布尔值其它类型的元素，如自然数或布尔值犁泌颓侨瑚吁捅钥溅酉毙答枫鸿邵召孔颂昆储慌片眺贤葬恋戒厉瘦粒
56、碉诬第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.5 代数数据类型代数数据类型3.5.2 初始代数语义和数据类型归纳初始代数语义和数据类型归纳代数规范有几种不同的代数规范有几种不同的“语义语义”形式形式宽宽松松语语义义：满满足足一一个个代代数数规规范范的的所所有有代代数数所所构构成成的代数类的代数类初初始始代代数数语语义义：满满足足一一个个代代数数规规范范的的所所有有初初始始代代数所构成的同构类数所构成的同构类终终结结代代数数语语义义：满满足足一一个个代代数数规规范范的的所所有有终终结结代代数所构成的同构类数所构成的同构类生生成成语语义义：满满足足一一个个代代数数规规范范的的所所有有
57、生生成成代代数数所所构成的代数类构成的代数类缀寞盟约振皋正倒噪邀蜂晦惰需醛宜腮等寇资袭煌蔫总陌绰组潞膀颁僧笋第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.5 代数数据类型代数数据类型初始代数的性质初始代数的性质没有假货没有假货没有混淆没有混淆支持基于数据类型构造符的归纳支持基于数据类型构造符的归纳构造符集合构造符集合Spec , E 的的 函函 数数 符符 号号 子子 集集 F0， 使使 得得Terms( ,)E,的的每每个个等等价价类类正正好好只只含含一一个个由由F0的函数符号所构成的基项的函数符号所构成的基项可以基于对构造符的归纳来证明初始代数的性质可以基于对构造符的归纳来证明初
58、始代数的性质足饼忆一厦筏领蹬萎核盅蚂民烙珊衍氯瞄挞嘘硷栖扇汛挖中佣油环摸祭梢第3章泛代数和代数数据类型第3章泛代数和代数数据类型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
59、: 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) s = insert y (union s s ) condn true x y = x cond
60、n false x y = y . . .耪脾济淑酵淡疹阀按孝伎投泞梦捻名筏敞杨用沾度虫盘踩砖袍复辛陆颖寡第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.5 代数数据类型代数数据类型终结代数终结代数在在一一个个代代数数类类C中中，如如果果从从每每个个B C到到A C，都都存在唯一的同态，那么代数存在唯一的同态，那么代数A是终结代数是终结代数一个代数类中的所有终结代数都同构一个代数类中的所有终结代数都同构若用终结代数作为语义，则称之为终结语义若用终结代数作为语义，则称之为终结语义如如果果所所有有载载体体都都是是单单元元素素集集合合的的代代数数也也在在C中中，则这个代数一定是则这个代数一定
61、是C的终结代数的终结代数妆睁酮钩绞唱毒惦芒俩雅林畜合阶描诌刘羡旺逢惟奴蚕膏序彤守湍绸焰焰第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.5 代数数据类型代数数据类型初始语义和终结语义初始语义和终结语义初始语义初始语义：不能证明为相等的就是不相等的不能证明为相等的就是不相等的终结语义终结语义：不能证明为不相等的则是相等的不能证明为不相等的则是相等的如如果果把把某某些些类类别别的的解解释释固固定定，而而其其它它类类别别的的解解释释用终结语义，则它是一个有用的方法用终结语义，则它是一个有用的方法从从初初始始语语义义角角度度看看，前前面面给给出出的的不不是是集集合合的的规规范范,而是表的规范。
62、因为不能证明而是表的规范。因为不能证明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章泛代数和代数数据类型第3章泛代数和代数数据类型3.5 代数数据类型代数数据类型3.5.3 解释没有意义的项解释没有意义的项表达式没有意义的情况表达式没有意义的情况除法是一个部
63、分函数，除数为零的表达式没意义除法是一个部分函数，除数为零的表达式没意义调用不终止的函数也构成一个没有意义的表达式调用不终止的函数也构成一个没有意义的表达式如如果果想想在在代代数数规规范范中中表表示示这这些些情情况况，必必须须在在基基调调中增加表示错误的项（简称错误值）中增加表示错误的项（简称错误值）怎样规定这些项的值？有三种可能：怎样规定这些项的值？有三种可能：什么也不规定什么也不规定任意做一个决定任意做一个决定非常仔细地说明什么是所需要的非常仔细地说明什么是所需要的臼第冯凸道组辩敲溢帛眩拌膘者敝萤劝屿寐钢设摘矾辉坍独谋屏烂婆咬钢第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重
64、写系统重写系统3.6.1 基本定义基本定义重写系统：用于代数项的归约系统重写系统：用于代数项的归约系统两种重要的应用两种重要的应用为代数项提供一种计算模型为代数项提供一种计算模型自动定理证明自动定理证明由一组叫做重写规则由一组叫做重写规则( (LR) )的有向等式组成的有向等式组成限制：限制：Var(R) Var(L)由由R R 确定的一步归约关系确定的一步归约关系RSL xM R SR x M关系关系 R是是R的自反传递闭包的自反传递闭包迈阁谊友畔浓橱囚呐睁烙粕仍楷项陶琶珊杖所恨校饰盒相犹唇恩疥壕犁蹄第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统sorts :
65、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 宵配壕诈刷社驮犀惑浆崭练蜂瞻蹬判摘亨赵雇完潍噬逢隘币蕾我偶恼娟站第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统引引理理（归归约约保保类类别别 ） 令令R R是是 上上的的重重写写系系统统. .如如果果M Termss ( , )，并并且且M R N，那那么么N Terms
66、s ( , ) 关关系系 （重重写写系系统统）是是合合流流的的，如如果果N M P蕴涵蕴涵N P的话的话关关系系 （重重写写系系统统）是是终终止止的的，如如果果不不存存在在一步归约的无穷序列一步归约的无穷序列M0 M1 M2不能再归约的项称为不能再归约的项称为范式范式合合流流并并且且终终止止的的重重写写系系统统通通常常又又叫叫做做典典范范系系统统卯雄华跺神堪驴氰寞二尽忱戒缔班代烟裳戎闽谆诱肛驳惕贝鳃痔参蛔盅厅第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统可变换性可变换性 如果存在如果存在M M1 M2 M3 Mk N 则项则项M, N Termss ( , )是是
67、可变换的，写成可变换的，写成M R N箭头的方向并没有什么意义箭头的方向并没有什么意义对对任任何何重重写写系系统统，可可变变换换性性和和可可证证明明的的相相等等性性是是一致的一致的蜕舰栓耳使唉狄磋束展肾紧陌卢祸账酋嘘氦跑权怕挣揭疽裕剖金呈难龋疏第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统项项中中的的一一个个位位置置：便便于于引引用用子子项项的的某某个个特特定定出现出现位置位置n = 1, 2的子项是的子项是hab用用M n表示表示M在在位置位置n的子项的子项用用 N n M表示表示M在在n的子项的子项由由N代换的结果代换的结果fggxxhababf (gx(ha
68、b)(gba) x贾露炭蜜烤手君众养舞昨赢汽祟泞白狸裁阔肖奔晒翔毛迈酸忽闻死疏舌衬第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统3.6.2 合流性和可证明的相等性合流性和可证明的相等性记记号号 如如果果R是是一一组组重重写写规规则则，ER用用来来表表示示对对应应的的无向的等式集合无向的等式集合定定理理 对对任任何何重重写写系系统统R，MR N当当且且仅仅当当ER M N对对任任何何合合流流的的重重写写系系统统R，ER M N当且仅当当且仅当M R R N 绩敦召峰典豌慧眷秘拒娇枷斑拴陇缆腹肘若夫帖普伐触逐互继秉相乒元憨第3章泛代数和代数数据类型第3章泛代数和代数数
69、据类型3.6 重写系统重写系统3.6.3 终止性终止性良良基基关关系系：集集合合A上上的的一一个个关关系系是是良良基基的的，如如果果不不存存在在A上上元元素素的的无无穷穷递递减减序序列列a0 a1 a2 的话。的话。如如果果能能在在项项和和有有良良基基关关系系的的集集合合A的的元元素素间间建建立立起起一一个个对对应应，那那么么可可以以利利用用它它去去证证明明不不存存在无穷的归约序列在无穷的归约序列M0 M1 M2 有几种方式可把项映射到有良基关系的集合有几种方式可把项映射到有良基关系的集合利用代数的语义结构利用代数的语义结构济模蔬肛牢悦午键栖促蚊辨更曾荐众颂喉浓拷舍绅培袱矩碳总靳借锈魏合第3章
70、泛代数和代数数据类型第3章泛代数和代数数据类型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，那那么么
71、写写成成A M N。 啪司孟廖诡吱统赣误棋高散稻藐横泼拉级尊朋兜悲谈腑坪则逃或诉凡拜刚第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统定定理理 令令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 (
72、y x) (z x) 每条重写规则的左部定义的值都大于其右部定义的值每条重写规则的左部定义的值都大于其右部定义的值 贺寿狱朋结掐韧剪戳羹吾黍咽瓶搪乙巴荧琴贺踏泞缀勾炯厕来县针问赖洱第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统3.6.4 临界对临界对局部合流局部合流关关系系是是局局部部合合流流的的，如如果果N M P蕴涵蕴涵N P 局部合流关系严格弱于合流关系局部合流关系严格弱于合流关系例例a b, b aa a0, b b0a0abb0肖篆浅夹耻诲遁诱妨灼坏措私逢翼缎佑根极券子齐乍良猿恭规藤詹禄耙驶第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写
73、系统重写系统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章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统cdr(cons x(cons(car l )(cdr l )规则如下：规则如下：cdr(cons x l) lcons(car l )(cdr l ) l 平凡的重迭平凡的重迭SLSL S
74、LSR SRSL SL SRSR SR 贼祟聪施贪菊摘苫愧痊焉茅莽方梧窃鲸掀晴牌酣野乎庭河脾惑断磊渐济饯第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统cdr(cons(car l )(cdr l )规则如下：规则如下：cdr(cons x l) lcons(car l )(cdr l ) l 非平凡的重迭非平凡的重迭SLSL SLSR SR?祈否欢诉玫诣瓶胸江钡醋何越坐劳丑皖撬梭危仰脓芭渊乡贪浆轧其政广埂第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统临界对临界对L R cdr(cons x l) lL R cons(car l )(c
75、dr l ) l 非平凡重迭是一个三元组非平凡重迭是一个三元组 SL，SL ，m 二元组二元组 SR， SR m SL 叫做叫做临界对临界对该例有两个临界对，第一个如下：该例有两个临界对，第一个如下：SL是是cdr(cons(car l)(cdr l)临界对是临界对是 cdr l, cdr l 它心肘骏兵倘务疡誓响眨绪掐市保绊铁屠分受撩充患寝喻分杰逻遏旋滨啊第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统第二个如下：第二个如下：L R cons(car l )(cdr l ) l L R cdr(cons x l) lSL是是cons(car (cons x l)(
76、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章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统命命题题 一一个个重重写写系系统统R是是局局部
77、部合合流流的的，当当且且仅仅当当对对每个临界对每个临界对 M, N 有有M R R N证明证明从左到右的蕴涵是简单明了的从左到右的蕴涵是简单明了的另另一一个个方方向向的的证证明明仿仿照照用用于于启启发发临临界界对对定定义义的的推推理：不相交、平凡的重迭、临界对的代换实例理：不相交、平凡的重迭、临界对的代换实例如如果果一一个个有有限限的的重重写写系系统统R是是终终止止的的，那那么么该该命命题题就就给给出出一一个个算算法法，可可用用于于判判定定R是是否否局局部部合流合流苟叛雇抖崎杏蹈也试斡端醛婚汽级助贪惭渡寸姑乡毋辈胚瞒叠码人雇猿钥第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系
78、统重写系统3.6.5 左线性无重迭重写系统左线性无重迭重写系统无重迭：没有非平凡的临界对无重迭：没有非平凡的临界对无重迭的重写系统不一定是合流的无重迭的重写系统不一定是合流的例如：例如： S Eq ? x x trueEq ? x (S x) falseEq ? 有两个不同的范式有两个不同的范式Eq ? trueEq ? Eq ? (S ) false旭妖仿暗馈浑鼠街团赁韦秀毯糟忿靴绿挣应氨筛铆剔村催鸵喂崎爆忽戮遍第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统左左线线性性的的规规则则：任任何何变变量量在在规规则则的的左左部部的的出出现不超过一次的话现不超过一次的话
79、左线性的系统：左线性的系统：每一条规则都是左线性的每一条规则都是左线性的命命题题 如如果果R是是左左线线性性和和无无重重迭迭的的，那那么么R是合流的是合流的例例 下面是一个下面是一个左线性无重迭重写系统左线性无重迭重写系统car (cons x l) xcdr (cons x l) lisempty? nil trueisempty? (cons x l) false 加入非左线性规则加入非左线性规则cons (car l) (cdr l) l 后不合流后不合流isempty? (cons (car l) (cdr l)有两个范式有两个范式斗酱丈肃抗把培唉侗且钥怀园诣烯炭镐痔槛镶支迪攻改吹位滔
80、茵债奸气踊第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统3.6.6 局部合流、终止和合流之间的联系局部合流、终止和合流之间的联系命命题题 令令R是是终终止止的的重重写写系系统统，那那么么R是是合合流流的的当当且仅当它是局部合流的且仅当它是局部合流的良基归纳良基归纳 令令是集合是集合A上的一个良基关系，上的一个良基关系，令令P是是A上的某个性质。若每当上的某个性质。若每当所有的所有的P(b) (b a)为真则为真则P(a)为真为真( a. . ( b.(.( b a P(b) P(a) )，那么，对所有的那么，对所有的a A，P(a)为真。为真。MN1P1QNRSP
81、裴活逃头眶起缝振瘴芍绞儒椰谋龋搐否终纹首醚语眨十匪雪痪摘持重罢陕第3章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统3.6.6 局部合流、终止和合流之间的联系局部合流、终止和合流之间的联系命命题题 令令R是是终终止止的的重重写写系系统统，那那么么R是是合合流流的的当当且仅当它是局部合流的且仅当它是局部合流的例例if true then x else y xif false then x else y yif u then x else x xMN1P1QNRSP我士雅吃笑稠砰巷屡桩罚婉责虏哩器佑财玖混净悍腑凭袭帝峭舵享俐增存第3章泛代数和代数数据类型第3章泛代数和代数数
82、据类型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章泛代数和代数数据类型第3章泛代数和代数数据类型3.6 重写系统重写系统产生一个临界对产生一个临界对 f (x + y) + z, f x +
83、 (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章泛代数和代数数据类型习习 题题 第一次：第一次：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爆箔嘻瞅伟拎凉压摈崎蓟漾琴若弘碴管禽怔茬菊缓袒埋激矮拒祥华暖敬三第3章泛代数和代数数据类型第3章泛代数和代数数据类型
