本文主要是介绍程序验证（五）：一阶理论的过程，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！
程序验证（五）：一阶理论的过程
主要讨论 T E T_E TE的量词自由片段以及 T A T_A TA
等价理论的判定
等价及未解释函数理论(Theory of Equality and Uninterpreted Functions)
除=外的谓词实际上使我们的讨论不必要地复杂化，去除这些累赘谓词的方法如下：
- 对每个谓词 p p p，引入一个新的(fresh)函数符号 f p f_p fp
- 引入一个新的常量 ∙ \bullet ∙
- 将每个谓词实例 p ( t 1 , . . . , t n ) p(t_1 ,..., t_n) p(t1,...,tn)替换为 f p ( t 1 , . . . , t n ) = ∙ f_p(t_1 ,..., t_n)=\bullet fp(t1,...,tn)=∙
这样就得到了等价及未解释函数理论(EUF):- EUF中唯一的谓词就是=
- 所有的公理都是相等或不等
转化方法举例：
x = y → ( p ( x ) ↔ p ( y ) ) x=y\to (p(x)\leftrightarrow p(y)) x=y→(p(x)↔p(y))
转化为
x = y → ( ( f p ( x ) = ∙ ) ↔ ( f p ( y ) = ∙ ) ) x=y\to ((f_p (x)=\bullet)\leftrightarrow (f_p (y)=\bullet)) x=y→((fp(x)=∙)↔(fp(y)=∙))
p ( x ) ∧ q ( x , y ) ∧ q ( y , z ) → ¬ q ( x , z ) p(x)\wedge q(x,y)\wedge q(y,z)\to \neg q(x,z) p(x)∧q(x,y)∧q(y,z)→¬q(x,z)
转化为
( f p ( x ) = ∙ ∧ f q ( x , y ) = ∙ ∧ f q ( y , z ) = ∙ ) → f q ( x , z ) ≠ ∙ (f_p(x)=\bullet \wedge f_q(x,y)=\bullet \wedge f_q(y,z)=\bullet) \to f_q(x,z)\ne \bullet (fp(x)=∙∧fq(x,y)=∙∧fq(y,z)=∙)→fq(x,z)=∙
一些概念
关系(relation)
给定 S S S上的二元关系 R R R， ∀ s 1 , s 2 ∈ S \forall s_1,s_2\in S ∀s1,s2∈S，或者 s 1 R s 2 s_1Rs_2 s1Rs2或者 ¬ ( s 1 R s 2 ) \neg (s_1Rs_2) ¬(s1Rs2)
一个二元关系 R R R若满足以下三个性质，即为一个等价关系(equivalence relation)：
- 自反性： ∀ x ∈ S . s R s \forall x\in S.sRs ∀x∈S.sRs
- 对称性： ∀ s 1 , s 2 ∈ S . s 1 R s 2 → s 2 R s 1 \forall s_1,s_2\in S.s_1Rs_2\to s_2Rs_1 ∀s1,s2∈S.s1Rs2→s2Rs1
- 传递性： ∀ s 1 , s 2 , s 3 ∈ S . s 1 R s 2 ∧ s 2 R s 3 → s 1 R s 3 \forall s_1,s_2,s_3\in S.s_1Rs_2 \wedge s_2Rs_3 \to s_1Rs_3 ∀s1,s2,s3∈S.s1Rs2∧s2Rs3→s1Rs3
一个二元关系 R R R是同余关系(congruence relation)，如果它除以上三个性质外，还满足函数同余性： - 函数同余性： ∀ s , t ∈ S n . ( ⋀ i = 1 n s i R t i ) → f ( s ) R f ( t ) \forall s,t \in S^n .(\bigwedge ^n_{i=1} s_iRt_i)\to f(s)Rf(t) ∀s,t∈Sn.(⋀i=1nsiRti)→f(s)Rf(t)
类(class)
令 R R R为 S S S上的一个等价关系，则 s ∈ S s\in S s∈S在 R R R下的等价类(equivalence class)为：
[ s ] R ≡ { s ′ ∈ S : s R s ′ } [s] _R \equiv \{s'\in S:sRs'\} [s]R≡{s′∈S:sRs′}
S S S中的每个元素都属于 R R R的一个等价类
如果 R R R是同余关系，那么 [ s ] R [s]_R [s]R是 s s s的同余类
举例：
Consider the relation ≡ 2 \equiv _2 ≡2 over Z \mathbb{Z} Z, where a ≡ 2 b a\equiv _2 b a≡2b iff ( a m o d 2 ) = ( b m o d 2 ) (a~mod~2)=(b~mod~2) (a mod 2)=(b mod 2)
The equivalence class of 4 under ≡ 2 \equiv_2 ≡2 is:
[ 4 ] ≡ 2 = { n ∈ Z : ( n m o d 2 ) = 0 } = { n ∈ Z : n i s e v e n } [4]_{\equiv_2} = \{n\in \mathbb{Z}: (n~mod~2)=0\}=\{n\in \mathbb{Z} : n~is~even\} [4]≡2={n∈Z:(n mod 2)=0}={n∈Z:n is even}
分割(partition)
S S S的一个分割 P P P是一个 S S S的子集的集合，满足：
- total: ( ⋃ S ′ ∈ P S ′ ) = S (\bigcup _{S'\in P} S')=S (⋃S′∈PS′)=S
- disjoint: ∀ S 1 , S 2 ∈ P . S 1 ≠ S 2 → S 1 ∩ S 2 = ∅ \forall S_1, S_2 \in P.S_1\ne S_2\to S_1 \cap S_2 = \empty ∀S1,S2∈P.S1=S2→S1∩S2=∅
等价关系 R R R 产生了 S S S的一个分割，叫做 S S S除以 R R R的商，也就是
S / R = { [ s ] R : s ∈ S } S/R = \{[s]_R : s\in S\} S/R={[s]R:s∈S}
例如，商 Z / ≡ 2 Z/\equiv_2 Z/≡2即为这个分割：
{ { n ∈ Z : n i s o d d } , { n ∈ Z : n i s e v e n } } \{\{n\in Z :~n~is~odd\},\{n\in Z:~n~is~even\}\} {{n∈Z: n is odd},{n∈Z: n is even}}
关系的精化(refinement)
给定 S S S上两个关系 R 1 R_1 R1和 R 2 R_2 R2，我们说 R 1 R_1 R1精化了 R 2 R_2 R2，写作 R 1 ≺ R 2 R_1 \prec R_2 R1≺R2，如果满足条件：
∀ s 1 , s 2 ∈ S . s 1 R 1 s 2 → s 1 R 2 s 2 \forall s_1, s_2\in S.s_1R_1s_2 \to s_1R_2s_2 ∀s1,s2∈S.s1R1s2→s1R2s2
我们可以把二元关系 R R R视为一个对(pair)的集合 R ^ \hat{R} R^，也就是：
∀ s 1 , s 2 ∈ S , i f s 1 R s 2 , t h e n ( s 1 , s 2 ) ∈ R ^ \forall s_1,s_2 \in S,~if~s_1Rs_2,~then~(s_1,s_2)\in \hat{R} ∀s1,s2∈S, if s1Rs2, then (s1,s2)∈R^
于是我们知道 R 1 ≺ R 2 R_1 \prec R_2 R1≺R2当且仅当 R ^ 1 ⊆ R ^ 2 \hat{R}_1 \subseteq \hat{R}_2 R^1⊆R^2
举例：
R 1 : { s R 1 s : s ∈ S } R_1:\{sR_1s:s\in S\} R1:{sR1s:s∈S}
R 2 : { s 1 R 2 s 2 : s 1 , s 2 ∈ S } R_2:\{s_1R_2s_2:s_1,s_2\in S\} R2:{s1R2s2:s1,s2∈S}
那么
R 1 ≺ R 2 R_1 \prec R_2 R1≺R2
等价闭包(equivalence closure)
一个 S S S上的关系 R R R的等价闭包 R E R^E RE是这样的一个等价关系，满足：
- R R R精化 R E R^E RE: R ≺ R E R\prec R^E R≺RE
- 对于其他满足 R ≺ R ′ R\prec R' R≺R′的等价关系 R ′ R' R′，或者 R ′ = R E R'=R^E R′=RE或者 R E ≺ R ′ R^E \prec R' RE≺R′
也就是说， R E R^E RE是包含 R R R的最小的等价关系
与之相似， R R R的同余闭包(congruence closure) R C R^C RC是包含 R R R的最小同余关系。
等价闭包的构造：一个例子
有一个论域 S = { a , b , c , d } S=\{a,b,c,d\} S={a,b,c,d}，一个关系 R R R满足：
a R b , b R c , d R d aRb,bRc,dRd aRb,bRc,dRd
为了构造 R E R^E RE，根据定义逐步构造：
| 构造 | 依据 |
|---|---|
| ( a , b ) , ( b , c ) , ( d , d ) ∈ R E (a,b),(b,c),(d,d)\in R^E (a,b),(b,c),(d,d)∈RE | R ⊆ R E R\subseteq R^E R⊆RE |
| ( a , a ) , ( b , b ) , ( c , c ) ∈ R E (a,a),(b,b),(c,c)\in R^E (a,a),(b,b),(c,c)∈RE | 自反性 |
| ( b , a ) , ( c , b ) ∈ R E (b,a),(c,b)\in R^E (b,a),(c,b)∈RE | 对称性 |
| ( a , c ) ∈ R E (a,c)\in R^E (a,c)∈RE | 传递性 |
| ( c , a ) ∈ R E (c,a)\in R^E (c,a)∈RE | 对称性 |
最后
R E = { ( a , b ) , ( b , a ) , ( a , a ) , ( b , b ) , ( b , c ) , ( c , a ) , ( c , b ) , ( c , c ) , ( d , d ) } R^E = \{(a,b),(b,a),(a,a),(b,b),(b,c),(c,a),(c,b),(c,c),(d,d)\} RE={(a,b),(b,a),(a,a),(b,b),(b,c),(c,a),(c,b),(c,c),(d,d)}
T E T_E TE的判定
T E T_E TE的量词自由片段是可判定的
核心逻辑
给定一个 T E T_E TE-公式 F F F:
F : ( s 1 = t 1 ) ∧ ⋯ ∧ ( s m = t m ) ∧ ( s m + 1 ≠ t m + 1 ) ∧ ⋯ ∧ ( s n ≠ t n ) F:(s_1 = t_1)\wedge\dots\wedge (s_m = t_m)\wedge(s_{m+1}\ne t_{m+1})\wedge\dots\wedge (s_n \ne t_n) F:(s1=t1)∧⋯∧(sm=tm)∧(sm+1=tm+1)∧⋯∧(sn=tn)
F F F是 T E T_E TE-可满足的，当且仅当存在一个同余关系~，使得：
- 对每个 i ∈ { 1 , … , m } i\in \{1,\dots ,m\} i∈{1,…,m}, s i s_i si ~ t i t_i ti
- 对每个 i ∈ { m + 1 , … , n } i\in \{m+1,\dots ,n\} i∈{m+1,…,n}, s i ̸ s_i \not si~ t i t_i ti
这样一个同余关系定义了 F F F的 T E T_E TE-解释 ( D , I ) (D,I) (D,I): - D D D由~的同余类构成
- I I I将 D D D的元素赋值给 F F F的子项(subterm)来满足~
- I I I赋值了=，一个与~相似的关系
我们把 ( D , I ) ⊨ F (D,I)\models F (D,I)⊨F简记为~ ⊨ F \models F ⊨F
同余闭包算法
令 S F S_F SF为 F F F的子项，~是 S F S_F SF上的关系，那么该算法如下：
- 在子项集合 S F S_F SF上构造 { s 1 = t 1 , … , s + m = t m } \{s_1=t_1,\dots ,s+m=t_m\} {s1=t1,…,s+m=tm}的同余闭包~
- 如果对于任何 i ∈ { m + 1 , … , n } i\in \{m+1,\dots ,n\} i∈{m+1,…,n}， s i s_i si~ t i t_i ti，那么返回 u n s a t unsat unsat
- 否则，返回 s a t sat sat
第一步中，构造同余闭包的方法如下：
- 从“最好”的同余关系开始
~ 0 = { { s } : s ∈ S F } _0 = \{\{s\}:s\in S_F\} 0={{s}:s∈SF}
这里 S F S_F SF每个子项都在它本身构成的同余类里 - 对于每个 i ∈ { 1 , … , m } i\in \{1,\dots , m\} i∈{1,…,m}, 通过把 s i = t i s_i = t_i si=ti加入~ i − 1 _{i-1} i−1 构造~ i _i i
- 将同余类 [ s i ] ∼ i − 1 [s_i]_{\sim _{i-1}} [si]∼i−1和 [ t i ] ∼ i − 1 [t_i]_{\sim _{i-1}} [ti]∼i−1merge起来
- 将任何通过以上步骤产生的新的同余关系传递下去
举例
1
判断以下公式的可满足性：
F : f ( a , b ) = a ∧ f ( f ( a , b ) , b ) ≠ a F: f(a,b) = a\wedge f(f(a,b),b)\ne a F:f(a,b)=a∧f(f(a,b),b)=a
- 建立子项集合 S F S_F SF: S F = { a , b , f ( a , b ) , f ( f ( a , b ) , b ) } S_F = \{a,b,f(a,b),f(f(a,b),b)\} SF={a,b,f(a,b),f(f(a,b),b)}
- 构造 S F S_F SF上的“最好”的闭包关系： { { a } , { b } , { f ( a , b ) } , { f ( f ( a , b ) , b ) } } \{\{a\},\{b\},\{f(a,b)\},\{f(f(a,b),b)\}\} {{a},{b},{f(a,b)},{f(f(a,b),b)}}
- 对于每个 i ∈ { 1 , … , m } i\in \{1,\dots ,m\} i∈{1,…,m}，将同余类 [ s i ] ∼ i − 1 [s_i]_{\sim _{i-1}} [si]∼i−1和 [ t i ] ∼ i − 1 [t_i]_{\sim_{i-1}} [ti]∼i−1merge起来
这里由 f ( a , b ) = a f(a,b) = a f(a,b)=a得到： { { a , f ( a , b ) } , { b } , { f ( f ( a , b ) , b ) } } \{\{a,f(a,b)\},\{b\},\{f(f(a,b),b)\}\} {{a,f(a,b)},{b},{f(f(a,b),b)}} - 每次merge之后，使用公理以推进
由 f ( a , b ) ∼ a , b ∼ b f(a,b)\sim a,b\sim b f(a,b)∼a,b∼b，有 f ( f ( a , b ) , b ) ∼ f ( a , b ) f(f(a,b),b)\sim f(a,b) f(f(a,b),b)∼f(a,b)，从而： { { a , f ( a , b ) , f ( f ( a , b ) , b ) } , { b } } \{\{a,f(a,b),f(f(a,b),b)\},\{b\}\} {{a,f(a,b),f(f(a,b),b)},{b}}
这也就是 S F S_F SF的同余闭包 - F F F是 T E T_E TE-不可满足的，因为 f ( f ( a , b ) , b ) ∼ a f(f(a,b),b)\sim a f(f(a,b),b)∼a而 F F F声称 f ( f ( a , b ) , b ) ≠ a f(f(a,b),b)\ne a f(f(a,b),b)=a
2
判断以下公式的可满足性：
F : f ( f ( f ( a ) ) ) = a ∧ f ( f ( f ( f ( f ( a ) ) ) ) ) = a ∧ f ( a ) ≠ a F:f(f(f(a)))=a\wedge f(f(f(f(f(a)))))=a\wedge f(a)\ne a F:f(f(f(a)))=a∧f(f(f(f(f(a)))))=a∧f(a)=a
- 建立子项集合 S F S_F SF： S F = { a , f ( a ) , f 2 ( a ) , f 3 ( a ) , f 4 ( a ) , f 5 ( a ) } S_F = \{a,f(a),f^2(a),f^3(a),f^4(a),f^5(a)\} SF={a,f(a),f2(a),f3(a),f4(a),f5(a)}
- 构造 S F S_F SF上的初始同余关系： { { a } , { f ( a ) } , { f 2 ( a ) } , { f 3 ( a ) } , { f 4 ( a ) } , { f 5 ( a ) } } \{\{a\},\{f(a)\},\{f^2(a)\},\{f^3(a)\},\{f^4(a)\},\{f^5(a)\}\} {{a},{f(a)},{f2(a)},{f3(a)},{f4(a)},{f5(a)}}
- 由 f 3 ( a ) = a f^3(a) = a f3(a)=a，合并 { f 3 ( a ) } \{f^3(a)\} {f3(a)}和 { a } \{a\} {a}： { { a , f 3 ( a ) } , { f ( a ) } , { f 2 ( a ) } , { f 4 ( a ) } , { f 5 ( a ) } } \{\{a,f^3(a)\},\{f(a)\},\{f^2(a)\},\{f^4(a)\},\{f^5(a)\}\} {{a,f3(a)},{f(a)},{f2(a)},{f4(a)},{f5(a)}}
- 由 f 3 ( a ) ∼ a f^3(a)\sim a f3(a)∼a，推导出 f 4 ( a ) ∼ f ( a ) f^4(a)\sim f(a) f4(a)∼f(a)： { { a , f 3 ( a ) } , { f ( a ) , f 4 ( a ) } , { f 2 ( a ) } , { f 5 ( a ) } } \{\{a,f^3(a)\},\{f(a),f^4(a)\},\{f^2(a)\},\{f^5(a)\}\} {{a,f3(a)},{f(a),f4(a)},{f2(a)},{f5(a)}}
- 由 f 4 ( a ) ∼ f ( a ) f^4(a)\sim f(a) f4(a)∼f(a)，推导出 f 5 ( a ) ∼ f 2 ( a ) f^5(a)\sim f^2(a) f5(a)∼f2(a)： { { a , f 3 ( a ) } , { f ( a ) , f 4 ( a ) } , { f 2 ( a ) , f 5 ( a ) } } \{\{a,f^3(a)\},\{f(a),f^4(a)\},\{f^2(a),f^5(a)\}\} {{a,f3(a)},{f(a),f4(a)},{f2(a),f5(a)}}
- 由 f 5 ( a ) = a f^5(a)=a f5(a)=a，合并 { f 2 ( a ) , f 5 ( a ) } \{f^2(a),f^5(a)\} {f2(a),f5(a)}和 { a , f 3 ( a ) } \{a,f^3(a)\} {a,f3(a)}： { { a , f 2 ( a ) , f 3 ( a ) , f 5 ( a ) } , { f ( a ) , f 4 ( a ) } } \{\{a,f^2(a),f^3(a),f^5(a)\},\{f(a),f^4(a)\}\} {{a,f2(a),f3(a),f5(a)},{f(a),f4(a)}}
- 由 f 3 ( a ) ∼ f 2 ( a ) f^3(a)\sim f^2(a) f3(a)∼f2(a)，推导出 f 4 ( a ) ∼ f 3 ( a ) f^4(a)\sim f^3(a) f4(a)∼f3(a)： { { a , f ( a ) , f 2 ( a ) , f 3 ( a ) , f 4 ( a ) , f 5 ( a ) } } \{\{a,f(a),f^2(a),f^3(a),f^4(a),f^5(a)\}\} {{a,f(a),f2(a),f3(a),f4(a),f5(a)}}
这就是 S F S_F SF的同余闭包 - F F F声称 f ( a ) ≠ a f(a)\ne a f(a)=a，而 f ( a ) ∼ a f(a)\sim a f(a)∼a，所以 u n s a t unsat unsat
实现同余闭包算法的底层算法：并查集
性质
可靠性与完备性：如果同余闭包算法返回 s a t sat sat那么量词自由的 F F F就是 T E − s a t T_E-sat TE−sat的
复杂度： O ( e 2 ) O(e^2) O(e2)（参见并查集算法）
数组的判定理论
核心逻辑
将 T A T_A TA可满足性判定归约为 T E T_E TE可满足性判定
如果一个 Σ Z \Sigma_Z ΣZ-公式 F F F不包含任何写项：
- 将每个数组变量 a a a与一个新的(fresh)函数符号 f a f_a fa关联起来
- 将每个读项 a [ i ] a[i] a[i]替换为 f a ( i ) f_a(i) fa(i)
- 判断并返回得到的公式的 T E T_E TE可满足性
否则，取一个项 a ⟨ i ◃ v ⟩ [ j ] a\langle i\triangleleft v\rangle [j] a⟨i◃v⟩[j]，并分为两种情况： - 将 F [ a ⟨ i ◃ v ⟩ [ j ] ] F[a\langle i\triangleleft v\rangle [j]] F[a⟨i◃v⟩[j]]替换为$F_1:F[v]\wedge i=j
- 将 F [ a ⟨ i ◃ v ⟩ [ j ] ] F[a\langle i\triangleleft v\rangle [j]] F[a⟨i◃v⟩[j]]替换为 F 2 : F [ a [ j ] ] ∧ i ≠ j F_2:F[a[j]]\wedge i\ne j F2:F[a[j]]∧i=j
- 递归地对 F 1 F_1 F1于 F 2 F_2 F2做以上处理。只要有一个分支是 s a t sat sat，那么返回 s a t sat sat
- 否则，返回 u n s a t unsat unsat
举例
判断以下公式的可满足性：
F : i 1 = j ∧ i 1 ≠ i 2 ∧ a [ j ] = v 1 ∧ a ⟨ i 1 ◃ v 1 ⟩ ⟨ i 2 ◃ v 2 ⟩ [ j ] ≠ a [ j ] F:i_1 = j\wedge i_1\ne i_2 \wedge a[j]=v_1 \wedge a\langle i_1 \triangleleft v_1 \rangle \langle i_2 \triangleleft v_2 \rangle [j]\ne a[j] F:i1=j∧i1=i2∧a[j]=v1∧a⟨i1◃v1⟩⟨i2◃v2⟩[j]=a[j]
由 F F F本身知， i 2 ≠ j i_2 \ne j i2=j:
F 2 : i 1 = j ∧ i 1 ≠ i 2 ∧ a [ j ] = v 1 ∧ a ⟨ i 1 ◃ v 1 ⟩ [ j ] ≠ a [ j ] ∧ i 2 ≠ j F_2:i_1=j\wedge i_1\ne i_2\wedge a[j] = v_1\wedge a\langle i_1\triangleleft v_1\rangle [j]\ne a[j]\wedge i_2\ne j F2:i1=j∧i1=i2∧a[j]=v1∧a⟨i1◃v1⟩[j]=a[j]∧i2=j
其中有一个写项，所以分为两种情况：
F 3 : i 1 = j ∧ i 1 ≠ i 2 ∧ a [ j ] = v 1 ∧ v 1 ≠ a [ j ] ∧ i 2 ≠ j ∧ i 1 = j F_3:i_1 =j\wedge i_1\ne i_2 \wedge a[j]=v_1 \wedge v_1\ne a[j]\wedge i_2\ne j\wedge i_1 =j F3:i1=j∧i1=i2∧a[j]=v1∧v1=a[j]∧i2=j∧i1=j
F 4 : i 1 = j ∧ i 1 ≠ i 2 ∧ a [ j ] = v 1 ∧ a [ j ] ≠ a [ j ] ∧ i 2 ≠ j ∧ i 1 ≠ j F_4:i_1=j\wedge i_1\ne i_2\wedge a[j]=v_1 \wedge a[j]\ne a[j]\wedge i_2\ne j\wedge i_1\ne j F4:i1=j∧i1=i2∧a[j]=v1∧a[j]=a[j]∧i2=j∧i1=j
二者都是不可满足的
所有的分支都是 u n s a t unsat unsat，所以得出结论： F F F是 T A T_A TA-不可满足的
性质
可靠性与完备性：给定一个 Σ A \Sigma_A ΣA公式 F F F，以上判定算法返回 s a t sat sat当且仅当 F F F是 T A T_A TA-可满足的，否则，它返回 u n s a t unsat unsat
复杂度：这是一个NP完全问题。
这篇关于程序验证（五）：一阶理论的过程的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！
