第2章 泛代数和代数数据类型 函数式程序设计语言PCF由三部分组成 第2章到第4章对这三部分进行透彻的研究

Presentation on theme: "第2章 泛代数和代数数据类型 函数式程序设计语言PCF由三部分组成 第2章到第4章对这三部分进行透彻的研究"— Presentation transcript:

1 第2章 泛代数和代数数据类型 函数式程序设计语言PCF由三部分组成 第2章到第4章对这三部分进行透彻的研究
第2章 泛代数和代数数据类型 函数式程序设计语言PCF由三部分组成 代数数据类型：自然数类型和布尔类型 带函数和积等类型的纯类型化演算 不动点算子 第2章到第4章对这三部分进行透彻的研究 本章研究像自然数类型和布尔类型这样的代数数据类型

2 2.1 引 言 代数数据类型包括 泛代数（也叫做等式逻辑） 一个或多个值集 一组在这些集合上的函数 基本限制是其函数不能有函数变元
2.1 引 言 代数数据类型包括 一个或多个值集 一组在这些集合上的函数 基本限制是其函数不能有函数变元 基本“类型”(type)符号被称为“类别” (sort) 泛代数（也叫做等式逻辑） 定义和研究代数数据类型的一般数学框架 本章研究泛代数和它在程序设计中定义常用数据类型时的作用

3 2.1 引 言 本章主要内容： 包括了大多数逻辑系统中的一些公共议题 代数项和它们在多类别代数中的解释
2.1 引 言 本章主要内容： 代数项和它们在多类别代数中的解释 等式规范（也叫代数规范）和等式证明系统 等式证明系统的可靠性和完备性（公理语义和指称语义的等价） 代数之间的同态关系和初始代数 数据类型的代数理论 从代数规范导出的重写规则（操作语义） 包括了大多数逻辑系统中的一些公共议题

4 2.2 代数、基调和项 2.2.1 代数 代数 例：N   N, 0, 1, +,   一个或多个集合，叫做载体
一组特征元素和一阶函数，也叫做代数函数 f : A1  … Ak  A 例：N   N, 0, 1, +,   载体N是自然数集合 特征元素0, 1N，也叫做零元函数 函数+,  : N  N  N

5 2.2 代数、基调和项 多个载体的例子 下面开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要
APCF  N, B, 0, 1, …, +, true, false, Eq ?, … 下面开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要 定义数据类型 证明性质 进行化简 还必须讨论这种语法描述的指称语义 A5PCF N5, B, 0, 1, 2, 3, 4, +5, true, false, Eq ?, …

6 2.2 代数、基调和项 2.2.2 代数项的语法 基调  S，F 例: N  S，F S是一个集合，其元素叫做类别
函数符号f : s1 …  sk  s的集合F ，其中表达式s1 …  sk  s叫做类型 零元函数符号叫做常量符号 例: N  S，F sorts : nat fctns : 0, 1 : nat ,  : nat  nat  nat

7 2.2 代数、基调和项 项 定义基调的目的是用于写代数项 项中可能有变量，因此需假定一个无穷的符号集合V，其元素称为变量
类别指派  x1 : s1, …, xk : sk 基调S，F和类别指派上类别s的代数项集合Termss (, )定义如下： 1、如果x : s  ，那么x  Termss (, ) 2、如果f : s1 …  sk  s并且Mi Termssi(, ) (i  1, …, k)，那么f M1 … Mk  Termss (, ) 当k  0时，如果f : s，那么f  Termss (, )

8 2.2 代数、基调和项 项的例子 代数项中无约束变元 记号 , x : s     x : s
0, 0  1 Termsnat (N, ) 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(, )中项的结构进行归纳

9 2.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) )是该基调的项

10 2.2 代数、基调和项 2.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 

11 2.2 代数、基调和项 代数A的环境 环境 满足 M  Termss (, )的含义AM是
 : V  s As 环境 满足 如果对每个x : s  都有(x)As M  Termss (, )的含义AM是 Ax  (x) AM  fA (AM1, …, AMk) 若f : s是常量符号，则Af   fA 若A清楚时，省略A而直接写成M 不依赖于时，用AM表示M在A中的含义

12 2.2 代数、基调和项 例 若(x)  0N x  1  N(x, 1)  N ((x), 1N)
 N (0N, 1N)  1N

