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

# IMP 的指称语义

# 目的

以 IMP 语言为例：

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

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

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

# 指称语义

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

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

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

# 算术表达式的指称

结构归纳法定义：

$$\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 表达法重写定义：

$$\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)\\$$

# 布尔表达式的指称

$$\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]\}$$

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

# 命令的指称

$$\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\equiv while\;b\;do\;c$ 的情况，这个比较麻烦。首先有$w\sim if\;b\;then\;c;w\;else\;skip$。于是根据条件命令的指称，我们有：

$$\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$ 表示$\mathscr{C}[w]$，$\beta$ 表示$\mathscr{B}[b]$，$\gamma$ 表示$\mathscr{C}[c]$，于是有：

$$\varphi=\{(\sigma,\sigma')|\beta(\sigma)=true,(\sigma,\sigma')\in\varphi\circ\gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}$$

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

$$\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$ 的一个不动点。考虑命令规则示例集合$R$：

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

$$R=\{\frac{\{(\sigma'',\sigma')\}}{(\sigma,\sigma')}|\beta(\sigma)=true,(\sigma,\sigma'')\in\gamma\}\cup\{\frac{\emptyset}{(\sigma,\sigma)}|\beta(\sigma)=false\}$$

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

$$\hat{R}(f)=\{(\sigma,\sigma')|\exists \sigma'',(\sigma'',\sigma')\in f,(\sigma,\sigma'')\in \gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}\\ =\Gamma(f)$$

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

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

其中，$\Gamma(f)=\{(\sigma,\sigma')|\beta(\sigma)=true,(\sigma,\sigma')\in f\circ\gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}$。

# 语义的等价性

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

  $$\mathscr{A}[a]=\{(\sigma,n)|\lang a,\sigma\rang\rightarrow n\}$$

  对所有的$b\in Bexp$，有

  $$\mathscr{B}[b]=\{(\sigma,t)|\lang b,\sigma\rang\rightarrow t\}$$

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

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

  $$\lang c,\sigma\rang\rightarrow\sigma'\Rightarrow(\sigma,\sigma')\in\mathscr{C}[c]$$

  证明：定义性质 P：

  $$P(c,\sigma,\sigma')\Leftrightarrow\lang c,\sigma\rang\rightarrow\sigma'\Rightarrow(\sigma,\sigma')\in\mathscr{C}[c]$$

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

  • $c\equiv c_0;c_1$，引入前提：

    $$\lang c_0,\sigma\rang\rightarrow \sigma''\& P(c_0,\sigma,\sigma'')\&\lang c_1,\sigma''\rang\rightarrow\sigma'\&P(c_1,\sigma'',\sigma')$$

    然后有

    $$(\sigma,\sigma'')\in\mathscr{C}[c_0],(\sigma'',\sigma')\in\mathscr{C}[c_1]$$

    所以

    $$(\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\equiv while\;b\;do\;c$，条件为真的情况。引入前提：

    $$\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')$$

    根据前提和性质，推得：

    $$(\sigma,\sigma'')\in\mathscr{C}[c],(\sigma'',\sigma')\in\mathscr{C}[w]$$

    即

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

    再由指称语义的定义，有

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

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

• 事实上，有：

  $$\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/y$ 的一组规则实例，给定集合 B，有算子$\hat{R}$：

  $$\hat{R}(B)=\{y|\exists (X/y)\in R,X\subseteq B\}$$

  以及考察如何用集合链

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

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

  $$fix(\hat{R})=\bigcup_{n\in\omega}\hat{R}^n(\emptyset)$$

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

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

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

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

  $$\forall q\in X,q\sqsubseteq p$$

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

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

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

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

  $$d_0\sqsubseteq_D d_1\sqsubseteq_D...\sqsubseteq_D d_n\sqsubseteq_D...$$

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

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

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

• 考察用规则实例集合$R$ 定义的算子，若$B_0\subseteq B_1\subseteq ...\subseteq B_n\subseteq ...$，则有：

  $$\hat{R}(B_0)\subseteq \hat{R}(B_1)\subseteq...\subseteq\hat{R}(B_n)\subseteq...$$

  又因为$\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)$，所以有：

  $$\bigcup_{n\in\omega}\hat{R}(B_n)\subseteq \hat{R}(\bigcup_{n\in\omega} B_n)$$

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

  $$\exists n,X\subseteq B_n\\ \therefore y\in\hat{R}(B_n)\\ \therefore y\in\bigcup_{n\in\omega}\hat{R}(B_n)$$

  所以$\hat{R}(\bigcup_{n\in\omega} B_n)\subseteq\bigcup_{n\in\omega}\hat{R}(B_n)$。综上，有:

  $$\hat{R}(\bigcup_{n\in\omega} B_n)=\bigcup_{n\in\omega}\hat{R}(B_n)$$

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

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

  $$\forall d,d'\in D,d\sqsubseteq_D d'\Rightarrow f(d)\sqsubseteq_Ef(d')$$

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

  $$\bigsqcup_{n\in\omega}f(d_n)=f(\bigsqcup_{n\in\omega}d_n)$$

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

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

  $$fix(f)=\bigsqcup_{n\in\omega}f^n(\perp)$$

  则$fix(f)$ 是 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,

  $$\perp\sqsubseteq d\Rightarrow f(\perp)\sqsubseteq f(d)\sqsubseteq d$$

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

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

# Knaster-Tarski 定理

• 对一组规则实例 R，有

  $$I_R=\bigcap\{Q|Q对R封闭\}$$

  命题等价为：

  $$fix(\hat{R})=\bigcap\{Q|\hat{R}(Q)\subseteq Q\}$$

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

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

  $$\forall q\in X,p\sqsubseteq q$$

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

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

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

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

  $$m=\sqcap\{x\in L|f(x)\sqsubseteq x\}$$

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

  $$M=\bigsqcup\{x\in L|x\sqsubseteq f(x)\}$$

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

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

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

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

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

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

# IMP 的公理语义

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

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

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

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

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

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

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

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

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

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

  $$\{A\}c\{B\}:\forall\sigma\models A\Rightarrow\mathscr{C}[c]\sigma\models B$$

# 断言语言 Assn

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

  $$a::=n|X|i|a_0+a_1|a_0-a_1|a_0\times a_1$$

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

  然后，扩充$Bexp$：

  $$b::=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)$ 为算术表达式$a\in Aexpv$（扩充集合）中的自由变量集合，有：

  $$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)=\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]$。首先用以下结构归纳法定义算术表达式中的代入：

  $$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]=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$$

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

  $$A=(i\geq 1)\wedge(\forall i,i=1)$$

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

