代数等式理论的自动定理证明计算机科学导论第一讲

1、代数等式理论的自动定理证明代数等式理论的自动定理证明计算机科学导论第一讲计算机科学导论第一讲计算机科学技术学院计算机科学技术学院陈意云陈意 http:/ 程程 内内 容容 课程内容课程内容围绕学科理论体系中的模型理论围绕学科理论体系中的模型理论, 程序理论和计算理论程序理论和计算理论1. 模型理论关心的问题模型理论关心的问题 给定模型给定模型M，哪些问题可以由模型，哪些问题可以由模型M解决；如何解决；如何比较模型的表达能力比较模型的表达能力2. 程序理论关心的问题程序理论关心的问题 给定模型给定模型M，如何用模型，如何用模型M解决问题解决问题 包括程序设计范型、程

2、序设计语言、程序设计、包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等形式语义、类型论、程序验证、程序分析等3. 计算理论关心的问题计算理论关心的问题给定模型给定模型M和一类问题和一类问题, 解决该类问题需多少资源解决该类问题需多少资源本次讲座基于中学的等式本次讲座基于中学的等式推理推理, ,与这些内容关系不大与这些内容关系不大2课课 程程 内内 容容 本讲座内容本讲座内容 以以代数等式理论中的定理证明为例，介绍怎样从代数等式理论中的定理证明为例，介绍怎样从中学生熟知的等式演算中学生熟知的等式演算方法方法，构造构造等式等式定理定理的的自自动证明动证明系统，即将问

3、题变为系统，即将问题变为可用计算机求解可用计算机求解 有助于理解计算思维的含义有助于理解计算思维的含义计算思维（译文）计算思维（译文） 运用计算机科学的基础概念进行问题求解、系统运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动的一系列思维活动3讲讲 座座 提提 纲纲 基本知识基本知识 代数项、代数等式、演绎推理规则、代数等式理代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法论、等式定理证明方法 项重写系统项重写系统 终止性、良基关系、合流性、局部合流性、关键终止性、良基关系、合流性、

4、局部合流性、关键对对 良基归纳法良基归纳法 仅举例说明仅举例说明 Knuth-Bendix完备化过程完备化过程 也仅举例说明也仅举例说明4基基 本本 知知 识识 代数项和代数等式（仅涉及一个类型）代数项和代数等式（仅涉及一个类型） 代数项代数项例：自然数类型例：自然数类型nat 0, 1, 2, : nat常量常量 x, y : nat变量变量 +, f : nat nat nat 二元函数二元函数 S : nat nat一元的后继函数一元的后继函数 0, x, x + 1, x + S(y)和和f(100, y) 都是代数项都是代数项 代数等式代数等式例：例： x + 0 = x，x + S

5、(y) = S(x + y) x + y = z + 55基基 本本 知知 识识 代数项和代数等式（代数项和代数等式（涉及多个类型涉及多个类型） 例：定义有限表：同类数据的有限序列的集合例：定义有限表：同类数据的有限序列的集合 6, 17, 50, 28, 188, 92, 30, 67, 15 18.8, 9.2, 50, 77, 8.6, 5.5, 40.0 a, b, c, d, e, f, , z（非数值数据）（非数值数据） 上述数据涉及两个类型上述数据涉及两个类型 序列中元素的类型序列中元素的类型 数值或非数值类型数值或非数值类型 这些序列所属的类型，称为表（这些序列所属的类型，称为

