欢迎来到三一文库! | 帮助中心 三一文库31doc.com 一个上传文档投稿赚钱的网站
三一文库
全部分类
  • 研究报告>
  • 工作总结>
  • 合同范本>
  • 心得体会>
  • 工作报告>
  • 党团相关>
  • 幼儿/小学教育>
  • 高等教育>
  • 经济/贸易/财会>
  • 建筑/环境>
  • 金融/证券>
  • 医学/心理学>
  • ImageVerifierCode 换一换
    首页 三一文库 > 资源分类 > PPT文档下载
     

    第3章泛代数和代数数据类型.ppt

    • 资源ID:2549653       资源大小:741.01KB        全文页数:83页
    • 资源格式: PPT        下载积分:8
    快捷下载 游客一键下载
    会员登录下载
    微信登录下载
    三方登录下载: 微信开放平台登录 QQ登录   微博登录  
    二维码
    微信扫一扫登录
    下载资源需要8
    邮箱/手机:
    温馨提示:
    用户名和密码都是您填写的邮箱或者手机号,方便查询和重复下载(系统自动生成)
    支付方式: 支付宝    微信支付   
    验证码:   换一换

    加入VIP免费专享
     
    账号:
    密码:
    验证码:   换一换
      忘记密码?
        
    友情提示
    2、PDF文件下载后,可能会被浏览器默认打开,此种情况可以点击浏览器菜单,保存网页到桌面,就可以正常下载了。
    3、本站不支持迅雷下载,请使用电脑自带的IE浏览器,或者360浏览器、谷歌浏览器下载即可。
    4、本站资源下载后的文档和图纸-无水印,预览文档经过压缩,下载后原文更清晰。
    5、试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓。

    第3章泛代数和代数数据类型.ppt

    第3章 泛代数和代数数据类型,PCF语言的三部分组成 带函数和积类型的纯类型化演算 自然数类型和布尔类型 不动点算子 第3章到第5章对这三部分进行透彻的研究 本章研究像自然数类型和布尔类型这样的代数数据类型,3.1 引 言,代数数据类型包括 一个或多个值集 一组在这些集合上的函数 基本限制是其函数不能有函数变元 基本“类型”符号被称为“类别” 泛代数(也叫做等式逻辑) 定义和研究代数数据类型的一般数学框架 本章研究泛代数和它在程序设计中定义常用数据类型时的作用,3.1 引 言,本章主要内容: 代数项和它们在多类别代数中的解释 等式规范(也叫代数规范)和等式证明系统 等式证明系统的可靠性和完备性(公理语义和指称语义的等价) 代数之间的同态关系和初始代数 数据类型的代数理论 从代数规范导出的重写规则(操作语义) 大多数逻辑系统中一些公共的议题将被覆盖,3.2 代数、基调和项,3.2.1 代数 代数 一个或多个集合,叫做载体 一组特征元素和一阶函数,也叫做代数函数 f : A1 Ak A 例:N N, 0, 1, +, 载体N是自然数集合 特征元素0, 1N,也叫做零元函数 函数+, : N N N,3.2 代数、基调和项,多个载体的例子 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是一个集合,其元素叫做类别 函数符号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 基调 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, 代数项中无约束变元,NxM就是简单地把M中x的每个出现都用N代替就是了 记号 , x : s x : s 引理 如果M Termss (, , x : s)并且N Termss(, ),那么NxM Termss (, ) 证明 按Termss(, )中项的结构进行归纳,3.2 代数、基调和项,例 用基调stk S, F来写自然数和栈表达式 sorts : nat, stack fctns : 0, 1, 2, : nat , : nat nat nat empty : stack push : nat stack stack pop : stack stack top : 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 ) 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 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 : s pop A(n : s) s pop A( ) top A(n : s) n top A( ) 0 A 若把x : nat映射到3A,把s : stack映射到2A,1A pop(push x s) popA(pushA( x ,s) ) popA(pushA(3A, 2A, 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), 那么M1 M2 证明 基于项结构的归纳,3.2 代数、基调和项,3.2.4 代换引理 引理 令M Termss (, , x : s)并且 N Termss(, ),那么NxMTermss(, )。并且对任何环境,有 NxM M(x a), 其中a N是N在下的含义 证明 根据项M的结构进行归纳,3.3 等式、可靠性和完备性,3.3.1 等式 代数规范:一个基调 + 一组等式 调查什么样的代数满足这些等式强加的要求 使用等式证明系统可推导新的等式 可靠性:从规范可证明的等式在任何满足该规范的代数中都成立 完备性:在满足规范的所有代数中都成立的等式都可从该规范证明 代数规范是描述代数数据类型公理语义的工具,3.3 等式、可靠性和完备性,空载体提出一个技术问题 逻辑公式 若A = ,则公式x:A. F(x) 为真 若A = ,则公式x:A. F(x) 为假 对任意的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都满足,写成 C M N 任何一个代数都满足等式M N,写成 M N (永真的、有效的 ),3.3 等式、可靠性和完备性,如果A满足上的所有等式,就说代数A是平凡的 例 令有两个类别a和b,令A是一个代数,其中Aa0,1并且Ab。 A不可能满足x yx : a, y : a,即下式不成立 A x yx : a, y : a 但是A x yx : a, y : a, z : b无意义地成立,3.3 等式、可靠性和完备性,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 u u a : u, b : u, c : u Tu 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 证明 对项进行归纳证明 从项代数可以知道,只有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是可证明的,那么E语义上蕴涵该等式 证明系统的完备性:如果E语义上蕴涵一个等式,那么该等式可从E证明 下面先给出代数证明系统,3.3 等式、可靠性和完备性,语义相等是个等价关系,因此有 M M 在等式中增加类别指派的规则 等价代换 P , Q Termss(, ),3.3 等式、可靠性和完备性,等式是可证明:如果从E中的等式和公理(ref)及推理规则(sym)、(trans)、(subst) 和(add var) 可以推出等式M N,那么就说该等式可证明,写成 E M N 语法理论 如果E M N蕴涵M N E E的语法理论Th(E) 从E可证明的所有等式的集合,3.3 等式、可靠性和完备性,等式集合E是语义一致的 如果存在某个等式M N,它不是E的语义蕴涵 等式集合E是语法一致的 如果存在某个等式M N,它不能由E证明,3.3 等式、可靠性和完备性,例 在基调stk S, F上增加等式 top (push x s ) = xs : stack, x : nat pop (push x s ) = ss : stack, x : nat 使用这些等式可以证明等式 top (push 3 empty ) = 3,3.3 等式、可靠性和完备性,导出规则 f : s1 sk s Mi, NiTermssi(, ) M和N中没有x,Termss(, )非空,3.3 等式、可靠性和完备性,定理(可靠性)如果E M N , 那么E M N 证明 可以根据该证明的长度进行归纳 归纳基础:长度为1的证明,它是公理或E的一个等式 归纳假设: M N的最后一步是从E1, , En得到。那么,如果A E,则A满足E1, , En 要证明:如果A满足最后一条规则的这些前提,那么A满足M N 证明 根据证明规则的集合,分情况进行分析,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 x : a E 可以找到一个使等式c = d 不成立的模型 由可靠性,c = d 是不可能从E证明的,3.3 等式、可靠性和完备性,例 栈代数规范 sorts : nat, stack fctns : 0, 1, 2, : nat +, : nat nat nat empty : stack 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,3.3 等式、可靠性和完备性,等式push (top s) (pop s) = ss : stack是不可证明的 任何形式为 top empty = M 的等式都是不可证明的,假定M是类别为nat的项,并且不含empty,3.3 等式、可靠性和完备性,3.3.4 完备性的形式 用于不同逻辑系统的三种形式的完备性 最弱的形式:所有的永真公式都是可证的 演绎完备性:每个语义蕴涵在证明系统中都是可推导的 最小模型完备性:每个语法理论是某一个“最小”模型的语义理论 对代数来说,最小模型完备性意味着每个语法理论是某个代数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 成立 E1和E2都不是E的语义蕴涵 不存在一个代数,其理论正好就是由E的等式推论组成的语法理论,3.3 等式、可靠性和完备性,3.3.5 同余、商和演绎完备性 同余关系:等价关系加上同余性 同余性:指函数保可证明的相等性 对单类代数A = A, f1A, f2A,,同余关系是载体A上的等价关系,使得对每个k元函数fA,如果aibi(i=1, k),即ai和bi等价,那么f A(a1, , ak ) fA (b1, , bk )。 对多类代数A = As, I ,同余关系是一簇等价关系 s, s AsAs,使得对每个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的一个元素 等价类a a a As a a 商代数A定义: (A)s是由As的所有等价类构成的集合 Ass as 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,上的同余关系“模k等价” 这个商代数是大家熟悉的整数模k加结构。如果k等于5,那么3 4 2,3.3 等式、可靠性和完备性,如果是A的一个环境,是一个同余关系,那么A的环境 定义如下: (x) = (x) 反过来,对于A的环境,对应它的A的环境有多种选择 引理 令是代数A上的同余关系,项MTerms(, )并且是满足的环境。那么项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 非空类别和最小模型性质 类别s非空:集合Termss(, )不是空集 对应的载体肯定非空 没有空载体时,可以增加推理规则(nonempty) 定理 令E是封闭于规则(nonempty)的语法理论,那么存在所有载体都非空的代数A,使得E Th (A) 没有空载体的代数有最小模型完备性,3.4 同态和初始性,3.4.1 同态和同构 将同态和同构的概念从单类代数推广到多类代数 同态是从一个代数到另一个代数的保结构的映射(或叫做翻译) 从代数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的等价关系。那么把nN映射到它的等价类n是从N到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 A(h (M1 ) h (Mk ) ),3.4 同态和初始性,引理 令h : A B是任意同态,并且是满足类别指派的任意A环境。那么对任何项M Terms(, ),有 h (AM) = BMh 当M中不含变量时,h (AM) =BM 证明 基于项的归纳 引理 如果h : A B和k : B C都是代数的同态,那么合成k h : A C也是代数的同态。 ( (k h)s = ks hs ) 同构 一个双射的同态, 写成A B,3.4 同态和初始性,3.4.2 初始代数 C是一类代数并且AC,若对每个BC,存在唯一的同态h : A B,那么A在C中叫做初始代数 初始代数是“典型”的 初始代数有尽可能少的非空载体 初始代数满足尽可能少的闭等式,3.4 同态和初始性,例 基调0 类别nat, 函数符号0 : nat和S : nat nat。 令C是所有0代数构成的代数类 闭项代数T Terms(0, )是C的初始代数 它的载体是所有闭项0, S (0), , S k(0), 该代数的函数S把Sk(0)映射到Sk1(0) 该代数的元素少到能解释所有的函数符号 该代数满足项之间尽可能少的等式,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中都成立 还要证明从A到任何满足E的代数有唯一的同态,3.4 同态和初始性,例 基调1:类别nat;函数符号0 : nat,S : nat nat和 : nat nat nat;等式集合E: x + 0 = x x + (Sy) = S (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,得一个初始代数 这个初始代数和该基调的标准模型(有后继算子和加法的自然数) 同构,3.4 同态和初始性,该规范的初始代数可以和其它有更多或较少元素的代数相对照 如果一个代数有更多元素的话,那么这些多余的元素不能由项定义。(有假货) 整数代数Z A = Anat, 0A, SA, +A Anat = (0 N) (1 Z) 0A = 0, 0 SAi, n = i, n +1 i, n +A j, m = max(i, j), n +m 如果一个代数有较少元素的话,那么就有一些不能被证明为相等的有区别的元素被等同。(出现混淆) 模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至少有两个元素) 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来说是初始代数。对任何等式M N,下面三个条件等价 A满足M N A满足M N的每一个基实例 M N的每一个基实例都可以从E证明,3.5 代数数据类型,3.5.1 代数数据类型 很多数据类型 不存在标准的数学构造 没有单一和标准的计算机实现 列出它们的操作并描述这些操作的行为 公理化地定义而不是由数学构造来定义 对于一个数据类型,是否可以断定有了“足够”的公理 本节讨论数据类型公理化方法的一般特征,3.5 代数数据类型,数据抽象的一般原理 抽象数据类型由它的规范定义。使用这样数据类型的程序应该只依赖于由它的规范保证的性质,而不依赖于它的任何特定实现 一个数据类型的函数可以划分成 构造算子:产生该数据类型的一个新元素 运算算子:是该数据类型上的函数,但不产生新的元素 观察算子:作用于该数据类型的元素,但返回某其它类型的元素,如自然数或布尔值,3.5 代数数据类型,3.5.2 初始代数语义和数据类型归纳 代数规范有几种不同的“语义”形式 宽松语义:满足一个代数规范的所有代数所构成的代数类 初始代数语义:满足一个代数规范的所有初始代数所构成的同构类 终结代数语义:满足一个代数规范的所有终结代数所构成的同构类 生成语义:满足一个代数规范的所有生成代数所构成的代数类,3.5 代数数据类型,初始代数的性质 没有假货 没有混淆 支持基于数据类型构造符的归纳 构造符集合 Spec , E的函数符号子集F0,使得Terms(,)E,的每个等价类正好只含一个由F0的函数符号所构成的基项 可以基于对构造符的归纳来证明初始代数的性质,3.5 代数数据类型,sorts: set, nat, bool 构造符、运算符、观察符 fctns: 0, 1, 2, : nat + : nat nat nat Eq? : nat nat nat true, false bool empty : set insert : nat set set union : set set set ismem? : 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) s = insert y (union s s) condn true x y = x condn false x y = y . . .,3.5 代数数据类型,终结代数 在一个代数类C中,如果从每个BC到AC,都存在唯一的同态,那么代数A是终结代数 一个代数类中的所有终结代数都同构 若用终结代数作为语义,则称之为终结语义 如果所有载体都是单元素集合的代数也在C中,则这个代数一定是C的终结代数,3.5 代数数据类型,初始语义和终结语义 初始语义:不能证明为相等的就是不相等的 终结语义:不能证明为不相等的则是相等的 如果把某些类别的解释固定,而其它类别的解释用终结语义,则它是一个有用的方法 从初始语义角度看,前面给出的不是集合的规范,而是表的规范。因为不能证明 insert x(insert y z)=insert y(insert x z) x: nat, y: nat, z: set insert x (insert x z) = insert x zx : nat, z : set 若用终结语义,且bool的解释固定,则为集合规范,3.5 代数数据类型,3.5.3 解释没有意义的项 表达式没有意义的情况 除法是一个部分函数,除数为零的表达式没意义 调用不终止的函数也构成一个没有意义的表达式 如果想在代数规范中表示这些情况,必须在基调中增加表示错误的项(简称错误值) 怎样规定这些项的值?有三种可能: 什么也不规定 任意做一个决定 非常仔细地说明什么是所需要的,3.6 重写系统,3.6.1 基本定义 重写系统:用于代数项的归约系统 两种重要的应用 为代数项提供一种计算模型 自动定理证明 由一组叫做重写规则(LR)的有向等式组成 限制:Var(R) Var(L) 由R 确定的一步归约关系R SLxM R SRxM 关系 R是R的自反传递闭包,3.6 重写系统,sorts : nat fctns : 0 : nat : nat nat + : nat nat nat 在这个基调上的一些归约规则如下: x 0 x x + (x) 0 (x y ) z x + (y + z) 实例:(x y ) (y) x + (y + (y) x 0 x,3.6 重写系统,引理(归约保类别 ) 令R是上的重写系统.如果M Termss (, ),并且M R N,那么N Termss (, ) 关系 (重写系统)是合流的,如果N M P蕴涵N P的话 关系 (重写系统)是终止的,如果不存在一步归约的无穷序列M0 M1 M2 不能再归约的项称为范式 合流并且终止的重写系统通常又叫做典范系统,3.6 重写系统,可变换性 如果存在M M1 M2 M3 Mk N 则项M, N Termss (, )是可变换的,写成 M R N 箭头的方向并没有什么意义 对任何重写系统,可变换性和可证明的相等性是一致的,3.6 重写系统,项中的一个位置:便于引用子项的某个特定出现 位置n = 1, 2的子项是hab 用M n表示M在位置n的子项 用N n M表示M在n的子项 由N代换的结果,3.6 重写系统,3.6.2 合流性和可证明的相等性 记号 如果R是一组重写规则,ER用来表示对应的无向的等式集合 定理 对任何重写系统R,MR N当且仅当ER M N 对任何合流的重写系统R,ER M N当且仅当M R R N,3.6 重写系统,3.6.3 终止性 良基关系:集合A上的一个关系是良基的,如果不存在A上元素的无穷递减序列a0 a1 a2 的话。 如果能在项和有良基关系的集合A的元素间建立起一个对应,那么可以利用它去证明不存在无穷的归约序列M0 M1 M2 有几种方式可把项映射到有良基关系的集合 利用代数的语义结构,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,那么写成A M N。,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 y x (y z) (x y) (x z) A(x) = 2x (y z) x (y x) (z x) 每条重写规则的左部定义的值都大于其右部定义的值,3.6 重写系统,3.6.4 临界对 局部合流 关系是局部合流的,如果N M P蕴涵N P 局部合流关系严格弱于合流关系 例 a b, b a a a0, b b0,3.6 重写系统,cond B (cdr(cons s l) (cons(car l)(cdr l) ) 规则如下: cdr(cons x l) l cons(car l)(cdr l) l 不相交的归约,3.6 重写系统,cdr(cons x(cons(car l)(cdr l) 规则如下: cdr(cons x l) l cons(car l)(cdr l) l 平凡的重迭,3.6 重写系统,cdr(cons(car l)(cdr l) 规则如下: cdr(cons x l) l cons(car l)(cdr l) l 非平凡的重迭,3.6 重写系统,临界对 L R cdr(cons x l) l L R cons(car l)(cdr l) l 非平凡重迭是一个三元组SL,SL,m 二元组SR,SR m SL叫做临界对 该例有两个临界对,第一个如下: SL是cdr(cons(car l)(cdr l) 临界对是cdr l, cdr l,3.6 重写系统,第二个如下: L R cons(car l)(cdr l) l L R cdr(cons x l) l SL是cons(car (cons x l)(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) a f (f (f x) 左部完全相同的情况:L R和L R,3.6 重写系统,命题 一个重写系统R是局部合流的,当且仅当对每个临界对M, N有M R R N 证明 从左到右的蕴涵是简单明了的 另一个方向的证明仿照用于启发临界对定义的推理:不相交、平凡的重迭、临界对的代换实例 如果一个有限的重写系统R是终止的,那么该命题就给出一个算法,可用于判定R是否局部合流,3.6 重写系统,3.6.5 左线性无重迭重写系统 无重迭:没有非平凡的临界对 无重迭的重写系统不一定是合流的 例如: S Eq ? x x true Eq ? x (S x) false Eq ? 有两个不同的范式 Eq ? true Eq ? Eq ? (S ) false,3.6 重写系统,左线性的规则:任何变量在规则的左部的出现不超过一次的话 左线性的系统:每一条规则都是左线性的 命题 如果R是左线性和无重迭的,那么R是合流的 例 下面是一个左线性无重迭重写系统 car (cons x l) x cdr (cons x l) l isempty? nil true isempty? (cons x l) false 加入非左线性规则cons (car l) (cdr l) l 后不合流 isempty? (cons (car l) (cdr l)有两个范式,3.6 重写系统,3.6.6 局部合流、终止和合流之间的联系 命题 令R是终止的重写系统,那么R是合流的当且仅当它是局部合流的 良基归纳 令是集合A上的一个良基关系, 令P是A上的某个性质。若每当 所有的P(b) (b a)为真则P(a)为真 (a. (b.( b a P(b) P(a) ), 那么,对所有的aA,P(a)为真。,3.6 重写系统,3.6.6 局部合流、终止和合流之间的联系 命题 令R是终止的重写系统,那么R是合流的当且仅当它是局部合流的 例 if true then x else y

    注意事项

    本文(第3章泛代数和代数数据类型.ppt)为本站会员(本田雅阁)主动上传,三一文库仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知三一文库(点击联系客服),我们立即给予删除!

    温馨提示:如果因为网速或其他原因下载失败请重新下载,重复下载不扣分。




    经营许可证编号:宁ICP备18001539号-1

    三一文库
    收起
    展开