13 2.2 代数、基调和项 例 Astk  N, N, 0A, 1A, …, A, A, emptyA,
pushA, pop A, top A emptyA   , 空序列 pushA(n, s)  n :: s popA(n :: s)  s popA( )   topA(n :: s)  n topA( )  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

14 2.2 代数、基调和项 引理2.2 令A是代数，MTermss(, )，并且是满足的环境，那么M  As
引理2.3 令x1, …, xk是由出现在MTermss(, )中的所有变量构成的变量表，1和2是满足的两个环境, 并且对i1, …, k有1(xi) 2(xi), 那么M1  M2 证明 基于项结构的归纳

15 2.2 代数、基调和项 2.2.4 代换引理 引理 令MTermss(, , x:s)并且N Termss(, )，那么NxMTermss(, )。并且对任何环境，有  NxM   M (x  a)， 其中a  N，它是N在下的含义 证明 根据项M的结构进行归纳

16 2.3 等式、可靠性和完备性 代数规范 一个基调 + 一组等式 调查什么样的代数满足这些等式强加的要求 使用等式证明系统可推导新的等式
可靠性：从规范可证明的等式在任何满足该规范的代数中都成立 完备性：在满足规范的所有代数中都成立的等式都可从该规范证明 代数规范是描述代数数据类型公理语义的工具

17 2.3 等式、可靠性和完备性 2.3.1 等式 公式 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 (永真的、有效的 )

18 2.3 等式、可靠性和完备性 若A满足上所有等式，就说代数A是平凡的 例
令有两个类别a和b，令A是一个代数，其中Aa{0,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]无意义地成立

19 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的结果

20 2.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(fa) (f (f b))

21 2.3 等式、可靠性和完备性 引理 令MTerms(, )，并且是满足的项代数Terms(, )的环境，那么M   M 证明 对项进行归纳证明 从项代数可以知道，只有M和N是语法上相同的项时，等式M  N 才会永真

22 2.3 等式、可靠性和完备性 2.3.3 语义蕴涵和等式证明系统 代数规范Spec  , E : 基调和一组等式E
语义蕴涵：E  M  N  满足E的所有代数A都满足等式M  N  语义理论E ： 如果E  M  N 蕴涵M  N   E 代数A的理论Th(A) 在A中成立的所有等式的集合 这是一个语义理论 22

23 2.3 等式、可靠性和完备性 证明系统的可靠性：若一个等式从一组假设E可证，则E语义上蕴涵该等式
下面先给出代数证明系统，然后讨论可靠性和完备性

24 2.3 等式、可靠性和完备性 1、语义相等是个等价关系，因此有 M  M  2、在等式中增加类别指派的规则 3、等价代换
M = N  N = M  M = N  N = P  M = P  M = N  M = N , x : s x不在中 M = N , x : s P = Q  P/xM = Q/xN  P , Q Termss(, )

25 2.3 等式、可靠性和完备性 等式可证：若从E中的等式和公理(ref)及推理规则(sym)、(trans)、(subst) 和(add var) 可以推出等式M  N ，则说该等式可证，写成 E  M  N  语法理论 如果E  M  N蕴涵M  N  E E的语法理论Th(E) 从E可证的所有等式的集合

26 2.3 等式、可靠性和完备性 等式集合E是语义一致的 等式集合E是语法一致的 若存在某个等式M  N ，它不是E的语义蕴涵

27 2.3 等式、可靠性和完备性 例 在基调stk  S, F上增加等式 使用这些等式可以证明等式
top (push x s ) = x [s : stack, x : nat] pop (push x s ) = s [s : stack, x : nat] 使用这些等式可以证明等式 top (push 3 empty ) = 3 top(push x s ) = x [s : stack, x : nat] empty = empty [x : nat] top(push x empty ) = x [x : nat] 3 = 3 [ ] top(push 3 empty ) = 3 [ ] 27

28 2.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

29 2.3 等式、可靠性和完备性 定理（可靠性）如果E  M  N  ， 那么E  M  N 
证明 可以根据该证明的长度进行归纳 归纳基础：长度为1的证明，它是公理或E的一个等式 归纳假设： M  N 的最后一步是从E1, …, En得到。那么，如果A  E，则A满足E1, …, En 要证明：若A满足最后一条规则的这些前提，则A满足M  N  证明 根据证明规则的集合，分情况进行分析 29

