Home

日月如百代过客，去而复返，返而复去。艄公穷生涯于船头；马夫引缰辔迎来老年，日日羁旅，随处栖身。

# IMP 的指称语义

# 目的

我们可以用状态集合上的部分函数来表示命令的指称，并称这种新的语义描述风格为指称语义。

以 IMP 语言为例：

  • 算术表达式a∈Aexpa\in Aexp 的指称函数A[a]:Σ→N\mathscr{A}[a]:\Sigma\rightarrow N
  • 布尔表达式b∈Bexpb\in Bexp 的指称函数B[b]:Σ→T\mathscr{B}[b]:\Sigma\rightarrow T
  • 命令c∈Comc\in Com 指称部分函数C[c]:Σ→Σ\mathscr{C}[c]:\Sigma\rightarrow\Sigma

注：方括号应该都为 “空心方括号”，但因为我打不出来 emm… 特此说明，后文也是。

空心方括号是指称语义的一个常用符号。A\mathscr{A} 实际上是类型为Aexp→(Σ→N)Aexp\rightarrow(\Sigma\rightarrow N) 的算术表达式的一个函数。

# 指称语义

  • 用结构归纳法定义语义函数

A:Aexp→(Σ→N)B:Bexp→(Σ→T)C:Com→(Σ→Σ)\mathscr{A}:Aexp\rightarrow(\Sigma\rightarrow N)\\ \mathscr{B}:Bexp\rightarrow(\Sigma\rightarrow T)\\ \mathscr{C}:Com\rightarrow(\Sigma\rightarrow\Sigma)

  • 对于命令，当我们给每条命令cc 定义一个部分函数C[c]\mathscr{C}[c] 时，都是假定 c 的子命令c′c' 已有定义。在定义C[c0;c1]\mathscr{C}[c_0;c_1] 时需先定义C[c0],C[c1]\mathscr{C}[c_0],\mathscr{C}[c_1]。称命令 c 指称C[c]\mathscr{C}[c]，或称C[c]\mathscr{C}[c] 是 c 的指称。

# 算术表达式的指称

结构归纳法定义：

