项重写系统 ·自动证明要解决的问题 项集T上等式集E中的等式要定向为单向项重写规 则，构成重写规则集R,以方便计算机对项化简 若E是：x+0=x,x+Sy)=S(x+y) x×0=0,x×Sy)=x×Jy+X 定向成如下的项重写系统R x+0→x,x+Sy)→Sx+y) x×0→0，x×Sy)→x×y+x 记号M→N:用一条规则可将项M归约成N - 例：x+S(Sy)→Sc+S)→S(Sc+) 子项能与第2条规则的左部匹配
项 重 写 系 统 • 自动证明要解决的问题 – 项集T 上等式集E中的等式要定向为单向项重写规 则, 构成重写规则集R, 以方便计算机对项化简 若E是：x + 0 = x，x + S(y) = S(x + y) x 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)) 子项能与第2条规则的左部匹配 17
项重写系统 ·自动证明要解决的问题 问题1：如何从E得到R,保证项的化简能终止 例：若有规则x+y=y+x,不管怎么定向都有 a+b→b+a→a+b→ -问题2：如何从E得到R,保证对项采用不同化简 策略所得最简项是唯一的（合流性） E:o=S(o),Eg(x,x)=true,Eg(x,S(x))=false R:oo→S(o),Eqx,x)-→true,Eqx,S(x)→false
项 重 写 系 统 • 自动证明要解决的问题 – 问题1：如何从E得到R，保证项的化简能终止 例：若有规则 x + y = y + x，不管怎么定向都有 a + b → b + a → a + b → … – 问题2：如何从E得到R，保证对项采用不同化简 策略所得最简项是唯一的（合流性） E： = S(), Eq(x, x) = true, Eq(x, S(x)) = false R： → S(), Eq(x, x) → true, Eq(x, S(x)) → false 18
项重写系统 自动证明要解决的问题 -问题1：如何从E得到R,保证项的化简能终止 例：若有规则x+y=y+x, 不管怎么定向都有 a+b→b+a→a+b> -问题2：如何从E得到R,保证对项采用不同化简 策略所得最简项是唯一的（合流性） R:oo→S(oo),Eqc,x)→true,Eqx,S(x)→false 则有：Eq(o,o)→true Eq(o,∞)-→Eq(o,S(o)-→false -问题3：如何从E得到R,使得E和R确定同样的代 数理论，即在E中能证则在R中也能证（完备性)
项 重 写 系 统 • 自动证明要解决的问题 – 问题1：如何从E得到R，保证项的化简能终止 例：若有规则 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中也能证（完备性）19
项重写系统 ·问题一：终止性 1.终止性 项集T上的R不存在无穷归约序列M→M,→M,→ 即：任何项都能归约到范式（不能再归约的项 2.有时很难对等式定向，以得到终止的重写系统 例如：对由三角函数公式构成的等式系统 和角公式：sin(a+B)=sina cosβ+cosa sinB,, 差角公式：sin(a-B)=sino cosβ-cosc sinβ，. 积化和差：sina cosβ=(sin(a+B)+sin(a-B)/2,. 和差化积：sino+sinβ=2sin(a+β)/2)cos(a-B)/2)
项 重 写 系 统 • 问题一：终止性 1. 终止性 项集T 上的R不存在无穷归约序列M0→M1→M2 → …, 即: 任何项都能归约到范式(不能再归约的项) 2. 有时很难对等式定向，以得到终止的重写系统 例如：对由三角函数公式构成的等式系统 和角公式: sin(+) = sin cos + cos sin, … 差角公式: sin( − ) = sin cos − cos sin, … 积化和差: sin cos = (sin(+)+sin(−))/2, … 和差化积: sin+sin = 2sin((+)/2)cos((−)/2), … … … 20
项重写系统 问题一：终止性 3.定义：良基关系（良基：wel-founded 集合A上的二元关系<是良基的，若不存在A上元 素的无穷递减序列ao>a1>a2>·(a>bffb<a) 例：自然数上的<关系是良基的，但≤关系不是 4.若项集T和良基集A有映射f:T→A,满足 T上任意归约序列M→M,→M2>.·→M, A上存在递减序列4，>41>a2>·>am 则T上不存在无穷的归约序列 21
项 重 写 系 统 • 问题一：终止性 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 上不存在无穷的归约序列 21