数组理论"/>
形式化13：数组理论
数组理论(Arrays)
语法
E : : = x ∣ E [ E ] ∣ s t o r e ( E , E , E ) R : : = E = E ∣ E ≠ E P : : = R ∣ ¬ P ∣ P ∧ P \begin{align} E::=&\ x\ |\ E[E]\ |\ store(E,E,E) \\ R::=&\ E=E\ |\ E\ne E \\ P::=&\ R \\ |&\ \neg P \\ |&\ P\land P \end{align} E::=R::=P::=∣∣ x ∣ E[E] ∣ store(E,E,E) E=E ∣ E=E R ¬P P∧P
上面的语法中 E [ E ] E[E] E[E]表示读取数组, s t r o e ( E , E , E ) stroe(E,E,E) stroe(E,E,E)则是将数组的写入进行了函数式化,在函数式程序中,数组是不可变的,因此写入操作会返回一个新构造的数组,在数组推理中，证明器总会把命令程序先转换成函数式程序，对命令式程序的推理则转换成了等价的对函数式程序的推理。
例如,有如下的交换程序,我们要证明交换是正确的:
void swap(int[] A, int i, int j) {int tmp = A[i];A[i] = A[j];A[j] = tmp;
}
由于函数式程序中,数组是不可变的,因此如果写入的话就需要一个新的变量接收:
A' = store(A, i, x);
这样的话,我们可以将上面的代码改写为:
A' = store(store(A, i, A[j]), j, A[i])
要证明的命题为:
A'[i]==A[j] /\ A'[j]==A[i]
转换规则
A = B i = j A [ i ] = B [ j ] ( I n d e x ) i = j S t o r e ( A , i , x ) [ j ] = x ( R A W 1 ) i ≠ j S t o r e ( A , i , x ) [ j ] = A [ j ] ( R A W 2 ) ∀ i . A [ i ] = B [ i ] A = B ( E x t e n s i o n a l i t y ) \begin{align} &\cfrac{A=B \qquad i=j}{A[i]=B[j]}(Index) \\ \\ &\cfrac{i=j}{Store(A,i,x)[j]=x}(RAW1) \\ \\ &\cfrac{i\ne j}{Store(A,i,x)[j]=A[j]}(RAW2) \\ \\ &\cfrac{\forall i.A[i]=B[i]}{A=B}(Extensionality) \end{align} A[i]=B[j]A=Bi=j(Index)Store(A,i,x)[j]=xi=j(RAW1)Store(A,i,x)[j]=A[j]i=j(RAW2)A=B∀i.A[i]=B[i](Extensionality)
数组的决策过程
- 将数组看作一个函数, A → F A A\to F_A A→FA,则 A [ i ] → F A ( i ) A[i] \to F_A(i) A[i]→FA(i),这样基本的一些逻辑就可以转换为EUF理论,例如
i = j ∧ A [ i ] ≠ A [ i ] ⟶ i = j ∧ F A ( i ) ≠ F A ( j ) i=j \land A[i] \ne A[i]\quad \longrightarrow \quad i=j\land F_A(i) \ne F_A(j) i=j∧A[i]=A[i]⟶i=j∧FA(i)=FA(j) - 对于数组的更新,引入一个新的数组标识 A ′ A' A′,这样就得到了如下转换:
A [ i ] = x ⟶ A ′ [ i ] = = x ∧ ∀ j ≠ i . A ′ [ j ] = = A [ j ] A[i]=x\quad \longrightarrow \quad A'[i]==x\ \land \ \forall j \ne i.A'[j]==A[j] A[i]=x⟶A′[i]==x ∧ ∀j=i.A′[j]==A[j]
例如:
s t o r e ( A , i , x ) [ i ] ≥ x ⟹ A ′ [ i ] = x ∧ ( ∀ j ≠ i . A ′ [ j ] = = A [ j ] ) → A ′ [ i ] ≥ x ⟹ F A ′ ( i ) = x ∧ ( ∀ j ≠ i . A ′ [ j ] = = A [ j ] ) → F A ′ ( i ) ≥ x \begin{align} &store(A,i,x)[i] \ge x \\ \implies \quad &A'[i]=x\ \land \ (\forall j \ne i.A'[j]==A[j]) \to A'[i] \ge x \\ \implies \quad &F_{A'}(i)=x \land (\forall j \ne i.A'[j]==A[j]) \to F_{A'}(i) \ge x \end{align} ⟹⟹store(A,i,x)[i]≥xA′[i]=x ∧ (∀j=i.A′[j]==A[j])→A′[i]≥xFA′(i)=x∧(∀j=i.A′[j]==A[j])→FA′(i)≥x
但是,如果上面的式子变为 s t o r e ( A , i × i − i × i , x ) [ i ] ≥ x store(A,i\times i-i\times i,x)[i] \ge x store(A,i×i−i×i,x)[i]≥x,一般来说,对于高阶的结果是不可判定的！但是在某种限制下还是可解的。以下是进行限制后的语法
I : : = x ∣ c ∣ c × x ∣ I + I E : : = x ∣ x [ I ] ∣ s t o r e ( x , I , E ) R : : = E = E ∣ E ≠ E P : : = R ∣ ¬ P ∣ P ∧ P \begin{align} I::=&\ x\ |\ c\ |\ c\times x\ |\ I+I \\ E::=&\ x\ |\ x[I]\ |\ store(x,I,E) \\ R::=&\ E=E\ |\ E\ne E \\ P::=&\ R \\ |&\ \neg P \\ |&\ P\land P \end{align} I::=E::=R::=P::=∣∣ x ∣ c ∣ c×x ∣ I+I x ∣ x[I] ∣ store(x,I,E) E=E ∣ E=E R ¬P P∧P
上面将原来的 E [ E ] E[E] E[E]转化为了 x [ I ] x[I] x[I],一来限制了下标 I I I为一阶,二来限制了数组必须为原子变量
数组属性片段(array property fragment)
描述了推理Array数组相关性质时，能够出现的逻辑命题的形式是什么。必须具有如下的形式:
∀ j . G ( i ) → V ( i ) 其中 : G : : = G ∧ G ∣ G ∨ G ∣ A A : : = I = I ∣ I ≠ I ∣ T \begin{align} &\forall j.G(i) \to V(i) \\ 其中:& \\ &G::=G\land G|G \lor G|A \\ &A::=I=I|I\ne I|T \end{align} 其中:∀j.G(i)→V(i)G::=G∧G∣G∨G∣AA::=I=I∣I=I∣T
数组消除算法
// 输入满足数组属性形式的命题将其转换为等价的EUF形式
EUF arrayReduction(P){ P1 = eliminate all array write: store(A, i, x); P2 = replace ∃x.P1(x) with P1(y); // 将x替换为一个新变量yP3 = replace ∀x.P2(x) with P2(i)/\.../\P2(k); P4 = eliminate array read in P3: A[i]; return P4;
}
示例1:
s t o r e ( A , i , x ) [ i ] ≥ x store(A,i,x)[i] \ge x store(A,i,x)[i]≥x
-
消除 s t o r e store store
A ′ [ i ] = x ∧ ( ∀ j ∈ N . j ≠ i → A ′ [ j ] = A [ j ] ) → A ′ [ i ] ≥ x A'[i]=x \land (\forall j \in \mathbb{N}.j\ne i \to A'[j]=A[j]) \to A'[i]\ge x A′[i]=x∧(∀j∈N.j=i→A′[j]=A[j])→A′[i]≥x
证明命题 P P P的SAT,等同于证明 ¬ P \neg P ¬P的UNSAT,因此根据否定范式处提到的转化规则:¬ ( A → B ) ⟹ ¬ ( ¬ A ∨ B ) 转化式 : C ( P → Q ) = ∼ C ( P ) ∨ C ( Q ) : ⟹ ¬ ¬ A ∧ ¬ B 转化式 : C ( ∼ ( P ∨ Q ) ) = C ( ∼ P ) ∧ C ( ∼ Q ) ⟹ A ∧ ¬ B \begin{align} &\neg (A\to B) \\ \implies &\neg(\neg A\lor B) \quad 转化式:C(P \to Q) = \sim C(P)\lor C(Q):\\ \implies &\neg \neg A\land \neg B \quad 转化式:C(\sim (P\lor Q)) = C(\sim P)\land C(\sim Q)\\ \implies &A\land \neg B \end{align} ⟹⟹⟹¬(A→B)¬(¬A∨B)转化式:C(P→Q)=∼C(P)∨C(Q):¬¬A∧¬B转化式:C(∼(P∨Q))=C(∼P)∧C(∼Q)A∧¬B
将上式中的式子代入 A , B A,B A,B就得到:
A ′ [ i ] = x ∧ ( ∀ j ∈ N . j ≠ i → A ′ [ j ] = A [ j ] ) ∧ A ′ [ i ] < x A'[i]=x \land (\forall j \in \mathbb{N}.j\ne i \to A'[j]=A[j]) \land A'[i]< x A′[i]=x∧(∀j∈N.j=i→A′[j]=A[j])∧A′[i]<x -
参照代码消除 ∃ \exists ∃,本式中不存在
-
参照代码消除 ∀ \forall ∀,对于上述命题来说,索引集合为 { i } \{i\} {i},
A ′ [ i ] = x ∧ ( i ≠ i → A ′ [ i ] = A [ i ] ) ∧ A ′ [ i ] < x A'[i]=x\land (i\ne i\to A'[i]=A[i])\land A'[i]<x A′[i]=x∧(i=i→A′[i]=A[i])∧A′[i]<x
简化为
A ′ [ i ] = x ∧ A ′ [ i ] < x A'[i]=x\land A'[i]<x A′[i]=x∧A′[i]<x -
消除数组读取 A ′ [ i ] → F A ′ ( i ) A'[i] \to F_{A'}(i) A′[i]→FA′(i)
F A ( i ) = x ∧ F A ( i ) < x F_A(i)=x\land F_A(i)<x FA(i)=x∧FA(i)<x
很容易就能检查得到上面的命题是UNSAT的,因此原命题为真!
示例2:
( ∀ x ∈ N . x < i → A [ x ] = 0 ) ∧ A ′ = s t o r e ( A , i , 0 ) → ( ∀ x ∈ N . x ≤ i → A ′ [ x ] = 0 ) (\forall x \in N.x<i \to A[x]=0)\land A'=store(A,i,0) \to (\forall x \in N.x \le i \to A'[x]=0) (∀x∈N.x<i→A[x]=0)∧A′=store(A,i,0)→(∀x∈N.x≤i→A′[x]=0)
- 简化式子为规定的形式(上例中先消除再简化,其实顺序是无所谓的):证明原式SAT,等同于证明下面的式子UNSAT
( ∀ x ∈ N . x < i → A [ x ] = 0 ) ∧ A ′ = s t o r e ( A , i , 0 ) ∧ ( ∃ x ∈ N . x ≤ i → A ′ [ x ] ≠ 0 ) (\forall x \in N.x<i \to A[x]=0)\land A'=store(A,i,0) \land (\exists x \in N.x \le i \to A'[x]\ne 0) (∀x∈N.x<i→A[x]=0)∧A′=store(A,i,0)∧(∃x∈N.x≤i→A′[x]=0) - 消除 s t o r e store store:
( ∀ x ∈ N . x < i → A [ x ] = 0 ) ∧ ( A ′ [ i ] = 0 ∧ ∀ j ≠ i . A ′ [ j ] = A [ j ] ) ∧ ( ∃ x ∈ N . x ≤ i → A ′ [ x ] ≠ 0 ) \begin{align} &(\forall x \in N.x<i \to A[x]=0)\land \\ &(A'[i]=0\land \forall j\ne i.A'[j]=A[j]) \land \\ &(\exists x \in N.x \le i \to A'[x]\ne 0) \end{align} (∀x∈N.x<i→A[x]=0)∧(A′[i]=0∧∀j=i.A′[j]=A[j])∧(∃x∈N.x≤i→A′[x]=0) - 消除 ∃ \exists ∃:将 x x x替换为 z z z:
( ∀ x ∈ N . x < i → A [ x ] = 0 ) ∧ ( A ′ [ i ] = 0 ∧ ∀ j ≠ i . A ′ [ j ] = A [ j ] ) ∧ ( z ≤ i ∧ A ′ [ z ] ≠ 0 ) \begin{align} &(\forall x \in N.x<i \to A[x]=0)\land \\ &(A'[i]=0\land \forall j\ne i.A'[j]=A[j]) \land \\ &(z \le i \land A'[z]\ne 0) \end{align} (∀x∈N.x<i→A[x]=0)∧(A′[i]=0∧∀j=i.A′[j]=A[j])∧(z≤i∧A′[z]=0) - 消除 ∀ \forall ∀,索引集合为 { i , z } \{i,z\} {i,z},按照代码转换为索引集合的并集:
( i < i → A [ i ] = 0 ) ∧ ( z < i → A [ z ] = 0 ) ∧ ( A ′ [ i ] = 0 ∧ i ≠ i → A ′ [ i ] = A [ i ] ∧ z ≠ i → A ′ [ z ] = A [ z ] ) ∧ ( z ≤ i ∧ A ′ [ z ] ≠ 0 ) \begin{align} &(i<i \to A[i]=0)\land (z<i \to A[z]=0)\land \\ &(A'[i]=0\land i\ne i\to A'[i]=A[i] \land z\ne i\to A'[z]=A[z]) \land \\ &(z \le i \land A'[z]\ne 0) \end{align} (i<i→A[i]=0)∧(z<i→A[z]=0)∧(A′[i]=0∧i=i→A′[i]=A[i]∧z=i→A′[z]=A[z])∧(z≤i∧A′[z]=0)
由于假可以推出一切 Γ ⊢ ⊥ Γ ⊢ P ( ⊥ E ) \frac{\Gamma \vdash \bot}{\Gamma \vdash P}(\bot E) Γ⊢PΓ⊢⊥(⊥E),因此上面的命题中 i < i → A [ i ] = 0 i<i \to A[i]=0 i<i→A[i]=0 等,由于 i < i i<i i<i必为假,因此这条命题必为真,因此上面的命题可以简化为:
( z < i → A [ z ] = 0 ) ∧ ( A ′ [ i ] = 0 ∧ z ≠ i → A ′ [ z ] = A [ z ] ) ∧ ( z ≤ i ∧ A ′ [ z ] ≠ 0 ) \begin{align} &(z<i \to A[z]=0)\land \\ &(A'[i]=0\land z\ne i\to A'[z]=A[z]) \land \\ &(z \le i \land A'[z]\ne 0) \end{align} (z<i→A[z]=0)∧(A′[i]=0∧z=i→A′[z]=A[z])∧(z≤i∧A′[z]=0) - 消除数组读取 A ′ [ i ] → F A ′ ( i ) A'[i] \to F_{A'}(i) A′[i]→FA′(i)
( z < i → F A ( z ) = 0 ) ∧ ( F A ′ ( i ) = 0 ∧ z ≠ i → F A ′ ( z ) = F A ( z ) ) ∧ ( z ≤ i ∧ F A ′ ( z ) ≠ 0 ) \begin{align} &(z<i \to F_{A}(z)=0)\land \\ &(F_{A'}(i)=0\land z\ne i\to F_{A'}(z)=F_{A}(z)) \land \\ &(z \le i \land F_{A'}(z)\ne 0) \end{align} (z<i→FA(z)=0)∧(FA′(i)=0∧z=i→FA′(z)=FA(z))∧(z≤i∧FA′(z)=0)
哈希表
哈希表的接口类似于数组:
// array // hash table
read(A, i); -> lookup(H, k);
store(A, i, x); -> update(H, k, v);
这意味着我们可以利用和数组相似的方法设计理论验证
更多推荐
形式化13：数组理论
发布评论