# 断言的语义

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

  $$\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\in Aexpv$，对所有的状态$\sigma$ 和所有解释$I$ 都有

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

  这个结构归纳一下就好。

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

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

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

  $$\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\in Bexp$，$\sigma\in\Sigma$ 和任一解释 I，有$\mathscr{B}[b]\sigma=true$ 当且仅当$\sigma\models^I b$。

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

  $$A^I=\{\sigma\in\Sigma_\perp|\sigma\models^I A\}$$

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

• 部分正确性断言形如

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

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

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

  $$\sigma\models^I\{A\}c\{B\}\quad iff\quad (\sigma\models^I A\Rightarrow \mathscr{C}[c]\sigma\models^I B)$$

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

---

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

  $$\forall\sigma\in\Sigma_\perp,\sigma\models^I\{A\}c\{B\}$$

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

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

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

  $$\models\{A\}c\{B\}$$

  表示对所有的解释$I$ 和所有的状态$\sigma$ ，有

  $$\sigma\models^I\{A\}c\{B\}$$

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

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

  $$\forall\sigma\in\Sigma_\perp,((\sigma\models^I A)\Rightarrow(\sigma\models^I B))$$

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

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

  $$\forall\sigma\in\Sigma_\perp,((\sigma\models^I A)\Rightarrow(\mathscr{C}[c]\sigma\models^I B))$$

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

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

• skip 规则：

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

• 赋值规则：