6、表（list）类型）类型 非数值类型非数值类型 中学所学的代数概念在此已经扩展中学所学的代数概念在此已经扩展6基基 本本 知知 识识 代数项和代数等式（代数项和代数等式（涉及多个类型涉及多个类型） 代数项（表代数项（表类型类型list ，表元类型，表元类型atom） x : atom,l : list 变量变量 nil : list 零元构造函数零元构造函数 (常量常量) cons : atom list list 构造函数构造函数 first : list atom，rest : list list 观察函数观察函数 nil, cons(x, l), rest(cons(x, nil), r

7、est(cons(x, l), cons(first(l), rest(l)都是代数项。用都是代数项。用T 表示项集表示项集 代数等式代数等式(方括号列出等式中出现的变量及类型方括号列出等式中出现的变量及类型) first(cons(x, l) = x x : atom, l : list rest(cons(x, l) = l x : atom, l : list7基基 本本 知知 识识 等式证明等式证明例：基于一组等式（公式、公理）：例：基于一组等式（公式、公理）：x + 0 = x 和和 x + S(y) = S(x + y) 怎么证明等式：怎么证明等式：x + S(S(y) = S(S

8、(x + y) ?需要有推理规则需要有推理规则8 等式证明的演绎推理规则等式证明的演绎推理规则自反公理：自反公理：M M 对称规则：对称规则：传递规则：传递规则：加变量规则：加变量规则：等价代换规则：等价代换规则：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 = Q/x N 基基 本本 知知 识识x不在不在 中中P , Q 是类型是类型s的项的项9 等式推理的例子等式推理的例子等价代换规则：等价代换规则：等式公理：等式公理：x + 0 = x和和x + S(y) = S(x + y)证明等

9、式：证明等式： x + S(S(y) = S(S(x + y)证证明明: x + S(S(y) 根据根据x + S(z) = S(x + z)，S(y) = S(y)= S(x + S(y)使用等价代换规则得到第一个等式使用等价代换规则得到第一个等式 S(x + S(y) 根据根据S(z) = S(z)，x + S(y) = S(x + y)= S(S(x + y) 使用等价代换规则得到第二个等式使用等价代换规则得到第二个等式x + S(S(y) = S(S(x + y) 根据根据传递规则和上面两等式传递规则和上面两等式M = N , x : s P = Q P/x M = Q/x N 基基

10、本本 知知 识识10 等式推理的例子等式推理的例子等价代换规则：等价代换规则：等式公理：等式公理：x + 0 = x和和x + S(y) = S(x + y)证明等式：证明等式： x + S(S(y) = S(S(x + y)证明证明: x + S(S(y)= S(x + S(y) 我们的证明演算习惯见左边我们的证明演算习惯见左边= S(S(x + y) 它是基于刚才所介绍的演绎推理的它是基于刚才所介绍的演绎推理的若希望计算机来自动推理，严格的推理规则是必若希望计算机来自动推理，严格的推理规则是必须提供的须提供的M = N , x : s P = Q P/x M = Q/x N 基基 本本 知

11、知 识识11基基 本本 知知 识识 代数等式理论（代数等式理论（algebraic equation theory）在在项集项集T 上上从一组等式从一组等式E（公理）能推出的公理）能推出的所有等式的集合称为一个等式理论（通俗的解释）所有等式的集合称为一个等式理论（通俗的解释） 代数等式理论的定理证明代数等式理论的定理证明判断等式判断等式 M = N 是否在某个代数等式理论中是否在某个代数等式理论中 常用证明方法常用证明方法 把把M和和N分别化简分别化简, 若它们的最简形式一样则相等若它们的最简形式一样则相等 分别证明分别证明M和和N都等于都等于L 证明证明M N等于等于0 还有其他方法还有其他

12、方法12基基 本本 知知 识识 哪种证明方法最适合于计算机自动证明？哪种证明方法最适合于计算机自动证明？ 把把M和和N分别化简分别化简, 若它们的最简形式一样则相等若它们的最简形式一样则相等 若基于等式若基于等式E，通过等式证明，把，通过等式证明，把M和和N化简到化简到最简形式，则这种方式相对简单，便于自动证明最简形式，则这种方式相对简单，便于自动证明 并且采用适合于计算机使用的单向并且采用适合于计算机使用的单向重写规则重写规则 分别证明分别证明M和和N都等于都等于L 自动选择自动选择L是非常困难的是非常困难的 证明证明M N等于等于0 不适用于非数值类型的项，例如先前给出的不适用于非数值类型

13、的项，例如先前给出的atom类型的表类型的表13项项 重重 写写 系系 统统 自动证明要解决的问题自动证明要解决的问题 项集项集T 上上等式集等式集E中的等式要定向为单向项重写中的等式要定向为单向项重写规则规则, 构成构成重写规则集重写规则集R, 以方便计算机对项化简以方便计算机对项化简若若E是：是：x + 0 = x，x + S(y) = S(x + y) x 0 = 0，x S(y) = x y + x定向成如下的项重写系统定向成如下的项重写系统Rx + 0 x，x + S(y) S(x + y)x 0 0，x S(y) x y + x 记号记号M N：用一条规则可将项：用一条规则可将项M

14、归约成归约成N 若规则若规则LR R，含，含z一次出现的项一次出现的项T，以及使得以及使得SL/zT T的代换的代换S，则，则SL/zT SR/zT “”既用于既用于规则，也用规则，也用于项的归约于项的归约14项项 重重 写写 系系 统统 自动证明要解决的问题自动证明要解决的问题 项集项集T 上上等式集等式集E中的等式要定向为单向项重写中的等式要定向为单向项重写规则规则, 构成重写规则集构成重写规则集R, 以方便计算机对项化简以方便计算机对项化简若若E是：是：x + 0 = x，x + S(y) = S(x + y) x 0 = 0，x S(y) = x y + x定向成如下的项重写系统定向成

15、如下的项重写系统Rx + 0 x，x + S(y) S(x + y)x 0 0，x S(y) x y + x 记号记号M N：用一条规则可将项：用一条规则可将项M归约成归约成N 例：例：x + S(S(y)“”既用于既用于规则，也用规则，也用于项的归约于项的归约15项项 重重 写写 系系 统统 自动证明要解决的问题自动证明要解决的问题 项集项集T 上上等式集等式集E中的等式要定向为单向项重写中的等式要定向为单向项重写规则规则, 构成重写规则集构成重写规则集R, 以方便计算机对项化简以方便计算机对项化简若若E是：是：x + 0 = x，x + S(y) = S(x + y) x 0 = 0，x

16、S(y) = x y + x定向成如下的项重写系统定向成如下的项重写系统Rx + 0 x，x + S(y) S(x + y)x 0 0，x S(y) x y + x 记号记号M N：用一条规则可将项：用一条规则可将项M归约成归约成N 例：例：x + S(S(y) S(x + S(y) S(x + S(y)/zz S(S(x + y)/zz16代换代换S：xx yS(y)项项 重重 写写 系系 统统 自动证明要解决的问题自动证明要解决的问题 项集项集T 上上等式集等式集E中的等式要定向为单向项重写中的等式要定向为单向项重写规则规则, 构成重写规则集构成重写规则集R, 以方便计算机对项化简以方便计

17、算机对项化简若若E是：是：x + 0 = x，x + S(y) = S(x + y) x 0 = 0，x S(y) = x y + x定向成如下的项重写系统定向成如下的项重写系统Rx + 0 x，x + S(y) S(x + y)x 0 0，x S(y) x y + x 记号记号M N：用一条规则可将项：用一条规则可将项M归约成归约成N 例：例：x + S(S(y) S(x + S(y) S(S(x + y) 子项能与第子项能与第2条规则的左部匹配条规则的左部匹配17项项 重重 写写 系系 统统 自动证明要解决的问题自动证明要解决的问题 问题问题1：如何从：如何从E得到得到R，保证项的化简能保

18、证项的化简能终止终止例：若有规则例：若有规则 x + y = y + x，不管怎么定向都有，不管怎么定向都有 a + b b + a a + b 问题问题2：如何从：如何从E得到得到R，保证对项采用不同化简，保证对项采用不同化简策略所得最简项是唯一的（策略所得最简项是唯一的（合流性合流性） E： = S( ), Eq(x, x) = true, Eq(x, S(x) = falseR： S( ), Eq(x, x) true, Eq(x, S(x) false18项项 重重 写写 系系 统统 自动证明要解决的问题自动证明要解决的问题 问题问题1：如何从：如何从E得到得到R，保证项的化简能保证项

19、的化简能终止终止例：若有规则例：若有规则 x + y = y + x，不管怎么定向都有，不管怎么定向都有 a + b b + a a + b 问题问题2：如何从：如何从E得到得到R，保证对项采用不同化简，保证对项采用不同化简策略所得最简项是唯一的（策略所得最简项是唯一的（合流性合流性）R： S( ), Eq(x, x) true, Eq(x, S(x) false则有：则有： Eq( , ) true Eq( , ) Eq( , S( ) false 问题问题3：如何从：如何从E得到得到R, ,使得使得E和和R确定同样的代确定同样的代数理论，即在数理论，即在E中能证则在中能证则在R中也能证（中

20、也能证（完备性完备性）19项项 重重 写写 系系 统统 问题一：终止性问题一：终止性1. 终止性终止性 项集项集T 上的上的R不存在无穷归约序列不存在无穷归约序列M0M1M2 , 即即: 任何项都能归约到范式任何项都能归约到范式(不能再归约的项不能再归约的项)2. 有时很难对等式定向，以得到终止的重写系统有时很难对等式定向，以得到终止的重写系统例如：对由三角函数公式构成的等式系统例如：对由三角函数公式构成的等式系统 和角公式和角公式: sin( + ) = sin cos + cos sin , 差角公式差角公式: sin( ) = sin cos cos sin , 积化和差积化和差: si

21、n cos = (sin( + )+sin()/2, 和差化积和差化积: sin +sin = 2sin( + )/2)cos()/2), 20项项 重重 写写 系系 统统 问题一：问题一：终止性终止性3. 定义：良基关系（良基：定义：良基关系（良基：well-founded）集合集合A上的二元关系上的二元关系 是是良基的良基的，若不存在，若不存在A上元上元素的无穷递减序列素的无穷递减序列a0 a1 a2 （a b iff b a）例：自然数上的例：自然数上的1, 有有 x 规则规则2： x, y 1, 有有2(x+y+1) = 2x2y2 2x2y22x24项项 重重 写写 系系 统统 问题

22、二：合流性问题二：合流性1. 记号记号 MN：M经若干步经若干步(含含0步步)重写后得到重写后得到N NM：若有：若有MN M N：若存在：若存在P，使得，使得MP且且NP2. 定义定义 令令R是项集是项集T 上的上的重写系统重写系统, ,若若N M P 蕴涵蕴涵N P，则，则R是是合流合流的的3. 定义定义 令令R是项集是项集T 上的上的重写系统重写系统, ,若若N M P 蕴涵蕴涵N P，则，则R是是局部局部合流合流的的 局部合流关系严格弱于合流关系局部合流关系严格弱于合流关系 先考虑局部合流的判定方法，然后再考虑合流的先考虑局部合流的判定方法，然后再考虑合流的判定方法判定方法25项项 重

23、重 写写 系系 统统 插曲插曲在介绍局部合流性之前，先介绍代数项的树形表示在介绍局部合流性之前，先介绍代数项的树形表示代数项代数项cons(first(cons(x, l), rest(cons(y, l)的树形的树形表示表示 倒长的树：根在上，叶在下倒长的树：根在上，叶在下 每棵子树代表一个子项，整个树每棵子树代表一个子项，整个树代表完整的代数项代表完整的代数项26consconsconsrestfirstyllx项项 重重 写写 系系 统统 局部合流性的判定（问题二的子问题）局部合流性的判定（问题二的子问题）1. 讨论所选用的例子讨论所选用的例子函数：函数：nil : listcons :

24、 atom list list first : list atom，rest : list list cond : bool list list list等式：等式： first(cons(x, l) = x, rest(cons(x, l) = l, cons(first(l), rest(l) = l, 下面的讨论针对如下两条重写规则：下面的讨论针对如下两条重写规则：rest(cons(x, l) lcons(first(l ), rest(l ) l 27项项 重重 写写 系系 统统 局部合流性的判定（问题二的子问题）局部合流性的判定（问题二的子问题） (1) 无重叠的归约无重叠的归约

25、归约规则：归约规则： rest(cons(x, l) l （规则（规则LR） cons(first(l ), rest(l ) l （规则（规则LR ） 待归约项：待归约项：cond (B, rest(cons s l), cons(first(l), rest(l) ) 方式方式1: 原式原式 cond(B, l, cons(first(l), rest(l) ) cond(B, l, l) 方式方式2: 原式原式 cond (B, rest(cons s l), l) cond(B, l, l) 特点：特点：M中无重叠子项的归约相互不受影响中无重叠子项的归约相互不受影响28项项 重重 写写

26、 系系 统统 局部合流性的判定局部合流性的判定 (1) 无重叠的归约无重叠的归约图示：图示： LR 和和LR 是规则是规则 图中图中SL和和SR分别表示分别表示 代换代换S作用于作用于L的的 结果结果 S : T T 代换代换S的最主要部分的最主要部分是把变量映射到项是把变量映射到项MSLSL MSLSR MSRSR SL MSR29cond (B, rest(cons s l), cons(first(l), rest(l)项项 重重 写写 系系 统统 局部合流性的判定（问题二的子问题）局部合流性的判定（问题二的子问题） (2) 平凡的重叠平凡的重叠 归约规则：归约规则：rest(cons(

27、x, l) l（规则（规则LR） cons(first(l ), rest(l ) l （规则（规则LR ） 待归约项：待归约项： rest(cons(x, cons(first(l), rest(l) 方式方式1: 原式原式 cons(first(l), rest(l) l 方式方式2: 原式原式 rest(cons(x, l) l30项项 重重 写写 系系 统统 局部合流性的判定（问题二的子问题）局部合流性的判定（问题二的子问题） (2) 平凡的重叠平凡的重叠 归约规则：归约规则：rest(cons(x, l) l（规则（规则LR） cons(first(l ), rest(l ) l （

28、规则（规则LR ） 待归约项：待归约项： rest(cons(x, cons(first(l), rest(l) 特点：特点：SL 是是SL的子项的子项，且，且S把把L中的某变量中的某变量(这里是这里是l)用用由由SL 构成的项代换构成的项代换 不同的第不同的第1步归约不会影响局部合流，但合流所步归约不会影响局部合流，但合流所需归约步数可能不一样（取决于需归约步数可能不一样（取决于R中有几个中有几个l）31项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 (2) 平凡的重叠平凡的重叠 图示：图示： SL 是是SL的子项的子项，且，且S把把L中的某变量中的某变量x用有用有SL 构成

29、的项代换构成的项代换 不同的第不同的第1步归约步归约不会影响局部合流，不会影响局部合流，但合流所需归约但合流所需归约步数可能不一样步数可能不一样SLSL SLSR SRSL SL SRSR SR 32rest(cons(x, cons(first(l), rest(l)项项 重重 写写 系系 统统 局部合流性的判定（问题二的子问题）局部合流性的判定（问题二的子问题）(3) 非平凡的重叠非平凡的重叠 归约规则：归约规则：rest(cons(x, l) l（规则（规则LR） cons(first(l ), rest(l ) l （规则（规则LR ） 待归约项：待归约项：rest(cons(firs

30、t(l), rest(l) 方式方式1: 原式原式 rest(l)（用规则（用规则LR） 方式方式2: 原式原式 rest(l)（用规则（用规则LR ） 该例比较特殊，都一步归约就到范式该例比较特殊，都一步归约就到范式33项项 重重 写写 系系 统统 局部合流性的判定（问题二的子问题）局部合流性的判定（问题二的子问题）(3) 非平凡的重叠非平凡的重叠 归约规则：归约规则：rest(cons(x, l) l（规则（规则LR） cons(first(l ), rest(l ) l （规则（规则LR ） 待归约项：待归约项：rest(cons(first(l), rest(l) 特点：特点：SL 在

31、在SL的非变量位置的非变量位置LR 或或LR 的使用都可能使的使用都可能使对方在原定位置对方在原定位置 不能使用，故不能保证局部合流不能使用，故不能保证局部合流34项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定(3) 非平凡的重叠非平凡的重叠 图示：图示： SL 在在SL的非变量位置的非变量位置 LR或或LR 的使用的使用都可能使都可能使对方在原定对方在原定位置不能使用，故不位置不能使用，故不能保证局部合流能保证局部合流SLSL SLSR SR? 35rest(cons(first(l), rest(l)项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 若所有含非

32、平凡重叠的项都能局部合流若所有含非平凡重叠的项都能局部合流, 则则R也能也能 把对所有含非平凡重叠的项的检查缩小为对有限把对所有含非平凡重叠的项的检查缩小为对有限的重写规则集的检查的重写规则集的检查 若由若由R的重写规则确定的所有关键对的重写规则确定的所有关键对(critical pair)都能归约到同一个项，则都能归约到同一个项，则所有项的非平凡重所有项的非平凡重叠都能局部合流叠都能局部合流（课堂上不介绍（课堂上不介绍） 例：重写规则例：重写规则rest(cons(x, l) l，和，和 cons(first(l ), rest(l ) l 会形成两个关键对会形成两个关键对36项项 重重 写

33、写 系系 统统第第1个关键对：个关键对：（课堂上不介绍）（课堂上不介绍） 选适当的代换，使得两规则代换后绿色选适当的代换，使得两规则代换后绿色部分一样部分一样cons(first(l ), rest(l ) l rest(cons(x, l) l 第第1条规则中的条规则中的l 用用cons(x, l)代换后代换后, 其左部是项：其左部是项：cons(first(cons(x, l), (rest(cons(x, l) 用这两条规则化简上述项可得第用这两条规则化简上述项可得第1个关键对：个关键对： cons(x, l), cons(first(cons(x, l), l) 归约关键对：归约关键对

34、：cons(x, l)已经是范式已经是范式 cons(first(cons(x, l), l) cons(x, l) 第第1个关键对能归约到同一个项个关键对能归约到同一个项37项项 重重 写写 系系 统统第第2个关键对：个关键对：（课堂上不介绍）（课堂上不介绍） 选适当的代换，使得两规则代换后绿色选适当的代换，使得两规则代换后绿色部分一样部分一样 cons(first(l ), rest(l ) l rest(cons(x, l) l 第第2条规则中的条规则中的x和和l分别代换成分别代换成first(l )和和rest(l )后后,其左部是项：其左部是项：rest(cons(first(l )

35、, rest(l ) 用这两条规则化简上述项可得第用这两条规则化简上述项可得第2个关键对：个关键对： rest(l ), rest(l ) 显然，第显然，第2个关键对也能归约到同一个项个关键对也能归约到同一个项38项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 定理定理 一个重写系统一个重写系统R是局部合流的，当且仅当对是局部合流的，当且仅当对每个关键对每个关键对 M, N 有有M N 如果如果一个有限的重写系统一个有限的重写系统R是终止的，那么该定是终止的，那么该定理就给出一个算法，可用于判定理就给出一个算法，可用于判定R是否局部合流是否局部合流39项项 重重 写写 系系 统

36、统 局部合流、终止和合流之间的联系局部合流、终止和合流之间的联系定理定理 令令R是终止的重写系统，那么是终止的重写系统，那么R是合流的当是合流的当且仅当它是局部合流的且仅当它是局部合流的 合流蕴含局部合流（这是显然的）合流蕴含局部合流（这是显然的） 反方向蕴含的证明需要使用良基归纳法反方向蕴含的证明需要使用良基归纳法40良良 基基 归归 纳纳 法法 良基归纳法良基归纳法用一个简单例子说明它比自然数归纳法更一般用一个简单例子说明它比自然数归纳法更一般证明：对任何自然数的有限集合，每次删除一个元证明：对任何自然数的有限集合，每次删除一个元 素，最终会到达空集素，最终会到达空集 1. 若忽略集合中元

37、素的个性，只关心集合中元素若忽略集合中元素的个性，只关心集合中元素的个数，则可以用自然数归纳法的个数，则可以用自然数归纳法 2. 若关注元素个性（虽无必要）若关注元素个性（虽无必要） ：集合之间的归约：集合之间的归约规则规则: x1, , xnx2, , xn其中其中x1是左边集合的任意元素是左边集合的任意元素 3.良基关系：良基关系：A B则则A B410, 1, 21, 20, 20, 1012良良 基基 归归 纳纳 法法 良基归纳法良基归纳法需要证明：任何自然数的有限集合可归约到空集需要证明：任何自然数的有限集合可归约到空集1. 对所有的归约路径进行归纳对所有的归约路径进行归纳2. 良基

38、归纳证明良基归纳证明归纳基础：归纳基础：经经0步归约到步归约到归纳假设：对所有的归纳假设：对所有的s s1, s s2, s sn, s1, s2, , sn都能归约都能归约到到归纳证明：证明归纳证明：证明s能归约到能归约到420, 1, 21, 20, 20, 1012良良 基基 归归 纳纳 法法 良基归纳法良基归纳法（课堂上不介绍）（课堂上不介绍）令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某个性质。若每当所有的个性质。若每当所有的P(b) (b a)为真则为真则P(a)为真为真(即即 a.( b.(b a P(b) P(a) )，那么，对所有的那么，对所

39、有的a A，P(a)为真为真证明步骤：证明步骤： 归纳基础归纳基础: 对任意不存在对任意不存在b使得使得b a的的a，证明，证明P(a) 在不存在在不存在b使得使得b a的情况下，的情况下， b.(b a P(b) P(a)等价于等价于 true P(a)等价于等价于 P(a)43良良 基基 归归 纳纳 法法 良基归纳法良基归纳法（课堂上不介绍）（课堂上不介绍）令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某个性质。若每当所有的个性质。若每当所有的P(b) (b a)为真则为真则P(a)为真为真(即即 a.( b.(b a P(b) P(a) )，那么，对所有的

40、那么，对所有的a A，P(a)为真为真证明步骤：证明步骤： 归纳基础归纳基础: 对任意不存在对任意不存在b使得使得b a的的a，证明，证明P(a) 归纳步骤：对任意存在归纳步骤：对任意存在b使得使得b a的的a， b.(b a P(b) P(a)在此得出归纳假设：在此得出归纳假设： 假定对所有假定对所有b a的的b，P(b)为真，然后证明：为真，然后证明： 归纳证明：证明归纳证明：证明P(a)为真为真44良良 基基 归归 纳纳 法法 用良基归纳法证明合流性用良基归纳法证明合流性证明：若有证明：若有M N和和 M P，则，则N P若若MN, 则规定则规定N M。因系统终止因系统终止, 故故 是良

41、基的是良基的归纳基础：归纳基础： 若不存在若不存在N使得使得N M，即即M是范式，显然是范式，显然M具有具有要证明的性质要证明的性质 因为因为M只能只能0步归约到步归约到M本身，图上的本身，图上的N和和P都只都只能是能是MMNP45(M)(M)M良良 基基 归归 纳纳 法法 用良基归纳法证明合流性用良基归纳法证明合流性证明：若有证明：若有M N和和 M P，则，则N P若若MN, 则规定则规定N M。因系统终止因系统终止, 故故 是良基的是良基的归纳步骤：归纳步骤：假定假定M N1 N并且并且M P1 P(1) 根据局部合流性，根据局部合流性，存在存在Q，使得，使得N1 Q P1MN1P1NP

42、46良良 基基 归归 纳纳 法法 用良基归纳法证明合流性用良基归纳法证明合流性证明：若有证明：若有M N和和 M P，则，则N P若若MN, 则规定则规定N M。因系统终止因系统终止, 故故 是良基的是良基的归纳步骤：归纳步骤： 假定假定M N1 N并且并且M P1 P(1) 根据局部合流性，根据局部合流性，存在存在Q，使得，使得N1 Q P1MN1P1QNP47良良 基基 归归 纳纳 法法 用良基归纳法证明合流性用良基归纳法证明合流性证明：若有证明：若有M N和和 M P，则，则N P若若MN, 则规定则规定N M。因系统终止因系统终止, 故故 是良基的是良基的归纳步骤：归纳步骤： 假定假定

43、M N1 N并且并且M P1 P(2) 由归纳假设，由归纳假设，存在存在R， 使得使得N R QMN1P1QNP48良良 基基 归归 纳纳 法法 用良基归纳法证明合流性用良基归纳法证明合流性证明：若有证明：若有M N和和 M P，则，则N P若若MN, 则规定则规定N M。因系统终止因系统终止, 故故 是良基的是良基的归纳步骤：归纳步骤： 假定假定M N1 N并且并且M P1 P(2) 由归纳假设，由归纳假设，存在存在R， 使得使得N R QMN1P1QNRP49良良 基基 归归 纳纳 法法 用良基归纳法证明合流性用良基归纳法证明合流性证明：若有证明：若有M N和和 M P，则，则N P若若M

44、N, 则规定则规定N M。因系统终止因系统终止, 故故 是良基的是良基的归纳步骤：归纳步骤： 假定假定M N1 N并且并且M P1 P(3) 再由归纳假设，再由归纳假设，存在存在S， 使得使得R S PMN1P1QNRP50良良 基基 归归 纳纳 法法 用良基归纳法证明合流性用良基归纳法证明合流性证明：若有证明：若有M N和和 M P，则，则N P若若MN, 则规定则规定N M。因系统终止因系统终止, 故故 是良基的是良基的归纳步骤：归纳步骤： 假定假定M N1 N并且并且M P1 P(3) 再由归纳假设，再由归纳假设，存在存在S， 使得使得R S P(4) N P得证得证MN1P1QNRSP

45、51Knuth-Bendix完备化过程完备化过程 问题三：完备性问题三：完备性回顾回顾 最适合于计算机自动证明代数等式最适合于计算机自动证明代数等式M=N的方式：的方式： 把把M和和N分别化简分别化简, 若它们的最简形式一样则相等若它们的最简形式一样则相等 由定向代数等式系统由定向代数等式系统E来得到等价的重写系统来得到等价的重写系统R，需解决三个问题：终止性、合流性和完备性需解决三个问题：终止性、合流性和完备性完备性：从完备性：从E可可得到得到R，E和和R确定同样的代数理论确定同样的代数理论 概要介绍概要介绍Knuth-Bendix完备化过程完备化过程 给出一个完备化过程不终止的例子。由此可

46、知，给出一个完备化过程不终止的例子。由此可知，并非对任何并非对任何E都都可以得到与之有同样代数理论的可以得到与之有同样代数理论的R52Knuth-Bendix完备化过程完备化过程 Knuth-Bendix完备化过程的目的完备化过程的目的完备化过程的目的完备化过程的目的 为一个代数等式系统为一个代数等式系统E，构造一个确定同样代数，构造一个确定同样代数理论的终止且合流的重写系统理论的终止且合流的重写系统R53Knuth-Bendix完备化过程完备化过程 Knuth-Bendix完备化过程简介完备化过程简介1. 把把E定向成一个终止的重写系统定向成一个终止的重写系统R（若定向失败，则完备化过程失败

47、）（若定向失败，则完备化过程失败）2. 检查检查R的局部合流性并进行完备化的局部合流性并进行完备化for(R的每个关键对的每个关键对 M, N ) if (不具备不具备M N) 把把MN或或NM加入加入R（原因稍后解释）（原因稍后解释） （若定向失败，则完备化过程失败）（若定向失败，则完备化过程失败） (过程可能因过程可能因R不断地被加入规则而不终止不断地被加入规则而不终止)3. 最终的最终的R为所求为所求54Knuth-Bendix完备化过程完备化过程 例：完备化过程不终止例：完备化过程不终止作为输入的等式系统作为输入的等式系统E如下如下f(x) f(y) = f(x + y)(x + y)

48、 + z = x + (y + z)1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化55Knuth-Bendix完备化过程完备化过程 例：完备化过程不终止例：完备化过程不终止作为输入的等式系统作为输入的等式系统E如下如下f(x) f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R f(x) f(y) f(x + y) (x + y) + z x + (

49、y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化(1) 把两条规则左部的绿色部分进行合一，把两条规则左部的绿色部分进行合一，产生产生一一个个临界临界对对 f(x + y) + z, f(x) + (f(y) + z) 临界对的两个项都已最简，这个临界对不能合流临界对的两个项都已最简，这个临界对不能合流 因第因第2条规则左部的合条规则左部的合一结果：一结果： (f(x) f(y) + z 56Knuth-Bendix完备化过程完备化过程 例：完备化过程不终止例：完备化过程不终止作为输入的等式系统作为输入的等式系统E如下如下f(x) f(y) = f(x + y)(x + y

50、) + z = x + (y + z)1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化(1) 把两条规则左部的绿色部分进行合一，把两条规则左部的绿色部分进行合一，产生产生一一个个临界临界对对 f(x + y) + z, f(x) + (f(y) + z) (2) 增加增加重写规则重写规则f(x + y) + z f(x) + (f(y) + z) 因第因第2条规则左部的合条规则左部的合一结果：一结果： (f(x) f(y) + z 57Kn

51、uth-Bendix完备化过程完备化过程 例：完备化过程不终止例：完备化过程不终止解释：增加规则解释：增加规则f(x + y) + z f(x) + (f(y) + z)的原因的原因 在在E中可证中可证f(x + y) + z和和f(x) + (f(y) + z)相等相等等式等式：f(x) f(y) = f(x + y)和和(x + y) + z = x + (y + z) 证明：证明：f(x + y) + z = f(x) f(y) + z = f(x) + (f(y) + z) 在未加上述重写规则在未加上述重写规则R中证明不了中证明不了, 即即R不不完备完备： 在在R中能证的等式在中能证的

52、等式在E中中能证，但存在能证，但存在E中中能证而能证而在在R中不能证的等式中不能证的等式 向向R中加规则是为了完备性中加规则是为了完备性58Knuth-Bendix完备化过程完备化过程 例（续）例（续）1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化(1) 产生一个临界对产生一个临界对 f(x + y) + z, f(x) + (f(y) + z) (2) 增加重写规则增加重写规则f(x + y) + z f(x) + (f(y) + z)(3) R扩大为：扩大为： f(x) f(y) f (x + y) (x + y) + z x + (y + z) f(x + y) + z f(x) + (f(y) + z)59Knuth-Bendix完备化过程完备化过程 例（续）例（续）1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R