代数等式理论自动定理证明计算机科学导论一章节.ppt

《代数等式理论自动定理证明计算机科学导论一章节.ppt》由会员分享，可在线阅读，更多相关《代数等式理论自动定理证明计算机科学导论一章节.ppt（51页珍藏版）》请在三一文库上搜索。

1、代数等式理论的自动定理证明 计算机科学导论第一讲,计算机科学技术学院 陈意云 0551-63607043 ,课 程 内 容,课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力 2. 程序理论关心的问题 给定模型M，如何用模型M解决问题 包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源,本次讲座与这些内容关系不大,课 程 内 容,本讲座内容 以代数等式理论中的定理证明为例，介绍怎样从中学生熟知的

2、等式演算方法，构造自动定理证明系统，即将问题变为可用计算机求解 有助于理解什么是计算思维 计算思维（译文） 运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动,讲 座 提 纲,基本知识 代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法 项重写系统 终止性、良基关系、合流性、局部合流性、关键对 良基归纳法 Knuth-Bendix完备化过程,基 本 知 识,代数项 仅涉及一个类型的代数项 例：自然数类型的项0, x, x + 1, x + S(y), f(100, y) 其中x和y变量，f 和S是一阶函数，S是后继函数 涉及多个类

3、型的代数项 若有变量 x : atom, l : list（list是atom的表类型） 并有函数 nil : list, cons : atom list list first : list atom，rest : list list 则 nil, cons(x, l), rest(cons(x, nil), rest(cons(x, l)和cons(first(l), rest(l)都是代数项,基 本 知 识,代数等式 例： x + 0 = x，x + S(y) = S(x + y)， x + y = z + 5 first(cons(x, l) = x x : atom, l : lis

4、t rest(cons(x, l) = l x : atom, l : list 其中方括号中至少列出等式中出现的变量 等式证明 例：基于一组等式：x + 0 = x和x + S(y) = S(x + y) 怎么证明等式x + S(S(y) = S(S(x + y) ? 需要有推理规则,等式证明的演绎推理规则 自反公理：M M 对称规则： 传递规则： 加变量规则： 等价代换规则：,基 本 知 识,x不在中,P , Q 是类型s的项,等式推理的例子 等价代换规则： 等式公理：x + 0 = x和x + S(y) = S(x + y) 证明等式： x + S(S(y) = S(S(x + y) 证

5、: x + S(S(y) 根据x + S(z) = S(x + z)，S(y) = S(y) = S(x + S(y) 使用等价代换规则得到第一个等式 = S(S(x + y) 根据S(z) = S(z), x + S(y) = S(x + y) 使用等价代换规则得到第二个等式 再利用传递规则可得要证的等式,基 本 知 识,基 本 知 识,代数等式理论（algebraic equation theory） 在项集T 上从一组等式E(公理、公式)能推出的所 有等式的集合称为一个等式理论（通俗的解释） 代数等式理论的定理证明 判断等式 M = N 是否在某个代数等式理论中 常用证明方法 把M和N分

6、别化简, 若它们的最简形式一样则相等 分别证明M和N都等于L 证明MN等于0,还有其它方法,基 本 知 识,哪种证明方法最适合于计算机自动证明？ 把M和N分别化简, 若它们的最简形式一样则相等 若基于所给的等式E，能把M和N化简到最简形式，则这种方式相对简单，便于自动证明 分别证明M和N都等于L 自动选择L是非常困难的 证明MN等于0 不适用于非数值类型的项，例如先前给出的atom类型的表,项 重 写 系 统,自动证明要解决的问题 项集T 上等式集E中的等式要定向为单向项重写规则, 构成重写规则集R, 以方便计算机对项化简 例如：x + 0 = x，x + S(y) = S(x + y) x

7、0 = 0，x S(y) = x y + x 定向成如下的项重写系统R x + 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) 两步重写都使用规则x + S(y) S(x + y),“”既用于规则，也用于项的归约,项 重 写 系 统,自动证明要解决的问题 项集T 上等式集E中的等式要定向为单向项重写规则, 构成重写规则集R, 以方便计算机对项化简 例如：x + 0 = x，x + S(y) = S(x + y) x 0 = 0，x S(y) =

8、x y + x 定向成如下的项重写系统R x + 0 x，x + S(y) S(x + y) x 0 0，x S(y) x y + x 记号M N：用一条规则可将项M归约成N 通过定向等式来得到确定同样代数理论的重写系统，需解决三个问题：终止性、合流性和完备性,“”既用于规则，也用于项的归约,项 重 写 系 统,终止性 1. 终止性 项集T 上的R不存在无穷归约序列M0M1M2 , 即: 任何项都能归约到范式(不能再归约的项) 2. 有时很难对等式定向，以得到终止的重写系统 例如：对由三角函数公式构成的等式系统 和角公式: sin(+) = sin cos + cos sin, 差角公式: s

9、in( ) = sin cos cos sin, 积化和差: sin cos = (sin(+)+sin()/2, 和差化积: sin+sin = 2sin(+)/2)cos()/2), ,项 重 写 系 统,终止性 3. 定义：良基关系（良基：well-founded） 集合A上的一个关系是良基的，若不存在A上元 素的无穷递减序列a0 a1 a2 （a b iff b a） 例：自然数上的关系是良基的，但关系不是 4. 若项集T 和有良基的集合A有映射f :T A, 满足 T 上任意归约序列 M0 M1 M2 Mn f f f f A上存在递减序列 a0 a1 a2 an 则T 上不存在无穷

10、的归约序列,项 重 写 系 统,终止性 5. 定理 令R是项集T 上的一个重写系统，若能找到有良基关系的集合A和映射f :T A，使得对R中每条规则L R都有f (L) f (R) ,那么R是终止的 6. f 的选择 基于项的语法特点，或者给项指派一种语义 例1（基于语法特点：根据两边项语法上的繁简） first(cons(x, l) x rest(cons(x, l) l,项 重 写 系 统,终止性 例2（逻辑运算系统，给项指派一种语义） x x A 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

11、) (x y) (x z) A(x) = 2x (y z) x (y x) (z x) A表示f 映射算符的结果，它是A上的二元函数 对每条规则L R，都有f (L) f (R) 规则1：x 1, 有 x 规则2：x, y 1, 有2(x+y+1) = 2x2y2 2x2y,项 重 写 系 统,合流性 1. 记号 MN：M经若干步(含0步)重写后得到N NM：若有MN M N：若存在P，使得MP且NP 2. 定义 令R是项集T 上的重写系统,若N M P 蕴涵N P，则R是合流的 3. 定义 令R是项集T 上的重写系统,若N M P 蕴涵N P，则R是局部合流的 局部合流关系严格弱于合流关系

12、先考虑局部合流的判定方法，然后再考虑合流,项 重 写 系 统,局部合流性的判定 1. 讨论所选用的例子 函数：nil : list cons : 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) l cons(first(l), rest(l) l,项 重 写 系 统,局

13、部合流性的判定 (1) 无重叠的归约 归约规则： rest(cons(x, l) l （规则LR） cons(first(l), rest(l) l （规则LR） 待归约项： cond (B, rest(cons s l), cons(first(l), rest(l) ) 特点： M中无重叠子项的归约相互不受影响,项 重 写 系 统,局部合流性的判定 (1) 无重叠的归约 图示： LR 和LR是规则 图中SL表示代换S作用 于L的结果 代换是变量到项的映射,项 重 写 系 统,局部合流性的判定 (2) 平凡的重叠 归约规则： rest(cons(x, l) l （规则LR） cons(fir

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

15、l （规则LR） cons(first(l),rest(l) l （规则LR） 待归约项： rest(cons(first(l), rest(l) 特点： SL在SL的非变量位置 LR 或LR的使用都可能使对方在原定位置 不能使用，故不能保证局部合流,项 重 写 系 统,局部合流性的判定 (3) 非平凡的重叠 图示： SL在SL的非变量位置 LR或LR的使用都可能使对方在原定位置不 能使用，故不能保证局部合流,项 重 写 系 统,局部合流性的判定 若所有含非平凡重叠的项都能局部合流, 则R也能 把对所有含非平凡重叠的项的检查缩小为对有限的重写规则集的检查 若由R的重写规则确定的所有关键对(cr

16、itical pair)都能归约到同一个项，则所有项的非平凡重叠都能局部合流（可以证明，但在此不深究） 例：重写规则 rest(cons(x, l) l，和 cons(first(l), rest(l) l 会形成两个关键对,项 重 写 系 统,第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),

17、cons(first(cons(x, l), l) 归约关键对：cons(x, l)已经是范式 cons(first(cons(x, l), l) cons(x, l) 第1个关键对能归约到同一个项,项 重 写 系 统,第2个关键对： 选适当的代换，使得两规则代换后绿色部分一样 cons(first(l), rest(l) l rest(cons(x, l) l 第2条规则中的x和l分别代换成first(l)和rest(l)后,其左部是项： rest(cons(first(l), rest(l) 用这两条规则化简上述项可得第2个关键对： rest(l), rest(l) 显然，第2个关键对也能

18、归约到同一个项,项 重 写 系 统,局部合流性的判定 定理 一个重写系统R是局部合流的，当且仅当对每个关键对M, N有M N 如果一个有限的重写系统R是终止的，那么该定理就给出一个算法，可用于判定R是否局部合流,项 重 写 系 统,局部合流、终止和合流之间的联系 定理 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的 合流蕴含局部合流 反方向蕴含的证明需要使用良基归纳法,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为

19、真 证明步骤： 归纳基础: 对任意不存在b使得b a的a，证明P(a) 在不存在b使得b a的情况下， b.(b a P(b) P(a) 等价于 true P(a) 等价于 P(a),良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 证明步骤： 归纳基础: 对任意不存在b使得b a的a，证明P(a) 归纳步骤：对任意存在b使得b a的a， b.(b a P(b) P(a)的含义是 假定对所有b a的b，P(b)为真， 然后证明

20、P(a)为真,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 现在要证明的是：若有M N 和 M P，则N P 若MN, 则规定N M。 因是终止的系统，因此是良基的。 归纳基础：若不存在N使得N M，即M是范式， 显然M具有要证明的性质,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那

21、么，对所有的aA，P(a)为真 现在要证明的是：若有M N 和 M P，则N P 归纳步骤： 1. 若M N 或 M P是 0步归约，显然有N P,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 2. 假定M N1 N并且 M P1 P (1) 根据局部合流性， 存在Q，使得N1 Q P1,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真

22、(即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 2. 假定M N1 N并且 M P1 P (1) 根据局部合流性， 存在Q，使得N1 Q P1,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 2. 假定M N1 N并且 M P1 P (2) 由归纳假设， 存在R， 使得N R Q,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b

23、 a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 2. 假定M N1 N并且 M P1 P (2) 由归纳假设， 存在R， 使得N R Q,M,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 2. 假定M N1 N并且 M P1 P (3) 再由归纳假设， 存在S， 使得R S P,M,良 基 归 纳 法,良基归纳法 令是集合A上的一个良基关系，令P是A上的某 个性

24、质。若每当所有的P(b) (b a)为真则P(a)为真 (即a.(b.(b a P(b) P(a) )， 那么，对所有的aA，P(a)为真 2. 假定M N1 N并且 M P1 P (3) 再由归纳假设， 存在S， 使得R S P (4) N P得证,Knuth-Bendix完备化过程,Knuth-Bendix完备化过程的目的 回顾 最适合于计算机自动证明代数等式M=N的方式： 把M和N分别化简, 若它们的最简形式一样则相等 由定向代数等式系统E来得到等价的重写系统R，需解决三个问题：终止性、合流性和完备性 （完备性在后面的例子中解释） 完备化过程的目的 为一个代数等式系统E，构造一个确定同样

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

26、系统R f(x) f(y) f(x + y) (x + y) + z x + (y + z) 2. 检查局部合流性并进行完备化,Knuth-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 + (y + z) 2. 检查局部合流性并进行完备化 (1) 把两条规则左部的绿色部分进行合一，产生一 个临界对 f(x + y) + z, f(x) + (f(y) + z) 临界对的两个项都已最简，这个临界

27、对不能合流,第2条规则左部的合一结果： (f(x) f(y) + z,Knuth-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 + (y + z) 2. 检查局部合流性并进行完备化 (1) 把两条规则左部的绿色部分进行合一，产生一 个临界对 f(x + y) + z, f(x) + (f(y) + z) (2) 增加重写规则f(x + y) + z f(x) + (f(y) + z),第2条规

28、则左部的合一结果： (f(x) f(y) + z,Knuth-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中能证的等式在E中能证，但存在E中能证而在R中不能证的等式 向R中加规则是为了完备性,Knuth

29、-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),Knuth-Bendix完备化过程,例（续） 1. 先定向成一个终止

30、的重写系统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) 两条规则中的绿色部分也可以合一,Knuth-Bendix完备化过程,例（续） 1. 先定向成一个终止的重写系统R f(x) f

31、(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) 将产生无数规则: f n(x + y) + z f n(x) + (f n(y) + z),完备化过程因不断产生新的规则而不终止,构造性证明与传统证明对

32、比,传统证明的一个例子 证明 根据 是有理数或无理数来讨论,若 是有理数，则取x = 3 若 是无理数，则取x = 这种非构造性证明不太可能由计算机自动得到,小 结,本讲座小结 以代数等式理论中的定理证明为例，介绍怎样从熟知的等式演算方法，构造自动定理证明系统 不同逻辑的自动定理证明方法不同 自动定理证明的应用 集成电路设计 程序验证 程序分析 相关课程 数理逻辑、人工智能,小 结,工具 交互式定理证明辅助工具Coq http:/coq.inria.fr/， 获ACM2013年度软件系统奖 自动定理证明器Z3 1. http:/ redmond/projects/z3/old/index.html 2. http:/ 参考文献 Daniel Kroening and Ofer Strichman，Decision Procedures: An Algorithmic Point of View (Texts in Theoretical Computer Science. An EATCS Series),