课程内容 课程内容 围绕学科理论体系中的模型理论，程序理论和计算理论 1.模型理论关心的问题 给定模型M,哪些问题可以由模型M解决；如何 比较模型的表达能力 本次讲座基于中学的等式 2.程序理论关心的问题 推理，与这些内容关系不大 给定模型M,如何用模型M解袂问题 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3.计算理论关心的问题 给定模型M和一类问题，解决该类问题需多少资源
课 程 内 容 • 课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何 比较模型的表达能力 2. 程序理论关心的问题 – 给定模型M，如何用模型M解决问题 – 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源 本次讲座基于中学的等式 推理,与这些内容关系不大 2
课程内容 本讲座内容 以代数等式理论中的定理证明为例，介绍怎样从 中学生熟知的等式演算方法，构造等式定理的自 动证明系统，即将问题变为可用计算机求解 有助于理解计算思维的含义 计算思维（译文) 运用计算机科学的基础概念进行问题求解、系统 设计、以及人类行为理解等涵盖计算机科学之广度 的一系列思维活动
课 程 内 容 • 本讲座内容 – 以代数等式理论中的定理证明为例，介绍怎样从 中学生熟知的等式演算方法，构造等式定理的自 动证明系统，即将问题变为可用计算机求解 – 有助于理解计算思维的含义 计算思维（译文） 运用计算机科学的基础概念进行问题求解、系统 设计、以及人类行为理解等涵盖计算机科学之广度 的一系列思维活动 3
讲座提纲 ,基本知识 -代数项、代数等式、演绎推理规则、代数等式理 论、等式定理证明方法 项重写系统 -终止性、良基关系、合流性、局部合流性、关键 对 良基归纳法 -仅举例说明 Knuth-Bendix完备化过程 也仅举例说明
讲 座 提 纲 • 基本知识 – 代数项、代数等式、演绎推理规则、代数等式理 论、等式定理证明方法 • 项重写系统 – 终止性、良基关系、合流性、局部合流性、关键 对 • 良基归纳法 – 仅举例说明 • Knuth-Bendix完备化过程 – 也仅举例说明 4
基本知识 ·代数项和代数等式（仅涉及一个类型） -代数项 例：自然数类型nat 021,2,…:nat 常量 x,y:nat 变量 +,f:nat×nat→nat 二元函数 S:nat→nat 一元的后继函数 0,x,x+1,x+Sy)和100，y) 都是代数项 代数等式 例：x+0=x,x+S0y)=Sx+y) 5 x十y=z+5
基 本 知 识 • 代数项和代数等式（仅涉及一个类型） – 代数项 例：自然数类型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(y) = S(x + y) x + y = z + 5 5
基本知识 ·代数项和代数等式（涉及多个类型） 例：定义有限表：同类数据的有限序列的集合 6,17,50,28,188,92,30,67,15 18.8,9.2,50,77,8.6,5.5240.0 a,b,C,d,e,f,...Z (非数值数据》 上述数据涉及两个类型 。序列中元素的类型一 数值或非数值类型 ,这些序列所属的类型，称为表 (ist)类型 非数值类型 中学所学的代数概念在此已经扩展
基 本 知 识 • 代数项和代数等式（涉及多个类型） – 例：定义有限表：同类数据的有限序列的集合 • 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 （非数值数据） – 上述数据涉及两个类型 • 序列中元素的类型 — 数值或非数值类型 • 这些序列所属的类型，称为表（list）类型 — 非数值类型 – 中学所学的代数概念在此已经扩展 6
基本知识 ·代数项和代数等式（涉及多个类型） 代数项（表类型ist,表元类型atom) x:atom, l:list 变量 nil list 零元构造函数（常量 cons:atom×list→list 构造函数 first:list→atom,rest:list→list 观察函数 nil,cons(x,1),rest(cons(x,nil)),rest(cons(x,1)), cons(first((,rest()都是代数项。用T表示项集 代数等式（方括号列出等式中出现的变量及类型 first(cons(x,1)=x [x atom,I list] rest(cons(x,1)=l x atom,1 list]
基 本 知 识 • 代数项和代数等式（涉及多个类型） – 代数项（表类型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)), rest(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 : list] 7
基本知识 ·等式证明 例：基于一组等式（公式、公理）： x+0=x和x+Sy)=Sc+y) 怎么证明等式： x+SS))=S(S+))? 需要有推理规则 8
基 本 知 识 • 等式证明 例：基于一组等式（公式、公理）： x + 0 = x 和 x + S(y) = S(x + y) 怎么证明等式： x + S(S(y)) = S(S(x + y)) ? 需要有推理规则 8
基本知识 等式证明的演绎推理规则 M=N[T] 自反公理：M=M[T] 对称规则： N=M[T] M=NT]N=PT] 传递规则： M=P[] 加变量规则： M=NT] x不在T中 M=NI,x:s] M=NT,x:s]P=0[T] 等价代换规则： [PIx]M [Q/]N [T] P,2是类型s的项
• 等式证明的演绎推理规则 自反公理：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/xM = Q/xN 基 本 知 识 x不在中 P , Q 是类型s的项 9
基本知识 等式推理的例子 等价代换规则： M=NT,x:s]P=0[T] [PIx]M [Q/x]N [T] 等式公理：x+0=x和x+Sy)=S(x+y) 证明等式：x+SSy)=SSc+) 证明：x+SSy)根据x+Sz=Sx+z),Sy=Sy =S(x+S(y)) 使用等价代换规则得到第一个等式 S(x+S(y)) 根据Sz=Sz),x+Sy)=Sx+y S(S(x+y)) 使用等价代换规则得到第二个等式 x+S(Sy)=S(Sc+y)根据传递规则和上面两等式
• 等式推理的例子 等价代换规则： 等式公理：x + 0 = x和x + S(y) = S(x + y) 证明等式： 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/xM = Q/xN 基 本 知 识 10
基本知识 等式推理的例子 等价代换规则： M=NT,x:s]P=0[T] [PIx]M [Q/x]N [T] 等式公理：x+0=x和x+Sy)=S(x+y) 证明等式：x+SSy)=S(S(c+) 证明：x+SSy) =S(x+S(y)) 我们的证明演算习惯见左边 S(S(x+y)) 它是基于刚才所介绍的演绎推理的 若希望计算机来自动推理，严格的推理规则是必 须提供的
• 等式推理的例子 等价代换规则： 等式公理：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/xM = Q/xN 基 本 知 识 11