$$\{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$。

• 顺序复合规则：

$$\frac{\{A\}c_0\{C\}\quad\{C\}c_1\{B\}}{\{A\}c_0;c_1\{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 循环规则：

$$\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\}$，不需要前提就是有效的。

• 推论规则：

  $$\frac{\models(A\Rightarrow A')\quad\{A'\}c\{B'\}\quad\models(B'\Rightarrow B)}{\{A\}c\{B\}}$$

---

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

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

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

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

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

• 引理：对$a,a_0\in Aexpv,X\in Loc$，则对所有的解释$I$ 和状态$\sigma$，有：

  $$\mathscr{A}v[a_0[a/X]]I\sigma=\mathscr{A}v[a_0]I\sigma[\mathscr{A}v[a]I\sigma/X]$$

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

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

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

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

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

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

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

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

    $$\forall\sigma\in\Sigma,\sigma\models^IB[a/X]\Leftrightarrow\sigma[\mathscr{A}[a]\sigma/X]\models^I B$$

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

    $$\forall\sigma\in\Sigma,\sigma\models^I B[a/X]\Rightarrow\mathscr{C}[X:=a]\sigma\models^I B$$

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

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

    $$\models\{A\}c_0\{C\},\models\{C\}c_1\{B\}$$

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

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

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

    $$\models\{A\wedge b\}c_0\{B\},\models\{A\wedge \neg b\}c_1\{B\}$$

    对于任意一个解释$I$ 状态$\sigma$，若有$\sigma\models^I A$，则或$\sigma\models^I b$ 或$\sigma\models^I\neg b$。对于前一种情况，有$\sigma\models^I A\wedge b$。

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

    因此有$\mathscr{C}[if\;b\;c_0\;else\;c_1]\sigma\models^I 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 循环：引入规则前提有效：

    $$\models\{A\wedge b\}c\{A\}$$

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

    $$\mathscr{C}[w]=\bigcup_{n\in\omega}\theta_n$$

    其中

    $$\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)\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 成立，则有

    $$\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$$

    即$\forall\sigma\in \Sigma,\sigma\models^I A\Rightarrow\mathscr{C}[w]\sigma\models^I A\wedge\neg b$，即有$\models \{A\}w\{A\wedge\neg b\}$。

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

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

      若$\mathscr{B}[b]\sigma=false\& \sigma'=\sigma$，于是$\mathscr{B}[b]\sigma'=false$，于是$\sigma\models^I A\Rightarrow\sigma'\models^I A\wedge\neg b$。

      若$\mathscr{B}[b]\sigma=true\&(\sigma,\sigma')\in\theta_n\circ\mathscr{C}[c]$，于是$\exists\sigma'',(\sigma,\sigma'')\in\mathscr{C}[c]$。

      $$\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$$

      因此得到证明成立。

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

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

    $$\models(A\Rightarrow A'),\models\{A'\}c\{B'\},\models(B'\Rightarrow B)$$

    于是有

    $$\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$$

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

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

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

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

考虑一个不变式

$$I\equiv(Y\times X!=n!\wedge X\geq 0)$$

先证明它确实是一个不变式，即$\{I\wedge X>0\}w\{I\}$（当然，$\{I\wedge X\leq 0\}w\{I\}$ 是显然的，结合起来就有$\{I\}w\{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]=Y\times(X-1)!=n!\wedge(X-1)\geq 0$。再根据赋值规则，有：

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

这样，由顺序规则，有：

$$\{X\times Y\times(X-1)!=n!\wedge(X-1)\geq 0\}Y:=X\times Y;X:=X-1\{I\}$$

而

$$I\wedge X>0\Rightarrow X\times Y\times(X-1)!=n!\wedge X>0\\ \Rightarrow Y\times X!=n!\wedge (X-1)\geq 0$$

于是根据推论规则，有：

$$\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 循环规则，有：

$$\frac{\{I\wedge X>0\}Y:=X\times Y;X=X-1\{I\}}{\{I\}w\{I\wedge\neg X>0\}}$$

显然有

$$\models((X=n)\wedge(n\geq 0)\wedge(Y=1)\Rightarrow I)$$

且

$$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!$$

于是根据推论规则，有

$$\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 一定要可以推出循环结束后的状态。在本例种，$I$+$\neg X>0$ 就可以推出跳出循环时，$X=0$。

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

# 霍尔规则的完备性

# 哥德尔不完备性定理

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

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

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

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

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

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

  $$\{A\}c_0;c_1\{B\}$$

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

  $$\{A\}c_0\{C\},\{C\}c_1\{B\}$$

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

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

  $$wp^I[c,B]=\{\sigma\in\Sigma_\perp|\mathscr{C}[c]\sigma\models^I B\}$$

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

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

• 假设存在断言$A_0$，使得对于所有的解释$I$，有

  $$A_0^I=wp^I[c,B]$$

  于是对所有的解释$I$，有

  $$\models^I\{A\}c\{B\}\quad iff\quad\models^I(A\Rightarrow A_0)$$

  即$A^I\subseteq A_0^I$。于是有

  $$\models\{A\}c\{B\}\quad iff\quad \models(A\Rightarrow A_0)$$

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

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

---

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

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

  $$a\geq 0\wedge b\geq 0\wedge\exists k,[0\leq x<b\wedge x=a-(k\times b)]$$

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

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

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

• 对于自然数的任一序列$n_0,...,n_k$，存在自然数$n,m$，使得对所有的$j\in[0,k]$ 以及所有的 x，有

  $$\beta(n,m,j,x)\Leftrightarrow x=n_j$$

  证明：令$m=(max\{k,n_0,...,n_k\})!,p_i=1+(1+i)\times m$，于是有$p_i,p_j$ 两两互质，因为$p_i,p_j-p_i$ 是互质的（欧几里得辗转相减）。

  继续令$c_i=\frac{\prod_{t=0}^{k} p_t}{p_i}$。显然$c_i$ 与$p_i$ 是互质的。（因为$k$ 个与$p_i$ 互质的数乘起来仍与$p_i$ 互质）因此存在唯一的$c_i$ 的乘法逆元$d_i$ 使得

  $$c_i\times d_i\equiv 1(mod\; p_i)$$

  于是令$n=\sum_{i=0}^k c_i\times d_i\times n_i$，就会有

  $$\forall i\in[0,k],n_i=n\;mod\;p_i$$

  因为$j\neq i$ 时，$c_j\times d_j\times n_j\;mod\;p_i=0$。（$c_j$ 是$p_i$ 的倍数）

  而$c_i\times d_i\times n_i\;mod\;p_i=n_i\;mod\;p_i$，所以$n\equiv n_i(mod\;p_i)$。

---

• 定义谓词：

  $$F(x,y)\equiv x\geq 0\&\exists z\geq 0,[(x=2\times z\Rightarrow y=z)\&(x=2\times z-1\Rightarrow y=-z)]\\ x,y,z\in N$$

  则定义$\beta^\pm$ 为：

  $$\beta^\pm(n,m,j,y)\Leftrightarrow \exists x,(\beta(n,m,j,x)\wedge F(x,y))$$

  说人话就是，若$\beta^\pm(n,m,j,x)$ 为真时，有：

  $$n_j=\begin{cases}x/2=n\;mod\;(1+(1+j)\times m)&x\%2=0\\ -(x+1)/2=-(n\;mod\;(1+(1+j)\times n))&x\%2=1 \end{cases}$$

# 证明 Assn 是可表达的

施结构归纳于命令$c$。证明对所有的断言$B$，都存在一个断言$w[c,B]$ 使得对于所有的解释 I 和命令 c，都有

$$wp^I[c,B]=w[c,B]^I$$

根据最弱前置条件的定义，对于解释$I$，$wp^I[c,B]=w[c,B]^I$，我们即要证明：

$$\sigma\models^I w[c,B]\quad iff\quad \mathscr{C}[c]\sigma\models^I B$$

• $c\equiv skip$，此时取$w[skip,B]\equiv B$。显然对所有的状态$\sigma$ 和解释$I$ 有

  $$\sigma\in wp^I[skip,B]\quad iff\quad \mathscr{C}[skip]\sigma\models^I B\\ iff\quad \sigma\models^I B\\ iff\quad \sigma\models^I w[skip,B]$$

  第一行是根据最弱前置条件的定义。

  第二行是根据指称语义的定义。

  第三行是因为取的$B\equiv w[skip,B]$。

• $c\equiv X:=a$，此时取$w[X:=a,B]\equiv B[a/X]$。于是

  $$\sigma\in wp^I[X:=a,B]\quad iff\quad\sigma[\mathscr{A}[a]\sigma/X]\models^I B\\ iff\quad \sigma\models^I B[a/X]\\ iff\quad \sigma\models^I w[X:=a,B]$$

  第一行是根据最弱前置条件的定义和指称语义的定义$\mathscr{C}[X:=a]=\{(\sigma,\sigma[n/X])|\sigma\in \Sigma,n=\mathscr{A}[a]\sigma\}$

  第二行是根据 “霍尔规则的完备性和可靠性” 一节中的第二个引理。

  第三行是因为这么取得$w[X:=a,B]$。

• $c\equiv c_0;c_1$，此时归纳定义取$w[c,B]=w[c_0,w[c_1,B]]$。对任意$\sigma,I$，有

  $$\sigma\in wp^I[c_0;c_1,B]\quad iff\quad \mathscr{C}[c_0;c_1]\sigma\models^I B\\ iff\quad \mathscr{C}[c_1](\mathscr{C}[c_0](\sigma))\models ^I B\\ iff\quad \mathscr{C}[c_0]\sigma\models^I w[c_1,B]\\ iff\quad \sigma\models^I w[c_0,w[c_1,B]]\\ iff\quad \sigma\models^I w[c_0;c_1,B]$$

  第一行是根据最弱前置条件的定义。

  第二行是根据顺序命令的指称语义。

  第三行是因为归纳假设$w[c_1,B]^I=wp^I[c_1,B]$，以及最弱前置条件的定义。

  $\mathscr{C}[c_1]\sigma\models^I B\Leftrightarrow\sigma\in wp^I[c_1,B]=w[c_1,B]^I$
  

  第四行也是因为归纳假设$w[c_0,B]^I=wp^I[c_0,B]$，以及最弱前置条件的定义。

  最后一行是因为取得$w[c,B]=w[c_0,w[c_1,B]]$。

• $c\equiv if\;b\;then\;c_0\;else\;c_1$，归纳定义

  $$w[if\;b\;then\;c_0\;else\;c_1,B]\equiv[(b\wedge w[c_0,B])\vee(\neg b\wedge w[c_1,B])]$$

  于是，对所有$\sigma,I$，有

  $$\sigma\in wp^I[c,B]\quad iff\quad \mathscr{C}[c]\sigma\models^I B\\ iff\quad (\mathscr{B}[b]\sigma=true\&\mathscr{C}[c_0]\sigma\models^I B)\;or\;(\mathscr{C}[b]\sigma=false\&\mathscr{C}[c_1]\sigma\models^I B)\\ iff\quad (\sigma\models^I b\& \sigma\in w^I[c_0,B])\;or\;(\sigma\models^I \neg b\&\sigma\in w^I[c_1,B])\\ iff\quad\sigma\models^I((b\wedge w[c_0,B])\vee(\neg b\wedge w[c_1,B]))\\ iff\quad\sigma\models^I w[c,B]$$

  第一行是根据最弱前置条件的定义。

  第二行是根据条件命令指称语义的定义。

  第三行是根据 Assn 断言的语义（在解释 I 下$\mathscr{C}[b]\sigma=true$ 当且仅当$\sigma\models^I b$）

  第四行是恒等变换，根据$\sigma\models^I w[c_0,B]\Leftrightarrow \sigma\in w^I[c_0,B]$。

  第五行是这么因为就是这么取的。

• $c\equiv while\;b\;do\;c_0$ 太复杂了（略（看书

---

总之，$Assn$ 中的任意一条断言作为后置条件和任意一条命令 c，都有最弱前置条件$w[c,B]$ 满足

$w[c,B]^I=wp^I[c,B]=\{\sigma\in\Sigma_\perp|\mathscr{C}[c]\sigma\models^I B\}$。

• 引理，对于最弱前置条件$w[c,B]$，有$\vdash\{w[c,B]\}c\{B\}$。

• 定理，若$\models\{A\}c\{B\}$，则有$\vdash\{A\}c\{B\}$。

  即，霍尔证明系统下，对部分正确性断言是完备的。所有有效的部分正确性断言都可以得到证明。（但注意不是所有有效的断言，譬如不应该有$\models A\Rightarrow\vdash A$，这是哥德尔不完备性定理告诉我们的。

# 验证条件

• 部分正确性断言$\{A\}c\{B\}$ 的有效性等价于小区命令 c 后的断言：$A\Rightarrow w[c,B]$ 的有效性。即$\{A\}c\{B\}$ 等价于$A\Rightarrow [c,B]$。

• 我们用断言来注释程序，定义有注释的命令的语法集合为：

  $$c::=skip|X:=a|c_0;(X:=a)|c_0;\{D\}c_1|if\;b\;then\;c_0\;else\;c_1|while\;b\;do\;\{D\}c$$

  其中$c_0,c_1$ 为带注释的命令。而$c_0;\{D\}c_1$ 中 D 是断言，$c_1$ 不是赋值命令。注释描述了状态，是一个执行命令时状态应该满足的条件，或者按书上说，控制流程到达命令的注释点时，该点的断言为真。

• 考虑部分性断言：

  $$\{A\}while\;b\;do\;\{D\}c\{B\}$$

  我们希望选择的 D 是一个不变式，即满足：$\{D\wedge b\}c\{D\}$。所以要证明上面那个部分性断言，只需证明：

  $$A\Rightarrow D,D\wedge\neg b\Rightarrow B$$

  类似地，要证明一个带注释的部分正确性断言，实际上只需要证明一些验证条件。然后可以通过霍尔规则证明部分正确性断言。

  验证条件中，命令是被消去的。记$vc(\{A\}c\{B\})$ 是部分正确性断言的验证条件：

  $$vc(\{A\}skip\{B\})=\{A\Rightarrow B\}\\ vc(\{A\}X:=a\{B\})=\{A\Rightarrow B[a/X]\}\\ vc(\{A\}c_0;X:=a\{B\})=vc(\{A\}c_0\{B[a/X]\})\\ vc(\{A\}c_0;\{D\}c_1\{B\})=vc(\{A\}c_0\{D\})\cup vc(\{D\}c_1\{B\})\\ vc(\{A\}if\;b\;then\;c_0\;else\;c_1\{B\})=vc(\{A\wedge b\}c_0\{B\})\cup vc(\{A\wedge\neg b\}c_1\{B\})\\ vc(\{A\}while\;b\;do\;\{D\}c\{B\})=vc(\{D\wedge b\}c\{D\})\cup\{A\Rightarrow D\}\cup\{D\wedge\neg b\Rightarrow B\}$$

  因此，要证明$\{A\}c\{B\}$ 是有效的，只需要证明$vc(\{A\}c\{B\})$ 集合中每条断言都是有效的即可。

# 谓词转换器 *

• 我们把命令抽象地表示为一个函数：$f:\Sigma\rightarrow\Sigma_\perp$。称这样的函数为状态转换器。我们抽象地把部分正确性断言表示成含有$\perp$ 状态的子集，而把部分正确性谓词定义为：

  $$Pred(\Sigma)=\{Q|Q\subseteq \Sigma_\perp\&\perp\in Q\}$$

  可以按照$\supseteq$ 关系把这些谓词排成一个完全偏序：$(Pred(\Sigma),\supseteq)$。

  最弱前置条件的结构确定了谓词的完全偏序的连续函数 —— 谓词转换器。

• 定义，设$f:\Sigma\rightarrow\Sigma_\perp$ 是状态的部分函数，定义：

  $$Wf:Pred(\Sigma)\rightarrow Pred(\Sigma)\\ (Wf)(Q)=(f^{-1}Q)\cup\{\perp\}\\ 即，(Wf)(Q)=\{\sigma\in\Sigma|f(\sigma)\in Q\}\cup\{\perp\}$$

  命令 c 指称状态状态转换器：$\mathscr{C}[c]:\Sigma\rightarrow\Sigma_\perp$，设 B 是一个断言，对应于解释 I 有：

  $$(W(\mathscr{C}[c]))B^I=wp^I[c,B]$$

• 理解一条命令等于理解确保后置条件为真的最弱前置条件。—— 迪杰斯特拉。

• 我们不再用状态转换器而用谓词转换器来表示 IMP 命令的指称语义，定义从命令到谓词转换器的语义函数：

  $$\mathscr{P}t:Com\rightarrow[Pred(\Sigma)\rightarrow Pred(\Sigma)]$$

# 不完备性和不可判定性

# 可计算性

• 一个 IMP 命令$c$ 可以和$N$ 上的一个部分函数相关联。我们假定，将所有的存储单元排列为$X_1,X_2,X_3,...$。设在状态$\sigma_0$ 下，所有的存储单元内容都是 0。对于$n\in N$，定义:

  $$\{c\}(n)=\begin{cases}\sigma(X_1)&\sigma=\mathscr{C}[c]\sigma_0[n/X_1]\\undefined&\mathscr{C}[c]\sigma_0[n/X_1]\;is\;undefined\end{cases}$$

  任一$N\rightarrow N$ 的部分函数，若对某一命令$c$，能使$n\longmapsto \{c\}(n)$，其中$n\in N$，则称该函数是 IMP 可计算的。这样的函数也被称为是 “部分递归的”。如果是全函数，则称为 “递归的”。更一般地，可以定义$N^k\rightarrow N$ 的 IMP 可计算函数：

  $$\{c\}(n_1,...,n_k)=\begin{cases}\sigma(X_1)&\sigma=\mathscr{C}[c]\sigma_0[n_1/X_1,...,n_k/X_k]\\ undefined&\mathscr{C}[c]\sigma_0[n_1/X_1,...,n_k/X_k]\;is\;undefined \end{cases}$$

  譬如函数$f(n)=n+1$，则有对应$n\longmapsto f(n)=n+1=\{X_1:=n+1\}(n)$

  • 这是什么概念呢，根据我的理解，实际上意思就是抽象的数学函数的内容可以用 IMP 命令来描述。也就是 “借用了”$X_1$ 存储单元，先把函数输入 n 存进去得到$\sigma_0[n/X_1]$，然后执行命令 c（相当于函数操作），然后再取出$X_1$ 的值，得到函数的输出值。

• 定义，称 IMP 命令 c 是整洁的当且仅当对所有的状态$\sigma$ 和数$n$，有

  $$\mathscr{C}[c]\sigma_0[n/X_1]=\sigma\Rightarrow\sigma[0/X_1]=\sigma_0$$

  根据我的理解，$c$ 执行后内容发生改变的存储单元只能有$X_1$。

• 命题，设$c_0,c_1$ 是命令，且$c_0$ 是整洁的。对任意$n,m\in N$，有

  $$\{c_1\}(\{c_0\}(n))=m\quad iff\quad \{c_0;c_1\}(n)=m$$

  为什么要求$c_0$ 是整洁的呢？因为$c_0$ 是整洁的，所以$\{c_0\}(n)$ 取出$X_1$ 的内容后，剩下的状态就正好是$\sigma_0[\{c_0\}(n)/X_1]$（其他单元格都没发生内容变化），正好符合了$\{c_1\}(\{c_0\}(n))$ 外层要求的$\sigma=\mathscr{C}[c_1]\sigma_0[\{c_0\}(n)/X_1]$。

  即在计算$\{c\}(n)$ 时一个重要的要求是，刚开始状态为$\sigma_0$。然后把 n 存进$X_1$，执行$c$，再取出$X_1$ 的内容。如果$c$ 不是整洁的，那么将破坏状态不能继续用了。

• 记号，$f(n)\downarrow$ 表示$\exists m,f(n)=m$。即结果有定义。否则$f(n)\not\downarrow$ 表示结果没定义。而$\{c\}(n)\downarrow$ 就表示状态$\sigma_0[n/X_1]$ 在执行命令 c 后终止了。

• 对于 N 的一个子集 M，称其为 IMP 可检查的，当且仅当存在一个 IMP 命令 c，使得

  $$n\in M\quad iff\quad \{c\}(n)\downarrow$$

  可检查集合也称为 “递归可枚举” 集。

  对于 N 的一个子集 M，称其为 IMP 可判定的，当且仅当存在一个 IMP 命令 c，使得

  $$n\in M\Rightarrow\{c\}(n)=1\\ n\notin M\Rightarrow\{c\}(n)=0$$

  可判定集合有时也称作 “递归” 集。

  很显然地，若命令 c 可以用来 “判定” 是否$n\in M$，那么命令：

  $$c;if\;X_1=1\;then\;skip\;else\;Diverge$$

  （其中$Diverge=while\;true\;do\;skip$）就可以用来 “检查” 是否$n\in M$。

  所以可判定集合一定是可检查的。而且$M$ 是可判定的话，有$\bar{M}=N-M$ 也是可判定的（命令最后加一个$X_1:=1-X_1$）。

• 反之，若$c_1$ 可以用来检查 M，$c_2$ 可以用来检查$\bar{M}$，则可以通过使$c_1,c_2$ 来构造命令$c$，从而得到$M$ 的判定者：

  设$T,F,S$ 是不属于$Loc(c_1)\cup Loc(c_2)$ 的其他存储单元，把$Loc(c_i)-\{X_i\}$ 清零的赋值命令记为$Clear_i$，于是命令 c 为：

  $T:=X_1;$

  $F:=0;$

  $S:=1;$

  $while\;F=0\;do$

  $Clear_1;X_1:=T;$
  
  执行$c_1 S$次，或直到$c_1halts$。
  
  $if\;c_1$在执行$S$次内$halt$了$\;then$
  
  $F:=1;$
  
  $X_1:=1;$
  
  $else\;S:=S+1;$
  
  $if\;F=1\;then\;skip\;else$
  
  $Clear_2;X_1=T;$
  
  执行$c_2 S$次，或直到$c_2halts$。
  
  $if\;c_2$在执行$S$次内$halt$了$\;then$
  
  $F:=1;$
  
  $X_1:=0;$
  
  $else\;S:=S+1;$
  

  $Clear_1;Clear_2;T:=0;F:=0;S:=0;$

  这段代码就是在执行 $c_1$1次，执行$ c_2$2次，执行$ c_1$3次，....直到有一个$ halts$ 了。我也不知道为啥需要执行多次。

• 定理，集合$M$ 是可判定的当且仅当$M$ 和$\bar{M}$ 都是可检查的。

# 不可判定性

通过对命令进行编码，将它们转换为一些数，我们可以将它们作为其他命令的输入。

• 设$mkpair$ 是整数对的配对函数，譬如

  $$mkpair(n,m)=2^{sg(n)}\times3^{|n|}\times 5^{sg(m)}\times 7^{|m|}$$

  其中$sg(n)$ 为符号函数，n 为负数为 0，否则为 1。配对函数的细节无关紧要，重要的是有两个函数$left,right$，使得：

  $$left(mkpair(n,m))=n\\ right(mkpair(n,m))=m$$

  此外，还有一些类似于赋值语句的$IMP命令$，形式为：

  $$X:=mkpair(Y,Z)\\ X:=left(Y)\\ X:=right(Y)$$

• 此时可以将命令编为数。

  $$\#(X_i)=mkloc(i)=mkpair(0,i)\\ \#(n)=mknum(n)=mkpair(1,n)\\ \#(a_1+a_2)=mksum(\#a_1,\#a_2)=mkpair(2,mkpair(\#a_1,\#a_2))$$

  用 2，3，4 分别对$+,-,\times$ 的左项来编码。

  用 5，6，7，8，9 分别为$\leq,=,\wedge,\vee,\neg$ 的标志对布尔表达式编码，例如

  $$\#(a_1\leq a_2)=mkpair(5,mkpair(\# a_1,\# a_2))$$

  用 10，11，12，13 分别为$:=,skip,if,$ 顺序$,while$ 编码。例如

  $$\#(X_i:=a)=mkpair(10,mkpair(\#X_i,\#a))\\ \#(if\;b\;then\;c_0\;else\;c_1)=mkpair(12,mkpair(\#b,mkpair(\#c_0,\#c_1)))$$

  $\#(c)$ 也称为 c 的哥德尔数。我查到的是，任意一个命令的哥德尔数实际上就是

  $$enc(x_1,x_2,...,x_n)=2^{x_1}3^{x_2}...p_n^{x_n}$$

  就是素数幂的乘积。然后因为任意一个数素因子分解是唯一的，也可以从左到右还原。

• 我们称$Com$ 的一个子集$S$ 是可检查的（或可判定的），如果它们的编码集合

  $$\{\#c|c\in S\}$$

  是可检查的（或可判定的）。

• 设 H 为 “自停（self-halting）” 命令集：

  $$H=\{c|\{c\}(\#c)\downarrow\}$$

  $\bar{H}=Com-H$。

  定理，$\bar{H}$ 不是 IMP 可检查的。

  证明：反设存在一个命令 C 来检查$\bar{H}$，有

  $$c\in\bar{H}\quad iff\quad \{C\}(\# c)\downarrow$$

  又因为C子集也是一个命令，我们来检测C是否在$\bar{H}$里。
  

  $$C\in\bar{H}\quad iff\quad\{C\}(\#C)\downarrow$$

  而$\bar{H}$的定义又要求
  

  $$C\in\bar{H}\Rightarrow \{C\}\{\#C\}\not\downarrow$$

  于是矛盾，故任何一个可能检查$\bar{H}$的命令都无法检查它自己。
  

  推论，$H$ 不是 IMP 可判定的。因为定理：集合$M$ 是可判定的当且仅当$M$ 和$\bar{M}$ 都是可检查的。

• 譬如定义一个$H_0=\{c\in Com|\mathscr{C}[c]\sigma_0\neq\perp\}$，实际上$\mathscr{C}[c]\sigma_0\neq\perp\Leftrightarrow\{c\}(0)\downarrow$。

  零状态停机定理，$\bar{H_0}$ 是不可检查的。

# 哥德尔不完备性定理

• 我们可以类似对命令的编码，也对断言进行编码并得到其哥德尔数。我们要求

  $$Provable=\{A\in Assn|\vdash A\}$$

  是 IMP 可检查的。设有效断言组成的集合：

  $$Valid=\{A\in Assn|\models A\}$$

---

• 定理，$Valid$ 是不可检查的。

证明：构造函数函数$h$，满足对所有的命令$c$ 有

$$h(\# c)=\#(w[c,false][0/Loc(c)])$$

（$w[c,false]$ 其实就是一个断言，在满足这个断言的状态$\sigma$ 下执行命令 c 就不会停下来。）

因为 Assn 断言都是可表达的，于是$w[c,false][0/Loc(c)]$ 总是存在的，于是总存在命令$W$ 来实现函数$h$。（因为输入$\#c$ 相当于告诉你了命令 c 的内容，然后参考 “Assn 断言都是可表达的 “证明过程构造出 w，再用命令完成编码过程）而且一定可以把 W 构造成整洁的。

假设$Valid$ 是可检查的，即存在一个命令 C，使得对任一断言 A，有

$$A\in Valid\quad iff\quad\{C\}(\# A)\downarrow$$

对于任意一个命令 c，令$A\equiv w[c,false][0/Loc(c)]$，则

$$A\in Valid\quad iff\quad\models w[c,false][0/Loc(c)]\\$$

而

$$\models w[c,false][0/Loc(c)]\\ \Leftrightarrow\\ \forall\sigma,I,\sigma\models^I w[c,false][0/Loc(c)]\\ \Leftrightarrow\\ \forall\sigma,I,\sigma[0/Loc(c)]\models^I w[c,false]\\ \Leftrightarrow\\ \forall\sigma,\mathscr{C}[c]\sigma[0/Loc(c)]=\perp$$

于是

$$A\in Valid\quad iff\quad \forall\sigma,\mathscr{C}[c]\sigma[0/Loc(c)]=\perp\\ iff\quad \{C\}(\# A)\downarrow\\ iff\quad \{C\}(\{W\}(\# c))\downarrow\\ iff\quad \{W;C\}(\#c)\downarrow$$

所以如果$A\in Valid$，那么集合$\{c\in Com|\forall\sigma,\mathscr{C}[c]\sigma[0/Loc(c)]=\perp\}$ 是可由$W;C$ 来检查的。

然而我们可以证明该集合并不可检查。若$Loc(c)=\{X_1,...,X_n\}$，则定义状态：

$$\sigma_0=\{(X_1,0),(X_2,0),...,(X_n,0)\}$$

显然，有$\forall\sigma,\sigma_0\subseteq\sigma[0/Loc(c)]$。然后又因为$c$ 的操作实际上只在$X_1,...,X_n$ 上进行，于是有：

$$\{c\in Com|\forall\sigma,\mathscr{C}[c]\sigma[0/Loc(c)]=\perp\}=\{c\in Com|\mathscr{C}[c]\sigma_0=\perp\}$$

因为集合元素是 c，而且状态的其他存储单元并不会影响同一个 c 的执行是否终止。

实际上，就是要证明$\bar{H_0}=\{c\in Com|\{c\}(0)\not\downarrow\}$ 是不可检查的。

• 反设其为可检查的，于是有命令 C，满足对任意命令 c，有

  $$c\in \bar{H_0}\quad iff\quad \{C\}(\# c)\downarrow$$

  而

  $$c\in\bar{H}\quad iff\quad\{c\}(\# c)\downarrow\\ iff\quad \{X_1:=\#c;c\}(0)\downarrow\\ iff\quad (X_1:=\#c;c)\in\bar{H_0}\\ iff\quad \{C\}(\#(X_1:=\#c;c))\downarrow$$

  然后存在一条命令 W，实现$\{W\}(\# c)=\#(X_1:=\#c;c)$。（挺好构造的）于是

  $$iff\quad\{C\}(\{W\}(\# c))\downarrow\\ iff\quad \{W;C\}(\# c)\downarrow$$

  就有$c\in\bar{H}\quad iff\;\{W;C\}(\#c)\downarrow$。这与$\bar{H}$ 是不可检查的矛盾。故证毕

---

所以实际上，我们有：

$\bar{H}$ 不可检查$\Rightarrow\bar{H_0}$ 不可检查$\Rightarrow Valid$ 不可检查。

实际上，还可以定义：

$$Truth=\{A\in Assn|\models A\& A封闭\&A无存储单元\}$$

即是一种不依赖于系统的，可以说是真理的断言集合。我们有$Truth\subset Provable$。不是所有的真理都是可以证明的。