30 2.3 等式、可靠性和完备性 命题 存在代数理论E和不含x的项M和N，使得E  M =N , x : s，但是E  M =N  证明 令基调有类别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 []不成立的模型 由可靠性，c = d []是不可能从E证明的 30

31 2.3 等式、可靠性和完备性 例 栈代数规范 sorts : nat, stack fctns : 0, 1, 2, … : nat
例 栈代数规范 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, = 1, … 0  0 = 0, 0  1 = 0, … top (push x s ) = x pop (push x s ) = s 31

32 2.3 等式、可靠性和完备性 等式 push (top s) (pop s) = s [s : stack] 是不可证明的 任何形式为
top empty = M [] 的等式都是不可证明的，假定M是类别为nat的 项，并且不含empty 32

33 2.3 等式、可靠性和完备性 2.3.4 完备性的形式 用于不同逻辑系统的三种不同形式的完备性 最弱的形式：所有的永真公式都是可证的
演绎完备性：每个语义蕴涵在证明系统中都是可推导的 最小模型完备性：每个语法理论是某个“最小”模型的语义理论 对代数来说，最小模型完备性意味着每个语法理论是某个代数A的Th(A) “最小模型”是指它的理论包含的内容最少 33

34 2.3 等式、可靠性和完备性 最小模型完备性不一定成立，考虑等式 E  x = y [ x : a, y : a, z : b ]
1、a的载体只含一个元素，则E满足，此时 E1  x = y [ x : a, y : a ] 成立 2、 b的载体为空，则E也满足，此时 E2  z = w [ z : b, w : b ] 成立 E1和E2都不是E的语义蕴涵 不存在一个代数，其理论正好就是由E的等式推论组成的语法理论 34

35 2.3 等式、可靠性和完备性 2.3.5 同余、商和演绎完备性 同余关系：等价关系加上同余性 同余性：指函数保可证明的相等性
对单类代数A = A, f1A, f2A,…，同余关系是载体A上的等价关系，使得对每个k元函数fA，若aibi(i=1,…, k)，即ai和bi等价，则fA(a1, …, ak )  fA(b1, …, bk ) 对多类代数A = As, I ，同余关系是一簇等价关系  s, s  AsAs，使得对每个f : s1  …  sks及变元序列a1, …, ak和b1, …, bk(其中ai sibi  Asi),有fA(a1, …, ak ) s fA(b1, …, bk ) 35

36 2.3 等式、可靠性和完备性 A模的商的代数A 等价类[a] [a]  a  As  a  a 
(A)s是由As的所有等价类构成的集合 Ass  as  a  As} 函数fA由A的函数fA确定 对适当载体的a1,…, ak， fA ([a1], …, [ak]) = [fA(a1, …, ak)] 36

37 2.3 等式、可靠性和完备性 上面定义有意义的条件是 例 单类别代数N，0，1，上的同余关系“模k等价”
fA([a1], …, [ak])必须只依赖于[a1], …, [ak]，而不能依赖于所选的代表a1, …, ak 例 单类别代数N，0，1，上的同余关系“模k等价” 这个商代数是总所周知的整数模k的加结构。如果k等于5，那么3  4  2 37

38 2.3 等式、可靠性和完备性 如果是A的一个环境，是一个同余关系，那么A的环境 定义如下：
 (x) = [(x)] 反过来，对于A的环境，对应它的A的环境有多种选择 引理 令是代数A上的同余关系，项M Terms(, )并且是满足的环境。那么项M在商代数A和环境下的含义(A)M由下式决定 (A )M =  M 38

39 2.3 等式、可靠性和完备性 引理 令E是一组等式集合，令Terms(, )是基调上的项集。由E的可证明性确定的关系E,是Terms(, )上的同余关系 定理（ 完备性）如果E  M  N  ， 那么E  M  N  完备性定理加上可靠性定理表明语法理论和语义理论相同 39

40 2.3 等式、可靠性和完备性 3.3.6 非空类别和最小模型性质 空载体提出一个技术问题 逻辑公式
若A = ，则公式x:A. F(x) 为真 若A = ，则公式x:A. F(x) 为假 对任意的M, N  Termss(, ) 如果x:s且As为空，那么M和N被看成是相等的项 只有一个类别时，假定该类别非空是有意义的

