程序验证(四):一阶理论

Tattoo

发布日期: 2020-06-29 21:05:56 浏览量: 115
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106582753

注意:原文中有部分公式书写错误,本文转载的时候,修正了这部分错误!

一、定义

一个一阶理论(theory)TT被以下两点定义:

  • 它的符号集Σ\Sigma, 一个非逻辑符号的集合

  • 它的公理AA, 一个在Σ\Sigma上的闭公式(closed formula)

一阶逻辑理论定义了一个有限的词汇表以讨论所关注的主题,而理论中的公理定义了所意指的涵义(intended meaning)。

Σformula\Sigma-formula:一个Σformula\Sigma-formula只包含Σ\Sigma中的非逻辑符号,以及逻辑变元,逻辑连接词和量词。

举例:

x,y.x=yy=x\forall x,y.x=y\to y=x

a[i]=eaie=aa[i] = e\to a \langle i \triangleleft e\rangle = a

二、常用理论(theory)

2.1 等价理论(Theory of Equality)

2.1.1 定义

等价理论TET_E由以下符号集给出:

ΣE:{=,a,b,c,...,f,g,h,...,p,q,r,...}\Sigma_E: \{=,a,b,c, ... ,f,g,h, ... ,p,q,r, ...\}

这里有二元等价符号 =,以及其他的常量、函数、谓词符号。TET_E的公理 “=” 满足自反性、对称性、传递性,以及函数与谓词的同余性(congruence)。

TET_E公式举例:

  • x,y.x=yy=x\forall x,y.x=y\to y=x

  • a=bb=cg(f(a),b)=g(f(c),a)a=b\wedge b=c\to g(f(a),b) = g(f(c),a)

符号集

ΣE:{=,a,b,c,...,f,g,h,...,p,q,r,...}\Sigma_E : \{=,a,b,c, ... ,f,g,h, ... ,p,q,r, ...\}

公理集

  • 自反性(refelxivity):x.x=x\forall x.x=x

  • 对称性(symmetry):x,y.x=yy=x\forall x,y.x=y \to y=x

  • 传递性(transitivity):x,y,z.x=yy=zx=z\forall x,y,z.x=y\wedge y=z \to x=z

  • 函数同余性(function congruence):x,y.(i=1nxi=yi)f(x)=f(y)\forall x,y.(\bigwedge ^n_{i=1} x_i=y_i)\to f(x) = f(y)

  • 谓词同余性(predicate congruence):谓词同余性(predicate congruence):x,y.(i=1nxi=yi)(p(x)p(y))\forall x,y.(\bigwedge ^n_{i=1} x_i = y_i)\to (p(x) \leftrightarrow p(y))

注意,以上公理并不是标准的公理,实际上,它只是一个模式(schema)因为表达式中的ffpp可以代表任何函数(或谓词)。

2.1.2 性质

