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

## # 指称语义

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

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

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

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

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

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

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

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

## # 语义的等价性

• 引理：对所有的$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$ 对于 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$都是合理的。


• 推论规则：

$\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\}Y:=X\times Y;X:=X-1\{I\}$

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

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

# # 霍尔规则的完备性

## # 哥德尔不完备性定理

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

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

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

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

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

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

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

$\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}_{}$