41 2.3 等式、可靠性和完备性 没有空载体的代数有最小模型完备性
类别s非空：集合Termss(, )不是空集 对应的载体肯定非空 没有空载体时，可以增加推理规则(nonempty) 定理 令E是封闭于规则（nonempty）的语法理论，那么存在所有载体都非空的代数A，使得E  Th (A) M = N , x : s M = N  41

42 2.4 同态和初始性 2.4.1 同态和同构 将同态和同构概念从单类代数推广到多类代数 同态是从一个代数到另一个代数的保结构的映射
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 (hs1a1, …, hskak) ) 42

43 2.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

44 2.4 同态和初始性 例 含义函数是从项代数T = Terms(, )到任意代数A的一个同态h : T  A。如果是A的一个满足的环境，该同态的定义是 h(M) = AM 这是一个同态，因为 h (f M1 … Mk ) = A f M1 … Mk = fA(AM1,…, AMk) = fA(h (M1 ), …, h (Mk ) ) 44

45 2.4 同态和初始性 引理 令h :AB是任意同态，并且是满足类别指派的任意A环境。那么对任何项M Terms(, )，有
2.4 同态和初始性 引理 令h :AB是任意同态，并且是满足类别指派的任意A环境。那么对任何项M Terms(, )，有 h (AM) = BMh 当M中不含变量时，h (AM ) =BM 证明 基于项的归纳 引理 如果h :AB和k :B C都是代数的同态，那么合成kh :AC也是代数的同态， (k  h)s = ks  hs 同构 一个双射的同态, 写成A  B 45

46 2.4 同态和初始性 2.4.2 初始代数 C是一类代数并且AC，若对每个BC，存在唯一的同态h : AB，则A在C中叫做初始代数
2.4 同态和初始性 2.4.2 初始代数 C是一类代数并且AC，若对每个BC，存在唯一的同态h : AB，则A在C中叫做初始代数 初始代数是“典型”的 初始代数有尽可能少的非空载体 初始代数满足尽可能少的闭等式 A B3 B2 B1 46

47 2.4 同态和初始性 例 基调0 类别nat， 函数符号0 : nat和S : nat  nat 令C是所有0代数构成的代数类
2.4 同态和初始性 例 基调0 类别nat， 函数符号0 : nat和S : nat  nat 令C是所有0代数构成的代数类 闭项代数T  Terms(0, )是C 的初始代数 它的载体是所有闭项0, S (0), …, Sk(0), … 该代数的函数S把Sk(0)映射到Sk1(0) 该代数的元素少到能解释所有的函数符号 该代数满足项之间尽可能少的等式 47

48 2.4 同态和初始性 引理 假定h : AB和k : BA都是同态，并且h  k=IdB，k  h =IdA。那么A和B同构
2.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的代数有唯一的同态 48

49 2.4 同态和初始性 例 sorts: nat fctns: 0 : nat S : nat  nat
2.4 同态和初始性 例 sorts: nat fctns: 0 : nat S : nat  nat  : nat  nat  nat； eqns： [x : nat, y : nat] x + 0 = x x + (Sy) = S (x + y) 可以证明如下事实： Sk0 + Sl0 = Sk + l0 对任何闭项M，存在某个自然数k，使得M = Sk0 49

50 2.4 同态和初始性 例 x + 0 = x x + (Sy) = S (x + y) 可以证明如下事实：
2.4 同态和初始性 例 x + 0 = x x + (Sy) = S (x + y) 可以证明如下事实： 等式Sk0 = Sl0是不可证的，除非k = l 每个等价类正好包含一个形式为Sk0的项 等价类集和形式为Sk0的项集间有一个双射 若把闭项集合{0, S0, …, Sk0, …}作为载体，函数S映射Sk0  Sk＋10，映射(Sk0, Sl0)  Sk＋l0，则得一个初始代数 这个初始代数和该基调的标准模型（有后继算子和加法的自然数） 同构 50

51 2.4 同态和初始性 初始代数和其他代数的比较 Anat = (0  N)  ({1}  Z) 0A = 0, 0
2.4 同态和初始性 初始代数和其他代数的比较 1、和有更多元素的代数比较 多余的元素不能由项定义（有垃圾） 例1：整数代数Z 例2： A = 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