A[n]={(σ,n)∣σ∈Σ}A[X]={(σ,σ(X)∣σ∈Σ}A[a0+a1]={(σ,n0−n1)∣(σ,n0)∈A[a0]&(σ,n1)∈A[a1]}A[a0−a1]={(σ,n0+n1)∣(σ,n0)∈A[a0]&(σ,n1)∈A[a1]}A[a0×a1]={(σ,n0×n1)∣(σ,n0)∈A[a0]&(σ,n1)∈A[a1]}\mathscr{A}[n]=\{(\sigma,n)|\sigma\in \Sigma\}\\ \mathscr{A}[X]=\{(\sigma,\sigma(X)|\sigma\in\Sigma\}\\ \mathscr{A}[a_0+a_1]=\{(\sigma,n_0-n_1)|(\sigma,n_0)\in\mathscr{A}[a_0]\&(\sigma,n_1)\in\mathscr{A}[a_1]\}\\ \mathscr{A}[a_0-a_1]=\{(\sigma,n_0+n_1)|(\sigma,n_0)\in\mathscr{A}[a_0]\&(\sigma,n_1)\in\mathscr{A}[a_1]\}\\ \mathscr{A}[a_0\times a_1]=\{(\sigma,n_0\times n_1)|(\sigma,n_0)\in\mathscr{A}[a_0]\&(\sigma,n_1)\in\mathscr{A}[a_1]\}\\

因为每个指称输出是一个函数，也可以用 lambda 表达法重写定义：

A[n]=λσ∈Σ.nA[X]=λσ∈Σ.σ(X)A[a0+a1]=λσ∈Σ.(A[a0]σ+A[a1]σ)A[a0−a1]=λσ∈Σ.(A[a0]σ−A[a1]σ)A[a0×a1]=λσ∈Σ.(A[a0]σ×A[a1]σ)\mathscr{A}[n]=\lambda\sigma\in\Sigma.n\\ \mathscr{A}[X]=\lambda\sigma\in\Sigma.\sigma(X)\\ \mathscr{A}[a_0+a_1]=\lambda\sigma\in\Sigma.(\mathscr{A}[a_0]\sigma+\mathscr{A}[a_1]\sigma)\\ \mathscr{A}[a_0-a_1]=\lambda\sigma\in\Sigma.(\mathscr{A}[a_0]\sigma-\mathscr{A}[a_1]\sigma)\\ \mathscr{A}[a_0\times a_1]=\lambda\sigma\in\Sigma.(\mathscr{A}[a_0]\sigma\times\mathscr{A}[a_1]\sigma)\\

# 布尔表达式的指称

B[true]={(σ,true)∣σ∈Σ}B[false]={(σ,false)∣σ∈Σ}B[a0=a1]={(σ,true)∣σ∈Σ,A[a0]σ=A[a1]σ}∪{(σ,false)∣σ∈Σ,A[a0]σ≠A[a1]σ}B[a0≤a1]={(σ,true)∣σ∈Σ,A[a0]σ≤A[a1]σ}∪{(σ,false)∣σ∈Σ,A[a0]σ>A[a1]σ}B[¬b]={(σ,¬t)∣σ∈Σ,(σ,t)∈B[b]}B[b0∧b1]={(σ,t0∧t1)∣σ∈Σ,(σ,t0)∈B[b0],(σ,t1)∈B[b1]}B[b0∨b1]={(σ,t0∨t1)∣σ∈Σ,(σ,t0)∈B[b0],(σ,t1)∈B[b1]}\mathscr{B}[true]=\{(\sigma,true)|\sigma\in\Sigma\}\\ \mathscr{B}[false]=\{(\sigma,false)|\sigma\in\Sigma\}\\ \mathscr{B}[a_0=a_1]=\{(\sigma,true)|\sigma\in\Sigma,\mathscr{A}[a_0]\sigma=\mathscr{A}[a_1]\sigma\}\cup\{(\sigma,false)|\sigma\in\Sigma,\mathscr{A}[a_0]\sigma\neq\mathscr{A}[a_1]\sigma\}\\ \mathscr{B}[a_0\leq a_1]=\{(\sigma,true)|\sigma\in\Sigma,\mathscr{A}[a_0]\sigma\leq\mathscr{A}[a_1]\sigma\}\cup\{(\sigma,false)|\sigma\in\Sigma,\mathscr{A}[a_0]\sigma>\mathscr{A}[a_1]\sigma\}\\ \mathscr{B}[\neg b]=\{(\sigma,\neg t)|\sigma\in\Sigma,(\sigma,t)\in\mathscr{B}[b]\}\\ \mathscr{B}[b_0\wedge b_1]=\{(\sigma,t_0\wedge t_1)|\sigma\in\Sigma,(\sigma,t_0)\in\mathscr{B}[b_0],(\sigma,t_1)\in\mathscr{B}[b_1]\}\\ \mathscr{B}[b_0\vee b_1]=\{(\sigma,t_0\vee t_1)|\sigma\in\Sigma,(\sigma,t_0)\in\mathscr{B}[b_0],(\sigma,t_1)\in\mathscr{B}[b_1]\}

注：A[a]σ\mathscr{A}[a]\sigma 其实就是状态σ\sigma 下对aa 求值。因为A[a]\mathscr{A}[a] 是一个输入为σ\sigma 的函数，输出为对应状态下表达式的值。

# 命令的指称

C[skip]={(σ,σ)∣σ∈Σ}C[X:=a]={(σ,σ[n/X])∣σ∈Σ,n=A[a]σ}C[c0;c1]=C[c1]∘C[c0](复合函数)C[if  b  then  c0  else  c1]={(σ,σ′)∣B[b]σ=true,(σ,σ′)∈C[c0]}∪{(σ,σ′)∣B[b]σ=false,(σ,σ′)∈C[c1]}\mathscr{C}[skip]=\{(\sigma,\sigma)|\sigma\in\Sigma\}\\ \mathscr{C}[X:=a]=\{(\sigma,\sigma[n/X])|\sigma\in \Sigma,n=\mathscr{A}[a]\sigma\}\\ \mathscr{C}[c_0;c_1]=\mathscr{C}[c_1]\circ\mathscr{C}[c_0](复合函数)\\ \mathscr{C}[if\;b\;then\;c_0\;else\;c_1]=\{(\sigma,\sigma')|\mathscr{B}[b]\sigma=true,(\sigma,\sigma')\in\mathscr{C}[c_0]\}\cup\{(\sigma,\sigma')|\mathscr{B}[b]\sigma=false,(\sigma,\sigma')\in\mathscr{C}[c_1]\}\\

然后单独考虑下w≡while  b  do  cw\equiv while\;b\;do\;c 的情况，这个比较麻烦。首先有w∼if  b  then  c;w  else  skipw\sim if\;b\;then\;c;w\;else\;skip。于是根据条件命令的指称，我们有：

C[w]={(σ,σ′)∣B[b]σ=true,(σ,σ′)∈C[c;w]}∪{(σ,σ)∣B[b]σ=false}={(σ,σ′)∣B[b]σ=true,(σ,σ′)∈C[w]∘C[c]}∪{(σ,σ)∣B[b]σ=false}\mathscr{C}[w]=\{(\sigma,\sigma')|\mathscr{B}[b]\sigma=true,(\sigma,\sigma')\in\mathscr{C}[c;w]\}\cup\\ \{(\sigma,\sigma)|\mathscr{B}[b]\sigma=false\}\\ =\{(\sigma,\sigma')|\mathscr{B}[b]\sigma=true,(\sigma,\sigma')\in\mathscr{C}[w]\circ\mathscr{C}[c]\}\cup\\ \{(\sigma,\sigma)|\mathscr{B}[b]\sigma=false\}

用φ\varphi 表示C[w]\mathscr{C}[w]，β\beta 表示B[b]\mathscr{B}[b]，γ\gamma 表示C[c]\mathscr{C}[c]，于是有：

φ={(σ,σ′)∣β(σ)=true,(σ,σ′)∈φ∘γ}∪{(σ,σ)∣β(σ)=false}\varphi=\{(\sigma,\sigma')|\beta(\sigma)=true,(\sigma,\sigma')\in\varphi\circ\gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}

这其实是一个递归方程。我们其实可以构造一个集合算子Γ\Gamma，使得：

Γ(f)={(σ,σ′)∣β(σ)=true,(σ,σ′)∈f∘γ}∪{(σ,σ)∣β(σ)=false}={(σ,σ′)∣∃σ′′,β(σ)=true,(σ,σ′′)∈γ,(σ′′,σ′)∈f}∪{(σ,σ)∣β(σ)=false}\Gamma(f)=\{(\sigma,\sigma')|\beta(\sigma)=true,(\sigma,\sigma')\in f\circ\gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}\\ =\{(\sigma,\sigma')|\exists\sigma'',\beta(\sigma)=true,(\sigma,\sigma'')\in\gamma,(\sigma'',\sigma')\in f\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}

然后显然有Γ(φ)=φ\Gamma(\varphi)=\varphi，其实我们求解φ\varphi 就是在求算子Γ\Gamma 的一个不动点。考虑命令规则示例集合RR：

（一个具体确定状态实例到另一个具体确定状态实例的映射就是命令实例）

R={{(σ′′,σ′)}(σ,σ′)∣β(σ)=true,(σ,σ′′)∈γ}∪{∅(σ,σ)∣β(σ)=false}R=\{\frac{\{(\sigma'',\sigma')\}}{(\sigma,\sigma')}|\beta(\sigma)=true,(\sigma,\sigma'')\in\gamma\}\cup\{\frac{\emptyset}{(\sigma,\sigma)}|\beta(\sigma)=false\}

然后可以发现，R^(B)={y∣∃X⊆B,(X/y)∈R}\hat{R}(B)=\{y|\exists X\subseteq B,(X/y)\in R\}，所以

R^(f)={(σ,σ′)∣∃σ′′,(σ′′,σ′)∈f,(σ,σ′′)∈γ}∪{(σ,σ)∣β(σ)=false}=Γ(f)\hat{R}(f)=\{(\sigma,\sigma')|\exists \sigma'',(\sigma'',\sigma')\in f,(\sigma,\sigma'')\in \gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}\\ =\Gamma(f)

所以实际上，R^=Γ\hat{R}=\Gamma，然后我们讨论过R^\hat{R} 的最小不动点。我们定义：(基于C[c]\mathscr{C}[c] 已知)

C[while  b  do  c]=fix(Γ)=fix(R^)=IR\mathscr{C}[while\;b\;do\;c]=fix(\Gamma)=fix(\hat{R})=I_R

其中，Γ(f)={(σ,σ′)∣β(σ)=true,(σ,σ′)∈f∘γ}∪{(σ,σ)∣β(σ)=false}\Gamma(f)=\{(\sigma,\sigma')|\beta(\sigma)=true,(\sigma,\sigma')\in f\circ\gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}。

# 语义的等价性

  • 引理：对所有的a∈Aexpa\in Aexp，有

    A[a]={(σ,n)∣⟨a,σ⟩→n}\mathscr{A}[a]=\{(\sigma,n)|\lang a,\sigma\rang\rightarrow n\}

    对所有的b∈Bexpb\in Bexp，有

    B[b]={(σ,t)∣⟨b,σ⟩→t}\mathscr{B}[b]=\{(\sigma,t)|\lang b,\sigma\rang\rightarrow t\}

    可以用规则 / 结构归纳法证明。

  • 引理：对所有的命令 c 和状态σ,σ′\sigma,\sigma'，有

    ⟨c,σ⟩→σ′⇒(σ,σ′)∈C[c]\lang c,\sigma\rang\rightarrow\sigma'\Rightarrow(\sigma,\sigma')\in\mathscr{C}[c]

    证明：定义性质 P：

    P(c,σ,σ′)⇔⟨c,σ⟩→σ′⇒(σ,σ′)∈C[c]P(c,\sigma,\sigma')\Leftrightarrow\lang c,\sigma\rang\rightarrow\sigma'\Rightarrow(\sigma,\sigma')\in\mathscr{C}[c]

    根据规则归纳法，我们希望证明规则保持了性质 P。

    • c≡c0;c1c\equiv c_0;c_1，引入前提：

      ⟨c0,σ⟩→σ′′&P(c0,σ,σ′′)&⟨c1,σ′′⟩→σ′&P(c1,σ′′,σ′)\lang c_0,\sigma\rang\rightarrow \sigma''\& P(c_0,\sigma,\sigma'')\&\lang c_1,\sigma''\rang\rightarrow\sigma'\&P(c_1,\sigma'',\sigma')

      然后有

      (σ,σ′′)∈C[c0],(σ′′,σ′)∈C[c1](\sigma,\sigma'')\in\mathscr{C}[c_0],(\sigma'',\sigma')\in\mathscr{C}[c_1]

      所以

      (σ,σ′)=(σ′′,σ′)∘(σ,σ′′)∈C[c1]∘C[c0]∈C[c0;c1](\sigma,\sigma')=(\sigma'',\sigma')\circ(\sigma,\sigma'')\in\mathscr{C}[c_1]\circ\mathscr{C}[c_0]\in\mathscr{C}[c_0;c_1]

    • 其他情况类似

    • 再讨论下w≡while  b  do  cw\equiv while\;b\;do\;c，条件为真的情况。引入前提：

      ⟨b,σ⟩→true&⟨c,σ⟩→σ′′&P(c,σ,σ′′)&⟨w,σ′′⟩→σ′&P(w,σ′′,σ′)\lang b,\sigma\rang\rightarrow true\&\lang c,\sigma\rang\rightarrow\sigma''\& P(c,\sigma,\sigma'')\&\lang w,\sigma''\rang\rightarrow\sigma'\& P(w,\sigma'',\sigma')

      根据前提和性质，推得：

      (σ,σ′′)∈C[c],(σ′′,σ′)∈C[w](\sigma,\sigma'')\in\mathscr{C}[c],(\sigma'',\sigma')\in\mathscr{C}[w]

      即

      B[b]σ=true,C[c]σ=σ′′,C[w]σ′′=σ′\mathscr{B}[b]\sigma=true,\mathscr{C}[c]\sigma=\sigma'',\mathscr{C}[w]\sigma''=\sigma'

      再由指称语义的定义，有

      C[if  b  then  c;w  else  skip]σ=σ′(σ,σ′)∈C[if  b  then  c;w  else  skip]\mathscr{C}[if\;b\;then\;c;w\;else\;skip]\sigma=\sigma'\\ (\sigma,\sigma')\in \mathscr{C}[if\;b\;then\;c;w\;else\;skip]

      于是有(σ,σ′)∈C[w](\sigma,\sigma')\in \mathscr{C}[w]，即保持了性质。证毕。

  • 事实上，有：

    A[a]={(σ,n)∣⟨a,σ⟩→a}B[b]={(σ,t)∣⟨b,σ⟩→t}C[c]={(σ,σ′)∣⟨c,σ⟩→σ′}\mathscr{A}[a]=\{(\sigma,n)|\lang a,\sigma\rang\rightarrow a\}\\ \mathscr{B}[b]=\{(\sigma,t)|\lang b,\sigma\rang\rightarrow t\}\\ \mathscr{C}[c]=\{(\sigma,\sigma')|\lang c,\sigma\rang\rightarrow \sigma'\}

    这用定义 + 归纳法都能证明。

# 完全偏序与连续函数

我们引入更抽象的概念 —— 完全偏序和连续函数来定义递归，两者都是指称语义的标准工具。

  • 设 R 为形为X/yX/y 的一组规则实例，给定集合 B，有算子R^\hat{R}：

    R^(B)={y∣∃(X/y)∈R,X⊆B}\hat{R}(B)=\{y|\exists (X/y)\in R,X\subseteq B\}

    以及考察如何用集合链

    ∅⊆R^(∅)⊆R^2(∅)⊆...⊆R^n(∅)⊆...\emptyset\subseteq\hat{R}(\emptyset)\subseteq\hat{R}^2(\emptyset)\subseteq...\subseteq\hat{R}^n(\emptyset)\subseteq...

    的并集得到算子R^\hat{R} 的最小不动点

    fix(R^)=⋃n∈ωR^n(∅)fix(\hat{R})=\bigcup_{n\in\omega}\hat{R}^n(\emptyset)

  • 定义，如果集合 P 上的二元关系⊑\sqsubseteq 满足：

    • 自反性：∀p∈P,p⊑p\forall p\in P,p\sqsubseteq p
    • 传递性：∀p,q,r∈P,p⊑q&q⊑r⇒p⊑r\forall p,q,r\in P,p\sqsubseteq q\&q\sqsubseteq r\Rightarrow p\sqsubseteq r
    • 反对称性：∀p,q∈P,p⊑q&q⊑p⇒p=q\forall p,q\in P,p\sqsubseteq q\& q\sqsubseteq p\Rightarrow p=q

    则称集合(P,⊑)(P,\sqsubseteq) 是一个偏序。

  • 定义，对于偏序(P,⊑)(P,\sqsubseteq) 和子集X⊆PX\subseteq P，称 p 是XX 的上界，当且仅当：

    ∀q∈X,q⊑p\forall q\in X,q\sqsubseteq p

    称 p 是 X 的最小上界，当且仅当：

    • p 是 X 的上界
    • 对于所有 X 的上界qq，有p⊑qp\sqsubseteq q。

    记 X 的最小上界为⨆X\bigsqcup X

  • 定义，设(D,⊑D)(D,\sqsubseteq_D) 是一个偏序。该偏序的ω\omega 链是其元素的递增链：

    d0⊑Dd1⊑D...⊑Ddn⊑D...d_0\sqsubseteq_D d_1\sqsubseteq_D...\sqsubseteq_D d_n\sqsubseteq_D...

    如果对于所有的ω\omega 链都有一个在 D 中的最小上界⨆{dn∣n∈ω}\bigsqcup\{d_n|n\in\omega\}，则称(D,⊑D)(D,\sqsubseteq_D) 是完全偏序，简记为 cpo。

    如果它有一个最小元⊥D\perp_D（称为底），则称(D,⊑D)(D,\sqsubseteq_D) 是含底的 cpo。

  • 记号，把完全偏序(D,⊑D)(D,\sqsubseteq_D) 的次序简记为⊑\sqsubseteq，当它含底时记底元素为⊥\perp。

  • 考察用规则实例集合RR 定义的算子，若B0⊆B1⊆...⊆Bn⊆...B_0\subseteq B_1\subseteq ...\subseteq B_n\subseteq ...，则有：

    R^(B0)⊆R^(B1)⊆...⊆R^(Bn)⊆...\hat{R}(B_0)\subseteq \hat{R}(B_1)\subseteq...\subseteq\hat{R}(B_n)\subseteq...

    又因为∀n,Bn⊆⋃n∈ωBn⇒∀n,R^(Bn)∈R^(⋃n∈ωBn)\forall n,B_n\subseteq\bigcup_{n\in\omega} B_n\Rightarrow \forall n,\hat{R}(B_n)\in\hat{R}(\bigcup_{n\in\omega}B_n)，所以有：

    ⋃n∈ωR^(Bn)⊆R^(⋃n∈ωBn)\bigcup_{n\in\omega}\hat{R}(B_n)\subseteq \hat{R}(\bigcup_{n\in\omega} B_n)

    另一方面，对于任意y∈R^(⋃n∈ωBn)y\in\hat{R}(\bigcup_{n\in\omega}B_n)，根据算子R^\hat{R} 定义，一定存在X⊆⋃n∈ωBnX\subseteq\bigcup_{n\in\omega}B_n，使得X/y∈RX/y\in R。又因为 X 是有限的，所以

    ∃n,X⊆Bn∴y∈R^(Bn)∴y∈⋃n∈ωR^(Bn)\exists n,X\subseteq B_n\\ \therefore y\in\hat{R}(B_n)\\ \therefore y\in\bigcup_{n\in\omega}\hat{R}(B_n)

    所以R^(⋃n∈ωBn)⊆⋃n∈ωR^(Bn)\hat{R}(\bigcup_{n\in\omega} B_n)\subseteq\bigcup_{n\in\omega}\hat{R}(B_n)。综上，有:

    R^(⋃n∈ωBn)=⋃n∈ωR^(Bn)\hat{R}(\bigcup_{n\in\omega} B_n)=\bigcup_{n\in\omega}\hat{R}(B_n)

    这证明了R^\hat{R} 是连续的，前提是规则是有限的.

  • 定义：设函数f:D→Ef:D\rightarrow E 是单调的当且仅当:

    ∀d,d′∈D,d⊑Dd′⇒f(d)⊑Ef(d′)\forall d,d'\in D,d\sqsubseteq_D d'\Rightarrow f(d)\sqsubseteq_Ef(d')

    f 是连续的当且仅当它是单调的，且对 D 中所有链d0⊑d1⊑...⊑dn⊑...d_0\sqsubseteq d_1\sqsubseteq ...\sqsubseteq d_n\sqsubseteq... 都有:

    ⨆n∈ωf(dn)=f(⨆n∈ωdn)\bigsqcup_{n\in\omega}f(d_n)=f(\bigsqcup_{n\in\omega}d_n)

  • 设函数f:D→Df:D\rightarrow D 是完全偏序 D 上的连续函数.f 的不动点是 D 中满足f(d)=df(d)=d 的元素 d. f 的前缀不动点是 D 中使得f(d)⊑df(d)\sqsubseteq d 的元素 d.

    不动点定理：设函数f:D→Df:D\rightarrow D 是含底的完全偏序 D 上的连续函数。定义:

    fix(f)=⨆n∈ωfn(⊥)fix(f)=\bigsqcup_{n\in\omega}f^n(\perp)

    则fix(f)fix(f) 是 f 的一个不动点和最小的前缀不动点.

    证明：由连续性，

    f(fix(f))=f(⨆n∈ωfn(⊥))=⨆n∈ωfn+1(⊥)=⨆n∈ωfn+1(⊥)⊔{⊥}=⨆n∈ωfn(⊥)=fix(f)f(fix(f))=f(\bigsqcup_{n\in\omega}f^n(\perp))\\ =\bigsqcup_{n\in\omega} f^{n+1}(\perp)\\ =\bigsqcup_{n\in\omega} f^{n+1}(\perp)\sqcup\{\perp\}\\ =\bigsqcup_{n\in\omega} f^n(\perp)=fix(f)

    所以是不动点。借助单调性，而对于任意一个前缀不动点 d,

    ⊥⊑d⇒f(⊥)⊑f(d)⊑d\perp\sqsubseteq d\Rightarrow f(\perp)\sqsubseteq f(d)\sqsubseteq d

    然后再归纳一手，就有fn(⊥)⊑df^n(\perp)\sqsubseteq d. 故fix(f)⊑dfix(f)\sqsubseteq d, 即为最小的前缀不动点.

  • 关于完全偏序与连续函数的意义，我看了书挺久也理解不了。说后章会仔细讨论的吧。

# Knaster-Tarski 定理

  • 对一组规则实例 R，有

    IR=⋂{Q∣Q对R封闭}I_R=\bigcap\{Q|Q对R封闭\}

    命题等价为：

    fix(R^)=⋂{Q∣R^(Q)⊆Q}fix(\hat{R})=\bigcap\{Q|\hat{R}(Q)\subseteq Q\}

    即算子R^\hat{R} 的最小不动点可以用其前缀不动点的交集来刻画。这其实是克纳斯塔 - 塔尔斯基定理的特殊情况。

  • 定义，对偏序(P,⊑)(P,\sqsubseteq) 和子集X⊆PX\subseteq P，称 p 是 X 的下界，当且仅当

    ∀q∈X,p⊑q\forall q\in X,p\sqsubseteq q

    同样可以类似定义 X 的最大下界（glb）。

    如果一个偏序的子集 X 有最大下界，我们把它记为⊓X\sqcap X。最小上界又称为上确界（sups），最大下界又称为下确界（infs）。

  • 定义，如果一个偏序的任意子集都有最大下界，则称这个偏序为完全格。事实上，完全格的任意子集也必有最小上界。而且若(L,⊑)(L,\sqsubseteq) 是完全格，对应的逆关系(L,⊒)(L,\sqsupseteq) 也是完全格。

  • 克纳斯塔 - 塔尔斯基最小不动点定理，令(L,⊑)(L,\sqsubseteq) 是完全格，f:L→Lf:L\rightarrow L 是单调函数，定义

    m=⊓{x∈L∣f(x)⊑x}m=\sqcap\{x\in L|f(x)\sqsubseteq x\}

    则 m 是 f 的不动点和 f 的最小前缀不动点。同理，定义

    M=⨆{x∈L∣x⊑f(x)}M=\bigsqcup\{x\in L|x\sqsubseteq f(x)\}

    则 M 是 f 的不动点和 f 的最大后缀不动点。

    证明，以最小前缀不动点为例：

    首先，m 是前缀不动点集合的下界，所以其为最小前缀不动点。

    其次，因为f(m)⊑mf(m)\sqsubseteq m，由单调性，有f(f(m))⊑f(m)f(f(m))\sqsubseteq f(m)，所以f(m)f(m) 也是集合{x∈L∣f(x)⊑x}\{x\in L|f(x)\sqsubseteq x\} 的元素。

    又因为 m 是该集合的下界，所以也有m⊑f(m)m\sqsubseteq f(m)，所以有m=f(m)m=f(m)。即为不动点。

    注：以上定理限于前缀不动点集合存在下界的情况。

# IMP 的公理语义

  • 我们基于如下形式的断言建立证明系统：

    {A}c{B}\{A\}c\{B\}

    其中 A 和 B 是像布尔表达式 Bexp 中那样的断言，c 是一条命令。它的含义为：

    对于所有满足断言 A 的状态σ\sigma，如果从状态σ\sigma 下执行 c 后程序终止于状态σ′\sigma'，那么σ′\sigma' 满足断言 B。

    其中断言 A 称为前置条件，断言 B 称为后置条件。形如{A}c{B}\{A\}c\{B\} 的断言称为部分正确性断言，因为该断言不涉及命令 c 执行不重质的情况。譬如：

    c=while  true  do  skip{true}c{false}c=while\;true\;do\;skip\\ \{true\}c\{false\}

    上面这个断言是有效的。因为 c 不会终止。此时从任何满足 A 的状态开始执行 c 都是有效的，称为完全正确性断言，记为[A]c[B][A]c[B]。

  • 记号，σ⊨A\sigma\models A 表示断言 A 在状态σ\sigma 下为真。部分正确性断言意味着：

    {A}c{B}:∀σ,(σ⊨A&C[c]σ)有定义⇒C[c]σ⊨B\{A\}c\{B\}:\forall \sigma,(\sigma\models A\&\mathscr{C}[c]\sigma)有定义\Rightarrow\mathscr{C}[c]\sigma\models B

    什么叫C[c]σ\mathscr{C}[c]\sigma 有定义呢？事实上，用前一部分的定义，C[c]σ\mathscr{C}[c]\sigma 无定义⇔C[c]σ=⊥\Leftrightarrow\mathscr{C}[c]\sigma=\perp。特别地，规定C[c]⊥=⊥\mathscr{C}[c]\perp=\perp。而且⊥\perp 满足所有的断言。在规定后，可以重写为：

    {A}c{B}:∀σ⊨A⇒C[c]σ⊨B\{A\}c\{B\}:\forall\sigma\models A\Rightarrow\mathscr{C}[c]\sigma\models B

# 断言语言 Assn

  • 首先，扩充AexpAexp，使之包括整型变量i,j,k,...i,j,k,...，即对算术表达式的 BNF 描述扩充为：

    a::=n∣X∣i∣a0+a1∣a0−a1∣a0×a1a::=n|X|i|a_0+a_1|a_0-a_1|a_0\times a_1

    其中n∈N,X∈Loc,i∈Intvarn\in N,X\in Loc,i\in Intvar，IntvarIntvar 为整型变量集。

    然后，扩充BexpBexp：

    b::=true∣false∣a0=a1∣a0≤a1∣b0∨b1∣b0∧b1∣¬b0∣b0⇒b1∣∀i,b∣∃i,bb::=true|false|a_0=a_1|a_0\leq a_1|b_0\vee b_1|b_0\wedge b_1|\neg b_0|b_0\Rightarrow b_1|\forall i,b|\exists i,b

    我们称，扩充的布尔断言集合为断言语言 Assn。

# 自由变量与约束变量

  • 自由变量和约束变量类似，即是否被前束谓词限制。

  • 记FV(a)FV(a) 为算术表达式a∈Aexpva\in Aexpv（扩充集合）中的自由变量集合，有：

    FV(n)=FV(X)=∅FV(i)={i}Fv(a0+a1)=FV(a0−a1)=FV(a0×a1)=FV(a0)∪FV(a1)FV(n)=FV(X)=\emptyset\\ FV(i)=\{i\}\\ Fv(a_0+a_1)=FV(a_0-a_1)=FV(a_0\times a_1)=FV(a_0)\cup FV(a_1)

    对断言（布尔表达式）的定义为：

    FV(true)=FV(false)=∅FV(a0=a1)=FV(a0≤a1)=FV(a0)∪FV(a1)FV(b0∨b1)=FV(b0∧b1)=FV(b0)∪FV(b1)FV(¬b0)=FV(b0)FV(∀i,b0)=FV(∃i,b0)=FV(b0)/{i}FV(true)=FV(false)=\emptyset\\ FV(a_0=a_1)=FV(a_0\leq a_1)=FV(a_0)\cup FV(a_1)\\ FV(b_0\vee b_1)=FV(b_0\wedge b_1)=FV(b_0)\cup FV(b_1)\\ FV(\neg b_0)=FV(b_0)\\ FV(\forall i,b_0)=FV(\exists i,b_0)=FV(b_0)/\{i\}

    我们称不含自由变量的断言是封闭的。

# 代入

  • 断言 A 中的整型变量被算术表达式替换的过程称为代入。记为A[a/i]A[a/i]。首先用以下结构归纳法定义算术表达式中的代入：

    n[a/i]≡nX[a/i]≡Xj[a/i]≡ji[a/i]≡a(a0+a1)[a/i]≡(a0[a/i]+a1[a/i])(a0−a1)[a/i]≡(a0[a/i]−a1[a/i])(a0×a1)[a/i]≡(a0[a/i]×a1[a/i])n[a/i]\equiv n\quad X[a/i]\equiv X\\ j[a/i]\equiv j\quad i[a/i]\equiv a\\ (a_0+a_1)[a/i]\equiv (a_0[a/i]+a_1[a/i])\\ (a_0-a_1)[a/i]\equiv (a_0[a/i]-a_1[a/i])\\ (a_0\times a_1)[a/i]\equiv (a_0[a/i]\times a_1[a/i])\\

    在定义算术表达式的代入后，才方便定义布尔表达式的代入：

    true[a/i]=truefalse[a/i]=false(a0=a1)[a/i]=(a0[a/i]=a1[a/i])(a0≤a1)[a/i]=(a0[a/i]≤a1[a/i])(A0∨A1)[a/i]=(A0[a/i]∨A1[a/i])(A0∧A1)[a/i]=(A0[a/i]∧A1[a/i])(¬A)[a/i]=¬(A[a/i])(A0⇒A1)[a/i]=(A0[a/i]⇒A1[a/i])(∀j,A)[a/i]=∀j,A[a/i](∀i,A)[a/i]=∀i,A(∃j,A)[a/i]=∃j,(A[a/i])(∃i,A)[a/i]=∃i,Atrue[a/i]=true\quad false[a/i]=false\\ (a_0=a_1)[a/i]=(a_0[a/i]=a_1[a/i])\\ (a_0\leq a_1)[a/i]=(a_0[a/i]\leq a_1[a/i])\\ (A_0\vee A_1)[a/i]=(A_0[a/i]\vee A_1[a/i])\\ (A_0\wedge A_1)[a/i]=(A_0[a/i]\wedge A_1[a/i])\\ (\neg A)[a/i]=\neg(A[a/i])\\ (A_0\Rightarrow A_1)[a/i]=(A_0[a/i]\Rightarrow A_1[a/i])\\ (\forall j,A)[a/i]=\forall j,A[a/i]\\ (\forall i,A)[a/i]=\forall i,A\\ (\exists j,A)[a/i]=\exists j,(A[a/i])\\ (\exists i,A)[a/i]=\exists i,A

    如果aa 含有自由变量的话，根据离散中学到的，代入会有些麻烦，因为可能要对自由变量换名。例如：

    A=(i≥1)∧(∀i,i=1)A=(i\geq 1)\wedge(\forall i,i=1)

    如果要代入的话就要考虑 A 的换名A=(j≥1)∧(∀i,i=1)A=(j\geq 1)\wedge(\forall i,i=1)

# 断言的语义

由于算术表达式扩充后包含了整型变量，所以我们不能用前面的语义函数A\mathscr{A} 来精确描述新表达式的值。为此我们引入解释的概念。所谓解释是指一个函数，它将一个整数值赋给整型变量I:Intvar→NI:Intvar\rightarrow N

  • 定义语义函数Av\mathscr{A}v，在特定的状态和特定的解释下，它将值和整型变量的算术表达式相关联。在解释II 和状态σ\sigma 下，算术表达式a∈Aexpva\in Aexpv 的值记为Av[a]Iσ\mathscr{A}v[a]I\sigma（同样是空心中括号表示引用，打不出来）。用结构归纳法定义如下：

    Av[n]Iσ=nAv[X]Iσ=σ(X)Av[i]Iσ=I(i)Av[a0+a1]Iσ=Av[a0]Iσ+Av[a1]IσAv[a0−a1]Iσ=Av[a0]Iσ−Av[a1]IσAv[a0×a1]Iσ=Av[a0]Iσ×Av[a1]Iσ\mathscr{A}v[n]I\sigma=n\\ \mathscr{A}v[X]I\sigma=\sigma(X)\\ \mathscr{A}v[i]I\sigma=I(i)\\ \mathscr{A}v[a_0+a_1]I\sigma=\mathscr{A}v[a_0]I\sigma+\mathscr{A}v[a_1]I\sigma\\ \mathscr{A}v[a_0-a_1]I\sigma=\mathscr{A}v[a_0]I\sigma-\mathscr{A}v[a_1]I\sigma\\ \mathscr{A}v[a_0\times a_1]I\sigma=\mathscr{A}v[a_0]I\sigma\times \mathscr{A}v[a_1]I\sigma\\

  • 命题，对所有无整型变量的a∈Aexpva\in Aexpv，对所有的状态σ\sigma 和所有解释II 都有

    A[a]σ=Av[a]Iσ\mathscr{A}[a]\sigma=\mathscr{A}v[a]I\sigma

    这个结构归纳一下就好。

  • 记号，我们用记号I[n/i]I[n/i] 表示从解释II 中将整型变量 i 的值改变成 n 而得到的解释，即

    I[n/i](j)={nj=iI(j)elseI[n/i](j)=\begin{cases}n&j=i\\I(j)&else\end{cases}

  • 定义，σ⊨IA\sigma\models^I A 表示在解释 I，状态σ\sigma 下，断言 A 为真。而总有⊥⊨IA\perp\models^I A。归纳定义如下：

    σ⊨Itrueσ⊨I(a0=a1)ifAv[a0]Iσ=Av[a1]Iσσ⊨I(a0≤a1)ifAv[a0]Iσ≤Av[a1]Iσσ⊨IA∧Bifσ⊨IA  and  σ⊨IBσ⊨IA∨Bifσ⊨IA  or  σ⊨IBσ⊨I¬Aifnot  σ⊨IAσ⊨IA⇒Bif(not  σ⊨IA)  or  σ⊨IBσ⊨I∀i,Aif∀n∈n,σ⊨I[n/i]Aσ⊨I∃i,Aif∃n∈n,σ⊨I[n/i]A⊥⊨IA\sigma\models^I true\\ \sigma\models^I(a_0=a_1)\quad if\quad \mathscr{A}v[a_0]I\sigma=\mathscr{A}v[a_1]I\sigma\\ \sigma\models^I(a_0\leq a_1)\quad if\quad \mathscr{A}v[a_0]I\sigma\leq\mathscr{A}v[a_1]I\sigma\\ \sigma\models^IA\wedge B\quad if\quad \sigma\models^I A\;and\;\sigma\models^I B\\ \sigma\models^IA\vee B\quad if\quad \sigma\models^I A\;or\;\sigma\models^I B\\ \sigma\models^I\neg A\quad if\quad not\;\sigma\models^I A\\ \sigma\models^I A\Rightarrow B\quad if\quad(not\;\sigma\models^I A)\;or\;\sigma\models^I B\\ \sigma\models^I\forall i,A\quad if\quad \forall n\in n,\sigma\models^{I[n/i]}A\\ \sigma\models^I\exists i,A\quad if\quad \exists n\in n,\sigma\models^{I[n/i]}A\\ \perp\models^I A

    对b∈Bexpb\in Bexp，σ∈Σ\sigma\in\Sigma 和任一解释 I，有B[b]σ=true\mathscr{B}[b]\sigma=true 当且仅当σ⊨Ib\sigma\models^I b。

  • 对应于解释II，断言 A 的扩充定义为

    AI={σ∈Σ⊥∣σ⊨IA}A^I=\{\sigma\in\Sigma_\perp|\sigma\models^I A\}

    就是在解释 I 下，断言 A 成立的状态的集合。

  • 部分正确性断言形如

    {A}c{B}\{A\}c\{B\}

    其中，A,B∈Assn,c∈ComA,B\in Assn,c\in Com。注意部分正确性断言并不属于 Assn。

  • 对于解释II，我们定义状态和部分正确性断言之间满足关系：

    σ⊨I{A}c{B}iff(σ⊨IA⇒C[c]σ⊨IB)\sigma\models^I\{A\}c\{B\}\quad iff\quad (\sigma\models^I A\Rightarrow \mathscr{C}[c]\sigma\models^I B)

    换言之，状态σ\sigma 满足对应于解释II 的部分正确性断言，当且仅当从状态σ\sigma 下cc 的任何成功的计算都终止于满足 B 的状态。

  • 设II 是一个解释，考察{A}c{B}\{A\}c\{B\}。我们比较关心它在所有状态下是否为真。即：

    ∀σ∈Σ⊥,σ⊨I{A}c{B}\forall\sigma\in\Sigma_\perp,\sigma\models^I\{A\}c\{B\}

    也可以记作⊨I{A}c{B}\models^I\{A\}c\{B\}。例如考虑例子：

    {X<i}X:=X+1{X<i}\{X<i\}X:=X+1\{X<i\}

    我们不太关心II 对于 i 的特定赋值（或许关注终止状态）。引入有效性的概念：

    ⊨{A}c{B}\models\{A\}c\{B\}

    表示对所有的解释II 和所有的状态σ\sigma ，有

    σ⊨I{A}c{B}\sigma\models^I\{A\}c\{B\}

    若有这个式子，则称部分正确性断言{A}c{B}\{A\}c\{B\} 是有效的。类似也有⊨A\models A。

  • 例，若有⊨(A⇒B)\models(A\Rightarrow B)，则有

    ∀σ∈Σ⊥,((σ⊨IA)⇒(σ⊨IB))\forall\sigma\in\Sigma_\perp,((\sigma\models^I A)\Rightarrow(\sigma\models^I B))

    即AI⊆BIA^I\subseteq B^I。（在解释 I 下，A 成立的状态集合为 B 成立的状态集合的子集）

    例，若有⊨{A}c{B}\models\{A\}c\{B\}，则对于任意的解释II，有

    ∀σ∈Σ⊥,((σ⊨IA)⇒(C[c]σ⊨IB))\forall\sigma\in\Sigma_\perp,((\sigma\models^I A)\Rightarrow(\mathscr{C}[c]\sigma\models^I B))

    即C[c]AI⊆BI\mathscr{C}[c]A^I\subseteq B^I，意思是，在解释 I 下 A 成立的状态集合，在映射C[c]\mathscr{C}[c] 下的象集是BIB^I 的子集。

# 部分正确性的证明规则 —— 霍尔规则

介绍产生有效的部分正确性断言的证明规则，这组证明规则被称为霍尔规则，这组规则组成的证明系统称为霍尔逻辑。

  • skip 规则：

{A}skip{A}\{A\}skip\{A\}

  • 赋值规则：

{B[a/X]}X:=a{B}\{B[a/X]\}X:=a\{B\} 

这个其实有点绕，可以举个例子想想....譬如$B:\sigma(X)=3$，然后赋值语句有$X=3，a\equiv 3$，然后$B[a/X]:a=3$，然后满足$B[a/X]$的为全体状态集合。所以任意一个状态在进行$X:=3$赋值后，都会满足$B:\sigma[3/X](X)=3$。
  • 顺序复合规则：

{A}c0{C}{C}c1{B}{A}c0;c1{B}\frac{\{A\}c_0\{C\}\quad\{C\}c_1\{B\}}{\{A\}c_0;c_1\{B\}}

  • 条件规则：

{A∧b}c0{B}{A∧¬b}c1{B}{A}if  b  do  c0  else  c1{B}\frac{\{A\wedge b\}c_0\{B\}\quad\{A\wedge \neg b\}c_1\{B\}}{\{A\}if\;b\;do\;c_0\;else\;c_1\{B\}}

  • while 循环规则：

{A∧b}c{A}{A}while  b  do  c{A∧¬b}\frac{\{A\wedge b\}c\{A\}}{\{A\}while\;b\;do\;c\{A\wedge \neg b\}} 

这里其实我也想进行一点说明。首先这里b应该考虑其为一个布尔表达式，而这个规则应该无论b取$true/false$都是合理的。

例如在某个解释某个状态下$A$成立，$b=true$，于是有进入while循环执行c，执行后状态仍满足A，继续执行，直到最后b不为$true$，

此时终止状态显然是满足$A\wedge\neg b$的。

若在某个解释某个状态下$A$成立，$b=false$，则$\{A\}while\;b\;do\;c\{A\wedge \neg b\}$退化成$\{A\}skip\{A\}$，不需要前提就是有效的。
  • 推论规则：

    ⊨(A⇒A′){A′}c{B′}⊨(B′⇒B){A}c{B}\frac{\models(A\Rightarrow A')\quad\{A'\}c\{B'\}\quad\models(B'\Rightarrow B)}{\{A\}c\{B\}}

  • ++ 霍尔规则就是一个证明系统。++ 其中的推导称为证明，而推导的结论称为定理。如果{A}c{B}\{A\}c\{B\} 是一条定理，则记为\vdash\{A\}c\

    这里我理解的定理即为通过全是有效的前提推出来的结论。

# 霍尔规则的完备性和可靠性

  • 可靠性：如果假设某一条规则的前提是有效的，那么它的结论也是有效的，即规则的有效性得到保持。如果证明系统中每条规则都是可靠的，则称这个证明系统本身就是可靠的。

    完备性：证明系统足够强大，使得所有有效的部分正确性断言都能作为定理。

  • 引理：对a,a0∈Aexpv,X∈Loca,a_0\in Aexpv,X\in Loc，则对所有的解释II 和状态σ\sigma，有：

    Av[a0[a/X]]Iσ=Av[a0]Iσ[Av[a]Iσ/X]\mathscr{A}v[a_0[a/X]]I\sigma=\mathscr{A}v[a_0]I\sigma[\mathscr{A}v[a]I\sigma/X]

    也就是说取值时，算术表达式的代入可以等价为状态的变化。

  • 引理：设II 是一个解释，B∈Assn,X∈Loc,a∈AexpB\in Assn,X\in Loc,a\in Aexp，则对所有的状态σ∈Σ\sigma\in\Sigma，有：

    σ⊨IB[a/X]iffσ[A[a]σ/X]⊨IB\sigma\models^I B[a/X]\quad iff\quad \sigma[\mathscr{A}[a]\sigma/X]\models^I B

    这实际上是推导的结论和前提的状态等价性。

  • 定理：设{A}c{B}\{A\}c\{B\} 是部分正确性断言，如果⊢{A}c{B}\vdash \{A\}c\{B\}，则有⊨{A}c{B}\models\{A\}c\{B\}。

    换言之，即为：证明系统中每一条定理都是有效的。施结构归纳法来证明每条规则保持有效性：

    • skip：显然⊨{A}skip{A}\models\{A\}skip\{A\} 成立，因此该规则可靠。

    • 赋值：设c≡(X:=a)c\equiv (X:=a)，设II 是任意一个解释， 根据引理有

      ∀σ∈Σ,σ⊨IB[a/X]⇔σ[A[a]σ/X]⊨IB\forall\sigma\in\Sigma,\sigma\models^IB[a/X]\Leftrightarrow\sigma[\mathscr{A}[a]\sigma/X]\models^I B

      根据指称语义的定义，有C[X:=a]σ=σ[A[a]σ/X]\mathscr{C}[X:=a]\sigma=\sigma[\mathscr{A}[a]\sigma/X]。于是有

      ∀σ∈Σ,σ⊨IB[a/X]⇒C[X:=a]σ⊨IB\forall\sigma\in\Sigma,\sigma\models^I B[a/X]\Rightarrow\mathscr{C}[X:=a]\sigma\models^I B

      即⊨{B[a/X]}X:=a{B}\models \{B[a/X]\}X:=a\{B\}。

    • 顺序复合规则：引入规则前提是有效的 这个条件：

      ⊨{A}c0{C},⊨{C}c1{B}\models\{A\}c_0\{C\},\models\{C\}c_1\{B\}

      对任意一个解释II 状态σ\sigma，若有σ⊨IA\sigma\models^I A，于是有C[c0]σ⊨IC\mathscr{C}[c_0]\sigma\models^I C，于是有C[c1]C[c0]σ⊨IB\mathscr{C}[c_1]\mathscr{C}[c_0]\sigma\models^I B。根据指称语义的定义，顺序命令就是函数的嵌套，即C[c1](C[c0](σ))=C[c0;c1](σ)\mathscr{C}[c_1](\mathscr{C}[c_0](\sigma))=\mathscr{C}[c_0;c_1](\sigma)，于是得到C[c0;c1]σ⊨IB\mathscr{C}[c_0;c_1]\sigma\models^I B。

      于是有\models \{A\}c_0;c_1\

    • 条件规则：引入规则前提有效：

      ⊨{A∧b}c0{B},⊨{A∧¬b}c1{B}\models\{A\wedge b\}c_0\{B\},\models\{A\wedge \neg b\}c_1\{B\}

      对于任意一个解释II 状态σ\sigma，若有σ⊨IA\sigma\models^I A，则或σ⊨Ib\sigma\models^I b 或σ⊨I¬b\sigma\models^I\neg b。对于前一种情况，有σ⊨IA∧b\sigma\models^I A\wedge b。

      又因为⊨{A∧b}c0{B}\models\{A\wedge b\}c_0\{B\}，所以C[c0]σ⊨IB\mathscr{C}[c_0]\sigma\models^I B；对于后一种情况，同理有C[c1]σ⊨IB\mathscr{C}[c_1]\sigma\models^I B。

      因此有C[if  b  c0  else  c1]σ⊨IB\mathscr{C}[if\;b\;c_0\;else\;c_1]\sigma\models^I B，于是条件规则也保持了有效性：

      ⊨{A∧b}c0{B},⊨{A∧¬b}c1{B}⇒⊨{A}if  b  then  c0  else  c1{B}\models\{A\wedge b\}c_0\{B\},\models\{A\wedge \neg b\}c_1\{B\}\Rightarrow\models\{A\}if\;b\;then\;c_0\;else\;c_1\{B\}

    • while 循环：引入规则前提有效：

      ⊨{A∧b}c{A}\models\{A\wedge b\}c\{A\}

      记w≡while  b  do  cw\equiv while\;b\;do\;c，回忆之前的指称语义，有

      C[w]=⋃n∈ωθn\mathscr{C}[w]=\bigcup_{n\in\omega}\theta_n

      其中

      θ0=∅θn+1={(σ,σ′)∣B[b]σ=true&(σ,σ′)∈θn∘C[c]}∪{(σ,σ)∣B[b]σ=false}\theta_0=\emptyset\\ \theta_{n+1}=\{(\sigma,\sigma')|\mathscr{B}[b]\sigma=true\&(\sigma,\sigma')\in\theta_n\circ\mathscr{C}[c]\}\cup\{(\sigma,\sigma)|\mathscr{B}[b]\sigma=false\}

      定义性质 P：

      P(n)⇔∀σ,σ′∈Σ,(σ,σ′)∈θn&σ⊨IA⇒σ′⊨IA∧¬bP(n)\Leftrightarrow \forall\sigma,\sigma'\in\Sigma,(\sigma,\sigma')\in\theta_n\&\sigma\models^I A\Rightarrow\sigma'\models^I A\wedge\neg b

      我们证明 P 若对所有 n 成立，则有

      ∀σ,σ′∈Σ,(σ,σ′)∈⋃n∈ωθn=C[w],σ⊨IA⇒σ′⊨IA∧¬b\forall\sigma,\sigma'\in\Sigma,(\sigma,\sigma')\in\bigcup_{n\in\omega}\theta_n=\mathscr{C}[w],\sigma\models^I A\Rightarrow\sigma'\models^I A\wedge\neg b

      即∀σ∈Σ,σ⊨IA⇒C[w]σ⊨IA∧¬b\forall\sigma\in \Sigma,\sigma\models^I A\Rightarrow\mathscr{C}[w]\sigma\models^I A\wedge\neg b，即有⊨{A}w{A∧¬b}\models \{A\}w\{A\wedge\neg b\}。

      • 奠基：P(0)P(0) 成立。

      • 若P(n)P(n) 成立，考虑

        若B[b]σ=false&σ′=σ\mathscr{B}[b]\sigma=false\& \sigma'=\sigma，于是B[b]σ′=false\mathscr{B}[b]\sigma'=false，于是σ⊨IA⇒σ′⊨IA∧¬b\sigma\models^I A\Rightarrow\sigma'\models^I A\wedge\neg b。

        若B[b]σ=true&(σ,σ′)∈θn∘C[c]\mathscr{B}[b]\sigma=true\&(\sigma,\sigma')\in\theta_n\circ\mathscr{C}[c]，于是∃σ′′,(σ,σ′′)∈C[c]\exists\sigma'',(\sigma,\sigma'')\in\mathscr{C}[c]。

        ∵C[b]σ=true∴σ⊨IA⇒σ⊨IA∧b∵⊨{A∧b}c{A}∴σ⊨IA⇒σ′′⊨IA∵(σ′′,σ′)∈θn,P(n)∴σ⊨IA⇒σ′⊨IA∧¬b\because \mathscr{C}[b]\sigma=true\\ \therefore\sigma\models^I A\Rightarrow\sigma\models^I A\wedge b\\ \because\models\{A\wedge b\}c\{A\}\\ \therefore \sigma\models^I A\Rightarrow\sigma''\models^I A\\ \because (\sigma'',\sigma')\in\theta_n,P(n)\\ \therefore \sigma\models^I A\Rightarrow\sigma'\models^I A\wedge\neg b

        因此得到证明成立。

        这里我发现，其实定义θn\theta_n 时一定是θn+1=θn∘C[c]\theta_{n+1}=\theta_n\circ\mathscr{C}[c] 的，而不能反过来θn+1=C[c]∘θn\theta_{n+1}=\mathscr{C}[c]\circ\theta_n，否则证明将及其困难。看似嵌套顺序无关，但这事实上是有影响的，θn\theta_n 的含义实际上是进行nn 次循环后停止的意思。所以先执行cc 即使不进入循环也可以推出结果（循环的规则讨论了不进入循环的情况），但如果先执行nn 次循环，那结束循环时就没理由再执行一次cc 了，因为此时 b 已经为 false 了。

    • 推论规则：引入规则条件都是有效的：

      ⊨(A⇒A′),⊨{A′}c{B′},⊨(B′⇒B)\models(A\Rightarrow A'),\models\{A'\}c\{B'\},\models(B'\Rightarrow B)

      于是有

      σ⊨IA⇒σ⊨IA′⇒C[c]σ⊨IB′⇒C[c]σ⊨IB∴∀σ,I,σ⊨IA⇒C[c]σ⊨IB\sigma\models^IA\Rightarrow \sigma\models^I A'\Rightarrow\mathscr{C}[c]\sigma\models^I B'\Rightarrow\mathscr{C}[c]\sigma\models^I B\\ \therefore \forall\sigma,I,\sigma\models^I A\Rightarrow\mathscr{C}[c]\sigma\models^I B

      也就是⊨{A}c{B}\models\{A\}c\{B\}。

# 应用霍尔规则的一个示例：

如何用霍尔规则验证w≡(while  X>0  do  Y:=X×Y;X:=X−1)w\equiv(while\;X>0\;do\;Y:=X\times Y;X:=X-1) 确实是在计算阶乘，其中约定XX 初始值为 n，YY 为 1.

换为数学语言，我们要证明：

{X=n∧n≥0∧Y=1}w{Y=n!}\{X=n\wedge n\geq 0\wedge Y=1\}w\{Y=n!\}

考虑一个不变式

I≡(Y×X!=n!∧X≥0)I\equiv(Y\times X!=n!\wedge X\geq 0)

先证明它确实是一个不变式，即{I∧X>0}w{I}\{I\wedge X>0\}w\{I\}（当然，{I∧X≤0}w{I}\{I\wedge X\leq 0\}w\{I\} 是显然的，结合起来就有{I}w{I}\{I\}w\{I\}）

其实我们只需要证明对每一次循环都有

{I∧X>0}Y:=X×Y;X:=X−1{I}\{I\wedge X>0\}Y:=X\times Y;X:=X-1\{I\}

根据赋值规则，有{I[(X−1)/X]}X:=X−1{I}\{I[(X-1)/X]\}X:=X-1\{I\}。

其中，I[(X−1)/X]=Y×(X−1)!=n!∧(X−1)≥0I[(X-1)/X]=Y\times(X-1)!=n!\wedge(X-1)\geq 0。再根据赋值规则，有：

{X×Y×(X−1)!=n!∧(X−1)≥0}Y:=X×Y{I[(X−1)/X]}\{X\times Y\times(X-1)!=n!\wedge(X-1)\geq 0\}Y:=X\times Y\{I[(X-1)/X]\}

这样，由顺序规则，有：

{X×Y×(X−1)!=n!∧(X−1)≥0}Y:=X×Y;X:=X−1{I}\{X\times Y\times(X-1)!=n!\wedge(X-1)\geq 0\}Y:=X\times Y;X:=X-1\{I\}

而

I∧X>0⇒X×Y×(X−1)!=n!∧X>0⇒Y×X!=n!∧(X−1)≥0I\wedge X>0\Rightarrow X\times Y\times(X-1)!=n!\wedge X>0\\ \Rightarrow Y\times X!=n!\wedge (X-1)\geq 0

于是根据推论规则，有：

⊨(I∧X>0⇒Y×X!=n!∧(X−1)≥0){Y×X!=n!∧(X−1)≥0}Y:=X×Y;X:=X−1{I}⊨I⇒I{I∧X>0}Y:=X×Y;X=X−1{I}\frac{\models(I\wedge X>0 \Rightarrow Y\times X!=n!\wedge(X-1)\geq 0)\quad\{Y\times X!=n!\wedge(X-1)\geq 0\}Y:=X\times Y;X:=X-1\{I\}\quad\models I\Rightarrow I}{\{I\wedge X>0\}Y:=X\times Y;X=X-1\{I\}}

于是根据 while 循环规则，有：

{I∧X>0}Y:=X×Y;X=X−1{I}{I}w{I∧¬X>0}\frac{\{I\wedge X>0\}Y:=X\times Y;X=X-1\{I\}}{\{I\}w\{I\wedge\neg X>0\}}

显然有

⊨((X=n)∧(n≥0)∧(Y=1)⇒I)\models((X=n)\wedge(n\geq 0)\wedge(Y=1)\Rightarrow I)

且

I∧¬X>0⇒Y×X!=n!∧X≥0∧¬X>0⇒Y×X!=n!∧X=0⇒Y×0!=n!⇒Y=n!I\wedge \neg X>0\Rightarrow Y\times X!=n!\wedge X\geq0\wedge\neg X>0\\ \Rightarrow Y\times X!=n!\wedge X=0\\ \Rightarrow Y\times 0!=n!\Rightarrow Y=n!

于是根据推论规则，有

⊨((X=n)∧(n≥0)∧(Y=1)⇒I){I}w{I∧¬X>0}⊨(I∧¬X>0⇒Y=n!){(X=n)∧(n≥0)∧(Y=1)}w{Y=n!}\frac{\models((X=n)\wedge(n\geq 0)\wedge(Y=1)\Rightarrow I)\quad \{I\}w\{I\wedge\neg X>0\}\quad \models(I\wedge\neg X>0\Rightarrow Y=n!)}{\{(X=n)\wedge(n\geq 0)\wedge(Y=1)\}w\{Y=n!\}}

利用霍尔规则证明时，有几个注意点。分析顺序命令时一般从右到左分析，其次要选择尽量强的循环不变式。循环不变式 + 循环条件为 false 一定要可以推出循环结束后的状态。在本例种，II+¬X>0\neg X>0 就可以推出跳出循环时，X=0X=0。

程序正确性证明的研究促进了程序开发方法的拓展。事实上，程序及其正确性的证明应该同时地进行，而程序正确性的证明思想引导了程序设计的方法！

# 霍尔规则的完备性

# 哥德尔不完备性定理

（哥德尔不完备性定理（1931））不存在 Assn 的一个能行的证明系统，使得 Assn 的有效断言恰好是该系统的定理。

  • 系统：指证明系统，由一系列公理以及证明（推论）规则组成。譬如霍尔证明系统。
  • 能行的：一个系统是能行的，意思是系统能够判断输入的规则实例是否是系统内的一个规则实例。事实上，从公理开始利用推论规则可以证明一系列定理，由于是从公理出发以及系统的完备性（保持有效性），每条定理都是有效的。而能行的系统可以判断输入一条断言（或以该断言为结论的一个规则实例），该断言（或规则实例）是否是系统内可以由公理推出的定理（或系统内的规则实例）。

哥德尔不完备性定理意味着不存在部分正确性断言的能行的证明系统。换句话说，对于每一个证明系统，总有这样的断言存在，它既无法被这个系统证明，也无法被这个系统证伪。

  • 命题：对部分正确性断言，不存在一个能行的证明系统，使得其定理恰好是有效的部分正确性断言。

    （注：有效的部分正确性断言即为总是成立的断言，即是 “正确的断言”。但总有有效的部分正确性断言不是定理，即不能被证明系统证明或证伪。）

# 最弱前置条件与可表达性

  • 考察在霍尔系统下证明：

    {A}c0;c1{B}\{A\}c_0;c_1\{B\}

    为了使用复合规则，我们需要一个中间断言CC，使得

    {A}c0{C},{C}c1{B}\{A\}c_0\{C\},\{C\}c_1\{B\}

    都是可证明的。我们是怎么知道这样一个中间断言CC 一定能找到呢？一个充分条件是，对每条命令cc 和后置条件BB，我们能用 Assn 表示它们的最弱前置条件。

  • 设c∈Com,B∈Assn,Ic\in Com,B\in Assn,I 是解释，则 B 关于解释 I 对应于 c 的最弱前置条件wpI[c,B]wp^I[c,B]（空心中括号）定义为：

    wpI[c,B]={σ∈Σ⊥∣C[c]σ⊨IB}wp^I[c,B]=\{\sigma\in\Sigma_\perp|\mathscr{C}[c]\sigma\models^I B\}

    wpI[c,B]wp^I[c,B] 即为所有满足最弱前置条件的状态的集合，在这些状态下执行 c，要么发散，要么终止于满足 B 的终态。

    于是如果⊨I{A}c{B}\models^I\{A\}c\{B\}，当且仅当有AI⊆wpI[c,B]A^I\subseteq wp^I[c,B]。（回忆一下，AIA^I 表示在解释 I 下满足 A 的状态的集合）

  • 假设存在断言A0A_0，使得对于所有的解释II，有

    A0I=wpI[c,B]A_0^I=wp^I[c,B]

    于是对所有的解释II，有

    ⊨I{A}c{B}iff⊨I(A⇒A0)\models^I\{A\}c\{B\}\quad iff\quad\models^I(A\Rightarrow A_0)

    即AI⊆A0IA^I\subseteq A_0^I。于是有

    ⊨{A}c{B}iff⊨(A⇒A0)\models\{A\}c\{B\}\quad iff\quad \models(A\Rightarrow A_0)

    A0A_0 是一个断言，使得∀I,A0I=wpI[c,B]\forall I,A_0^I=wp^I[c,B]。

    这解释了啥叫 “最弱前置条件”，即任何一个使部分正确性断言有效的前置条件AA 可以推出A0A_0。但是特定的断言语言（Assn 之外）并不一定都包含断言A0A_0，使得A0I=wpI[c,B]A_0^I=wp^I[c,B]。

  • 定义，称AssnAssn 是可表达的当且仅当对于每一个命令cc 和断言BB 存在一个断言A0A_0，使得对于任意一个解释 I，都有A0I=wpI[c,B]A_0^I=wp^I[c,B]。

  • 我们用哥德尔的β\beta 谓词对AssnAssn 断言的状态序列进行编码。β\beta 为此包含了求 a 除以 b 的余数模运算a  mod  ba\;mod\;b。我们用 Assn 的断言来解释下什么是 mod 运算。对x=a  mod  bx=a\;mod\;b，记作：

    a≥0∧b≥0∧∃k,[0≤x<b∧x=a−(k×b)]a\geq 0\wedge b\geq 0\wedge\exists k,[0\leq x<b\wedge x=a-(k\times b)]

    设β(a,b,i,x)\beta(a,b,i,x) 是定义在自然数上的谓词（也可以理解为一个断言，命题），定义为

    β(a,b,i,x):x=a  mod  (1+(1+i)×b)\beta(a,b,i,x):x=a\;mod\;(1+(1+i)\times b)

    这有啥用呢，实际上，任何一个由k+1k+1 个自然数构成的序列n0,...,nkn_0,...,n_k 都可以编码成一对数n,mn,m。

  • 对于自然数的任一序列n