北航 计算理论 第四章 推理与计算2.ppt

定理2 如果R为典型项重写系统,则对任何项t1和t2,有： R? t1=t2 ? ||t1||R= ||t2||R 判定两个项t1和t2是否相等,只要利用R中的重写规则证明它们的典型式是否相同即可. 定理3： 对有限项重写系统R和项t，从t开始的所有 计算的可终止是不可判定的。 定理4： 对有限项重写系统R，R可终止是不可判定的。 等式与重写的区别： 等式表示的是一个关系，没有方向，且对等式两端都没有限制。 重写规则是方向性的动作(action)，如X?Y表示X可被Y代替，但反之就不成立。而且对X和Y都有限制，如X不能为一个变量，Y不能包含不在X中出现的变量。 抽象数据类型 数据类型： 若干数据域和其上的若干操作的集合。 抽象数据类型： 一类数据类型，各类型可以有不同的数据表示，但其上的操作有共同的抽象性质。 标记： 标记是一个二元组（S,??）,其中S是类型集合，?为操作符号集合， ??P({f| f:??s, ??S*,s?S})。 例：自然数栈的规范可用标记表示为： S = {bool, nat, stack, error} ? = {true:?bool,false:?bool, not: bool?bool,or: bool bool?bool 0:?nat,succ: nat ?nat, eq: nat nat ?bool creat: ?stack, pop: stack?stack, empty: stack?bool, read: stack?nat?error push: stack nat ? stack} 项：设(S, ?)是一个标记,对任意s?S， Xs表示类型s的变量集合。 X={Xs|s?S }称为标记(S, ?)的变量集合 类型s的项集合T?,s(X)定义如下： Xs ? T?,s(X) 任一? 中f：s1…sn?s,若t1…tn分别是类型s1…sn 的项，即ti? T?,si(X)，i=1,…,n。则 f(t1,…,tn)? T?,s(X) T?(X)= {T?,s(X)|s?S}称为标记的项集合。 类型s的常量和变量称为基本项 其它称为是复合项。 不含变量的类型s的项称为基项 类型s的基项集合记为T?,s(?)或T?,s。 T?(?)或T?为（S，?）的基项集合。 例: push(pop(push(create,0)),x1) push(pop(push(create,x2)),x1) 是复合项 0，create,x1,x2 是基本项 push(create,0),pop(push(create,0))是基项 公理： 设（S，?）是标记，一个类型s的?－等式e是二元组(L, R),其中s?S，L，R? T?,s(X) . 通常将（L，R）记为L=R 。若L，R ? T?,s，则称e是一基等式。称E={e1,…,en}是由n个?－等式e1,…,en组成的一组公理。 例： 上例自然数栈的?－等式: not(true)＝ false; not(false) = true; or(true, x) = true; or(false, x) = x; eq(0,0) = true; eq(0,succ(n)) =false; eq(succ(n),0) =false; eq(succ(n),succ(m)) =eq(n,m); empty(create)=true; pop(create) =create; empty(push(s,n)) = false; pop(push(s,n)) = s; read(push(s,n)) = n; read(create) = error. 代数规范(S,?,E) ： 由一个标记(S,?)和其上的一组?－等式组成的公理集E构成。 代数规范的扩展： 代数规范(S,?,E)称为是另一个代数规范(S1,?1,E1)的扩展，如果： (S,?,E) = (S1+S’,?1+?’,E1+E’) +表示集合上的不相交并。 Bool = S: bool ?: true:?bool false: ?bool not: bool ?bool or: bool bool ?bool E: not(true)=false; not(false)= true; or(true,x)=true; or(false,x)=x