52 2.4 同态和初始性 初始代数和其他代数的比较 2、和有较少元素的代数比较 一些不能证明为相等的项在该代数中被等同（有混淆）
2.4 同态和初始性 初始代数和其他代数的比较 2、和有较少元素的代数比较 一些不能证明为相等的项在该代数中被等同（有混淆） 例：模k的自然数 52

53 2.4 同态和初始性 初始代数的一个重要特点 初始代数可能会满足不能由E证明的额外的等式 例：自然数基调例子中，初始代数满足等式
2.4 同态和初始性 初始代数的一个重要特点 初始代数可能会满足不能由E证明的额外的等式 例：自然数基调例子中，初始代数满足等式 x + y = y + x 因为 E  M = Sk0和E  N = Sl0 蕴涵 E  M + N = Sk+l0 = N + M 53

54 2.4 同态和初始性 不满足交换律的代数 例：自然数基调例子中，初始代数满足等式 x + y = y + x
2.4 同态和初始性 例：自然数基调例子中，初始代数满足等式 x + y = y + x 不满足交换律的代数 Anat是所有f : X  X的函数的集合（X至少有两个元素） 0A是X上的恒等函数，SA是Anat上的恒等映射 +A是Anat上的函数合成 A = Anat  0A SA  +A满足E +A没有交换性，因为函数合成没有交换性 54

55 2.4 同态和初始性 基项、基代换、基实例（项、等式）
2.4 同态和初始性 基项、基代换、基实例（项、等式） 如果M  N 是Termss(, )的项之间的等式，并且S是一个，基代换，则把SM  SN 称为M  N 的基实例 命题 令E是一组等式，且A对E来说是初始代数，则对任何等式M  N ，下面三个条件等价 A满足M  N  A满足M  N 的每一个基实例 M  N 的每一个基实例都可以从E证明 55

56 2.5 代数数据类型 2.5.1 代数数据类型 本节讨论数据类型公理化方法的一般特征 程序设计中的很多数据类型
2.5 代数数据类型 2.5.1 代数数据类型 本节讨论数据类型公理化方法的一般特征 程序设计中的很多数据类型 不存在标准的数学构造，如优先队列和符号表 没有单一和标准的计算机实现 通常是列出它们的操作并公理化地描述这些操作之间的关系 因此是公理化地定义而不是由数学构造来定义 困难之处：对于一个数据类型，难以断定是否有了“足够”的公理 56

57 2.5 代数数据类型 数据抽象的一般原理 抽象数据类型由它的规范定义
2.5 代数数据类型 数据抽象的一般原理 抽象数据类型由它的规范定义 使用这样数据类型的程序应该只依赖于由它的规范保证的性质，而不依赖于它的任何特定实现 一个数据类型的函数可以划分成 构造算子：产生该数据类型的一个新元素 运算算子：是该数据类型上的函数，但不产生新的元素 观察算子：应用于该数据类型的元素，但返回其它类型的元素，如自然数或布尔值 57

58 2.5 代数数据类型 2.5.2 初始代数语义和数据类型归纳 代数规范有几种不同的“语义”形式
2.5 代数数据类型 2.5.2 初始代数语义和数据类型归纳 代数规范有几种不同的“语义”形式 宽松语义：满足一个代数规范的所有代数所构成的代数类 初始代数语义：满足一个代数规范的所有初始代数所构成的同构类 终结代数语义：满足一个代数规范的所有终结代数所构成的同构类 生成语义：满足一个代数规范的所有生成代数所构成的代数类 58

59 2.5 代数数据类型 初始代数的性质 构造符集合 没有垃圾 没有混淆 支持基于数据类型构造符的归纳
2.5 代数数据类型 初始代数的性质 没有垃圾 没有混淆 支持基于数据类型构造符的归纳 构造符集合 Spec  , E的函数符号集合的子集F0，使得Terms(,)E,的每个等价类正好只含一个由F0的函数符号所构成的基项 可以基于对构造符的归纳来证明初始代数的性质 59

60 2.5 代数数据类型 sorts: set, nat, bool 构造符、运算符、观察符 fctns: 0, 1, 2, … : nat + : nat  nat  nat Eq? : nat  nat  bool 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 +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 . . . 60