TET_E是可判定的吗?(不是

证明方法:将TET_E公式转化为一阶逻辑公式:

  • TET_E仍然允许所有常量、函数以及谓词符号存在

  • 可以将任何一阶逻辑公式FF编码为TET_E公式FF^{\prime}

    • FF中所有 = 符号用一个新的(fresh)谓词符号替换

    • FF^{\prime}中不出现 = 符号

    • TET_E中的公理与此无关

然而,TET_E的量词自由片段(quantifier-free fragment)是可判定的。

2.1.3 理论的片段(theory fragment)

一个理论的片段(fragment)是TT中公式的一个由语义约束的(syntactically-restricted)子集,如果对于每个符合片段的语义约束的公式FFTFT\models F是可判定的,那么这个片段是可判定的量词自由的片段:TT中没有量词的永真公式(也可以看做是所有量词都是全称量词)。

2.1.4 永真性的证明

使用一阶逻辑中的语义分析方法,同时假如TET_E的公理。

举例:证明以下公式的永真性

F:x=yy=zg(f(x),y)=g(f(z),x)F: x=y\wedge y=z \to g(f(x),y) = g(f(z), x)

2.2 佩亚诺算术(Peano Arithmetic)

2.2.1 定义

符号集

ΣPA:{0,1,+,×,=}\Sigma_{PA} : \{0,1,+,\times , =\}

  • 0与1是常量

  • +与×\times是二元函数

  • =是二元谓词

  • 没有其他符号

公理集

  • 所有的等价公理:自反性、对称性、传递性、以及同余性

  • Zero: x.¬(x+1=0)Zero: \space \forall x.\neg(x+1=0)

  • Successor: x,y.(x+1=y+1)x=ySuccessor: \space \forall x,y.(x+1=y+1)\to x=y

  • Plus zero: x.x+0=xPlus \space zero: \space \forall x.x+0=x

  • Plus successor: x,y.x+(y+1)=(x+y)+1Plus \space successor: \space \forall x,y.x+(y+1)=(x+y)+1

  • Times zero: x.x×0=0Times \space zero: \space \forall x.x\times 0=0

  • Times successor: x,y.x×(y+1)=x×y+xTimes \space successor: \space \forall x,y.x\times (y+1)=x\times y+x

为了方便,以后我们把x×yx\times y记作xyxy

数学归纳法

一个模板:

(F(0)(x.F[x]f[x+1]))x.F[x](F(0)\wedge (\forall x.F[x]\to f[x+1]))\to \forall x.F[x]

这里FF代表任意的TPAT_{PA}公式,这就是数学归纳法在佩亚诺算术下的表达。

2.2.2 一种佩亚诺算术

因为算术中的函数与谓词符号可以有多种解释,所以这里说是“一种”。

最常见的:

  • Domain:NN

  • I[0],I[1]:0N,1NNI[0],I[1]: 0_{N}, 1_{N} \in N

  • I[+]:+N, addition over NI[+]: +_{N}, \space addition \space over \space N

  • I[×]:×N, multiplication over NI[\times]:\times _{N}, \space multiplication \space over \space N

  • I[=]:=N, equality over NI[=]:=_{N}, \space equality \space over \space N

2.2.3 语法糖

TPAT_{PA}中如何写3x+5=2y3x+5=2y

(1+1+1)×x+1+1+1+1+1=(1+1)×y(1+1+1)\times x +1+1+1+1+1=(1+1)\times y

如何表达x>5x>5

y.¬(y=0)x=5+y\exists y.\neg (y=0)\wedge x = 5+y

如何表达x+1yx+1\le y

z.x+1+z=y\exists z.x+1+z = y

2.2.4 性质

TPAT_{PA}中的可满足性与永真性是不可判定的,甚至量词自由的TPAT_{PA}也是不可判定的。

另外,TPAT_{PA}是不完备的。

总结:很多永真的数学命题在TPA T_{PA}上是非永真的,原因是由于乘法过于复杂。

2.3 Presburger算术

2.3.1 定义

符号集

ΣN:{0,1,+,=}\Sigma_{N}:\{0,1,+,=\}

公理集

  • 所有的等价公理:自反性、对称性、传递性、同余性

  • Zero: x.¬(x+1=0)Zero:\space \forall x.\neg (x+1=0)

  • Successor: x,y.(x+1=y+1)x=ySuccessor: \space \forall x,y.(x+1=y+1)\to x=y

  • Plus zero: x.x+0=xPlus \space zero: \space \forall x.x+0=x

  • Plus successor: x,y.x+(y+1)=(x+y)+1Plus \space successor: \space \forall x,y.x+(y+1)=(x+y)+1

  • Induction: (F[0](x.F[x]F[x+1]))x.F[x]Induction: \space (F[0]\wedge (\forall x.F[x]\to F[x+1]))\to \forall x.F[x]

2.3.2 性质

常用的解释与佩亚诺算术一样,但是,它有很好的性质:

  • 永真性可判定,但是很困难:复杂度O(22n)O(2^{2^n})

  • 完备性:对于任一TNT_{N}上的公式FF,或者F\models F或者¬F\models \neg F

  • 可以量词消除:对于任一TNT_{N}上的公式FF,存在一个等价的量词自由的FF^{\prime}
    量词自由的片段的可判定性是coNP-complete的

2.3.3 技巧:如何证明整数

考虑这样一个公式:

F0:w,x.y,z.x+2yz13>2w+5F_0:\forall w,x.\exists y,z.x+2y-z-13 > -2w+5

这里的 - 被解释为标准减法,w,x,y,zw,x,y,z的范围为整数集ZZ

为了表示TNT_N中的公式,为F0F_0中每个变量vv都引入两个变量vpv_pvnv_n

F1:wp,wn,xp,xn.yp,yn,zp,zn.(xpxn)+2(ypyn)(zpzn)13>3(wpwn)+5F_1: \forall w_p ,w_n ,x_p ,x_n.\exists y_p ,y_n ,z_p ,z_n.(x_p-x_n)+2(y_p-y_n)-(z_p-z_n)-13 > -3(w_p-w_n)+5

“移项”(因为TNT_N中没有减号),得到最终形式:

F2:wp,wn,xp,xn.yp,yn,zp,zn.u.¬(u=0)xp+yp+yp+zn+wp+wp+wp=xn+yn+yn+zp+wn+wn+wn+u+1+1+...+1F_2: \forall w_p ,w_n ,x_p ,x_n. \exists y_p ,y_n ,z_p ,z_n. \exists u. \neg(u=0)\wedge x_p +y_p +y_p +z_n+w_p+w_p+w_p = x_n +y_n +y_n +z_p + w_n +w_n +w_n + u +1+1+...+1

(一共13个+1)

2.4 线性整数算术

2.4.1 定义

符号集

ΣZ:{...,2,1,0,1,2,...,3×,2×,2×,3×,...,+,,=,>}\Sigma_{Z}: \{...,-2,-1,0,1,2, ... ,-3\times ,-2\times ,2\times ,3\times ,...,+,-,=,>\}

  • -2,-1,0,1,2,…,+,-,=,>就是通常情况下的涵义

  • −3×\times, -2×\times, 2×\times, 3×\times都是常系数的一元乘法函数

论断:TZT_{Z}可以归约(reduce)为TNT_{N}

  • 它们的表达能力相同

  • TZT_{Z}更加方便,所以比TNT_{N}更加常用

举例:证明以下公式的永真性

F:x,y,z.x>zy0x+y>zF: \forall x,y,z.x>z\wedge y\ge 0\to x+y>z

2.5 数列理论

2.5.1 定义

符号集

ΣA:{=,[],}\Sigma_A: \{=,\cdot [\cdot], \cdot \langle \cdot\triangleleft \cdot\rangle\}

  • 其中,a[i]a[i]是一个二元函数,表示在索引为ii处读取aa

  • 其中,aiva\langle i\triangleleft v\rangle是一个三元函数,代表在索引为ii处向aa写入值vv

  • 如果一个值vv被写入到aa的位置ii处,那么之后对于aa位置ii处的读操作应当返回vv

  • 逻辑是静态的,所以数组可以函数化表示,如(ai1v1)i2v2(a\langle i_1\triangleleft v_1\rangle)\langle i_2 \triangleleft v_2 \rangle

公理集

  • 自反性、对称性、传递性的等价公理

  • 数组同余:a,i,j.i=ja[i]=a[j]\forall a,i,j.i=j\to a[i]=a[j]

  • 读写-1:a,v,i,j.i=jaiv[j]=v\forall a,v,i,j.i=j\to a\langle i \triangleleft v\rangle [j]=v

  • 读写-2:a,v,i,j.ijaiv[j]=a[j]\forall a,v,i,j. i\ne j\to a\langle i \triangleleft v\rangle [j]=a[j]

注意:等价性只在数组元素之间被讨论。比如公式a[i]=vaiv=aa[i] = v\to a\langle i\triangleleft v\rangle = a就不是TAT_A-永真的。

举例:证明以下公式的永真性

F:a[i]=v(j.aiv[j]=a[j])F: a[i]=v\to (\forall j.a\langle i\triangleleft v\rangle [j] = a[j])

2.5.2 性质

  • 不可判定

  • 但是量词自由片段可以判定

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

93
文章数
34
评论数
最近文章
eject