61 2.5 代数数据类型 终结代数 在一个代数类C中，如果从每个BC到AC，都存在唯一的同态，那么代数A是终结代数
2.5 代数数据类型 终结代数 在一个代数类C中，如果从每个BC到AC，都存在唯一的同态，那么代数A是终结代数 一个代数类中的所有终结代数都同构 若用终结代数作为语义，则称之为终结语义 如果所有载体都是单元素集合的代数也在C中，则这个代数一定是C的终结代数 61

62 2.5 代数数据类型 初始语义和终结语义 初始语义：不能证明为相等的就是不相等的 终结语义：不能证明为不相等的则是相等的
2.5 代数数据类型 初始语义和终结语义 初始语义：不能证明为相等的就是不相等的 终结语义：不能证明为不相等的则是相等的 如果把某些类别的解释固定，而其它类别的解释用终结语义，则它是一个有用的方法 从初始语义角度看，前面给出的不是集合的规范,而是表的规范。因为不能证明 insert x(insert y z)=insert y(insert x z) [x: nat, y: nat, z: set] insert x (insert x z) = insert x z[x : nat, z : set] 若用终结语义，且bool的解释固定,则为集合规范 62

63 2.5 代数数据类型 2.5.3 解释没有意义的项 表达式没有意义的情况 除法是一个部分函数，除数为零的表达式没意义
2.5 代数数据类型 2.5.3 解释没有意义的项 表达式没有意义的情况 除法是一个部分函数，除数为零的表达式没意义 调用不终止的函数也构成一个没有意义的表达式 如果想在代数规范中表示这些情况，必须在基调中增加表示错误的项（简称错误值） 怎样规定这些项的值？有三种可能： 什么也不规定 任意做一个决定 非常仔细地说明什么是所需要的 63

64 2.6 重写系统 2.6.1 基本定义 重写系统：用于代数项的归约系统 两种重要的应用 由一组叫做重写规则(LR)的有向等式组成
2.6 重写系统 2.6.1 基本定义 重写系统：用于代数项的归约系统 两种重要的应用 为代数项提供一种计算模型 自动定理证明 由一组叫做重写规则(LR)的有向等式组成 限制：Var(R)  Var(L) 由R确定的一步归约关系R [SLx]M R [SRxM 关系R是R的自反传递闭包 64

65 2.6 重写系统 sorts : nat fctns : 0 : nat  : nat  nat + : nat  nat  nat
2.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 65

66 2.6 重写系统 引理（归约保类别）令R是上的重写系统，若M  Termss (, )且MRN，则N  Termss (, ) 若N  M  P蕴涵N    P，则关系（重写系统）是合流的， 若不存在一步归约的无穷序列M0M1 M2…，则关系（重写系统）是终止的 不能再归约的项称为范式 合流并且终止的重写系统通常又叫做典范系统 66

67 2.6 重写系统 可变换性 若存在M  M1  M2  M3 … Mk  N，
2.6 重写系统 可变换性 若存在M  M1  M2  M3 … Mk  N， 则项M, N  Termss(, )是可变换的，写成 M ↔R N 箭头的方向并没有什么意义 对任何重写系统，可变换性和可证明的相等性是一致的 67

68 2.6 重写系统 项中的一个位置：便于引用子项的某个特定出现 位置n = 1, 2的子项是hab 用M n表示M在位置n的子项
2.6 重写系统 项中的一个位置：便于引用子项的某个特定出现 位置n = 1, 2的子项是hab 用M n表示M在位置n的子项 用N n M表示M在n的子项 由N代换的结果 f g x h a b f (gx(hab))(gba) x 68

69 2.6 重写系统 2.6.2 合流性和可证明的相等性 记号 若R是一组重写规则，ER用来表示对应的无向的等式集合 定理 1、对任何重写系统R，M RN 当且仅当ER  M  N； 2、对任何合流的重写系统R，ER  M  N 当且仅当M  R  R N 69

70 2.6 重写系统 2.6.3 终止性 良基关系：集合A上的一个关系是良基的，如果不存在A上元素的无穷递减序列a0  a1  a2 …的话。 如果能在项和有良基关系的集合A的元素间建立起一个对应，那么可以利用它去证明不存在无穷的归约序列M0 M1 M2 … 有几种方式可把项映射到有良基关系的集合 利用代数的语义结构 70

71 2.6 重写系统 代数A =  As1, As2, …, f1A, f2A, …是良基的，若
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 71

72 2.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) 各重写规则的左部定义的值都大于其右部定义的值 72

73 2.6 重写系统 2.6.4 临界对 局部合流 关系是局部合流的，若N  M P 蕴涵 N    P
2.6 重写系统 2.6.4 临界对 局部合流 关系是局部合流的，若N  M P 蕴涵 N    P 局部合流关系严格弱于合流关系 例 a  b, b  a a  a0, b  b0 a0 a b b0 73

74 2.6 重写系统 不相交的归约 cond B (cdr(cons s l)) (cons(car l)(cdr l) ) 规则如下：
2.6 重写系统 cond B (cdr(cons s l)) (cons(car l)(cdr l) ) 规则如下： cdr(cons x l)  l cons(car l)(cdr l)  l 不相交的归约 M SL SL SR SL SR 74

75 2.6 重写系统 平凡的重迭 cdr(cons x(cons(car l)(cdr l))) 规则如下：
2.6 重写系统 cdr(cons x(cons(car l)(cdr l))) 规则如下： cdr(cons x l)  l cons(car l)(cdr l)  l 平凡的重迭 SL SL SR SR 75

76 2.6 重写系统 非平凡的重迭 cdr(cons(car l)(cdr l)) 规则如下： cdr(cons x l)  l
2.6 重写系统 cdr(cons(car l)(cdr l)) 规则如下： cdr(cons x l)  l cons(car l)(cdr l)  l 非平凡的重迭 SL SL SR SR ??? 76

77 2.6 重写系统 临界对 L  R cdr(cons x l)  l L  R cons(car l)(cdr l)  l
2.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 77

78 2.6 重写系统 若f (gxy)  R，L中有子项f z、f (gPQ)、f (h …)。 f (h …)不可能与f (gxy) 合一
2.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 78

79 2.6 重写系统 命题 一个重写系统R是局部合流的，当且仅当对每个临界对M, N有M R  R N 证明
2.6 重写系统 命题 一个重写系统R是局部合流的，当且仅当对每个临界对M, N有M R  R N 证明 从左到右的蕴涵是简单明了的 另一个方向的证明仿照用于启发临界对定义的推理：不相交、平凡的重迭、临界对的代换实例 如果一个有限的重写系统R是终止的，那么该命题就给出一个算法，可用于判定R是否局部合流 79

80 2.6 重写系统 2.6.5 左线性无重迭重写系统 无重迭：没有非平凡的临界对 无重迭的重写系统不一定是合流的 例如：   S 
2.6 重写系统 2.6.5 左线性无重迭重写系统 无重迭：没有非平凡的临界对 无重迭的重写系统不一定是合流的 例如：   S  Eq ? x x  true Eq ? x (S x)  false Eq ?  有两个不同的范式 Eq ?    true Eq ?    Eq ?  (S )  false 80

81 2.6 重写系统 左线性的规则：任何变量在规则的左部的出现不超过一次的话 左线性的系统：每一条规则都是左线性的
2.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))有两个范式 81

82 2.6 重写系统 2.6.6 局部合流、终止和合流之间的联系 命题 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的 良基归纳
2.6 重写系统 2.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)为真 M N1 P1 Q N R S P 82

83 2.6 重写系统 2.6.6 局部合流、终止和合流之间的联系 命题 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的 例 if true then x else y  x if false then x else y  y if u then x else x  x M N1 P1 Q N R S P 83

84 2.6 重写系统 Knuth-Bendix完备化过程 一组等式 构造一个确定同样代数理论的终止且合流的重写系统
2.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) 84

85 2.6 重写系统 产生一个临界对f (x + y) + z, f x + (f y + z ) 增加一条重写规则
2.6 重写系统 产生一个临界对f (x + y) + z, f x + (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 ) 85

86 习 题 第一次：2.3(a)，2.9 第二次：2.11， 2.13， 2.14 第三次： 2.16(d), (e)， 2.19 第四次： 2.22， 2.23 第五次： 2.32(a)， 2.33 86