ホーム - 程序语言理论

一个没有才华没有灵感的人也没有放弃的资格

# 集合论基础内容

  • 幂集：

    Pow(X)={Y∣Y⊆X}Pow(X)= \{ Y|Y \subseteq X \}

  • ⋃X=⋃i=1nxi,xi∈X\bigcup X=\bigcup_{i=1}^n x_i,x_i\in X

  • 乘积：

    X×Y={(x,y)∣x∈X,y∈Y}X\times Y= \{ (x,y)|x\in X,y\in Y \}

  • 不相交并集：X⊎Y=({0}×X)∪({1}×Y)X\uplus Y=(\{0\}\times X)\cup (\{1\}\times Y)

  • 差集：X∖Y=X−YX\setminus Y=X-Y

  • ω\omega 常表示自然数集。

  • 基本公理：对于任意一个集合b0b_0，属于关系链：bn∈bn−1∈...∈b0b_n\in b_{n-1}\in...\in b_0 一定是有限的

  • 部分函数：X⇀YX\rightharpoonup Y 表示并不是 X 中所有元素都有定义，相对应有完全函数X→YX\rightarrow Y

  • λ\lambda 函数记号：λx∈X.e={(x,e)∣x∈X}\lambda x\in X.e=\{(x,e)|x\in X\}。例：λx∈ω.(x+1)\lambda x\in\omega.(x+1) 就同时描述了定义域和函数内容，即为一个后继函数

  • 康托对角线方法：证明 X 与其幂集不可能一一对应

    假设θ:X→Pow(X)\theta:X\rightarrow Pow(X) 是一一对应的。则构造集合：Y={x∈X∣x∉θ(x)}Y=\{x\in X|x\notin\theta(x)\}，显然 Y 是 X 的一个子集。那么肯定存在一个 y 使得θ(y)=Y\theta(y)=Y。那 y 属于 Y 嘛？此时就矛盾了。

    为啥这叫对角线方法呢？其实如果存在一个X→Pow(X)X\rightarrow Pow(X) 的一一对应，我们可以画一张表，表中aij={0xi∉θ(xj)1xi∈θ(xj)a_{ij}=\begin{cases}0& x_i\notin \theta(x_j)\\1&x_i\in \theta(x_j)\end{cases}，然后 Y 的构造其实就是对角线上为 1 对应的元素，即xi∈θ(xi)x_i\in \theta(x_i)

  • 对一个关系R:X×YR:X\times Y，对 X 的子集 A，定义其正象：

    RA={y∈Y∣∃x∈A,(x,y)∈R}RA=\{y\in Y|\exists x\in A,(x,y)\in R\}

    也可以对 Y 的子集 B 定义其逆象：

    R−1B={x∈X∣∃y∈B,(x,y)∈R}R^{-1}B=\{x\in X|\exists y\in B,(x,y)\in R\}

  • 等价类：

    {x}R={y∈X∣xRy}\{x\}_R=\{y\in X|xRy\}

  • 关系的幂：R0=IdXR^0=Id_X（IdXId_X 是集合 X 上的恒等关系），Rn+1=Rn∘RR^{n+1}=R^n\circ R

  • 传递闭包：将关系 R 中添加尽量少的有序对使其成为具有传递性的关系R+R^+，则有

    R+=⋃n∈ωRn+1R^+=\bigcup_{n\in \omega}R^{n+1}

    传递、自反闭包：将关系 R 中添加尽量少的有序对使其成为具有传递、自反性的关系R∗=IdX∪R+R^*=Id_X\cup R^+

# 操作语义

  • IMP 是一种带 while 的小型程序设计语言，其程序在运行时要依靠一连串的显式命令进行状态转换，因此 IMP 被称为是一种命令式语言。形式上 IMP 由一组规则来描述，规定了表达式如何计算和命令如何执行。规则也是证明命令间等价的基本工具。

# IMP—— 简单的命令式语言

  • IMP 的语法集合有：

    • 数集 (numbers)NN，它是整数集合。
    • 真值集 (truth values)T={true,false}T=\{true,false\}。
    • 存储单元集 (locations)LocLoc。
    • 算术表达式集 (arithmetic expressions)AexpAexp。
    • 布尔表达式集 (boolean expressions)BexpBexp。
    • 命令集 (commands)ComCom。

    其中，数集 N 和存储单元集的语法结构是假设已知的，譬如LocLoc 为非空字母或后跟数字的非空字符串的集合，而NN 为带符号位的正负十进制数的集合。但对于其他语法集合，我们必须说明其元素的构造方式。我们使用BNFBNF（Backus-Naur form）的一种变形形式。构造规则形如：

    如果a0和a1是算术表达式，则a0+a1也是算术表达式。如果a_0和a_1是算术表达式，则a_0+a_1也是算术表达式。

    显然a0a_0 和a1a_1 被用于代表任意算术表达式，称a0a_0 和a1a_1 为元变量。我们用元变量来表示语法集合的元素。

  • n,mn,m 表示数集NN 中的元素

    X,YX,Y 表示存储单元集LocLoc 中的元素

    aa 表示算术表达式集AexpAexp 中的元素

    bb 表示布尔表达式集BexpBexp 中的元素

    cc 表示命令集ComCom 中的元素

    这些元变量都可以添加下标或上标。

  • 算术表达式集AexpAexp 的构造规则可描述如下：

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

    其中::=::= 表示 "可以为"，∣| 表示 “或”（运算优先级最低，书上都不加括号的）。

    这句构造规则的意思是：算术表达式 a 可以为一个数 n，或一个存储单元 X，或表达式a0+a1a_0+a_1 或a0−a1a_0-a_1 或a0×a1a_0\times a_1。

    然而，对于一个运算式2×3+52\times 3+5，它到底是2×(3+5)2\times(3+5) 构造得来，还是(2×3)+5(2\times 3)+5 构造得来并不知道。其实构造规则只给出了构造新算术表达式的抽象语法，而要保证算术表达式是无歧义的话，就必须加上括号。

  • 抽象语法给出的是语言的分析树，而具体语法正是通过括号和运算符的优先级来保证进行唯一正确的语法分析。然而我们关注的是程序设计语言的含义而不是如何描述它们，所以抽象语法已经足够。

  • IMP 的完整构造规则如下：

    Aexp:a::=n∣X∣a0+a1∣a0−a0∣a0×a1Bexp:b::=true∣false∣a0=a1∣a0≤a1∣¬b∣b0∧b1∣b0∨b1Com:c::=skip∣X:=a∣c0;c1∣if  b  then  c0  else  c1∣while  b  do  cAexp:a::=n|X|a_0+a_1|a_0-a_0|a_0\times a_1\\ Bexp:b::=true|false|a_0=a_1|a_0\leq a_1|\neg b|b_0\wedge b_1|b_0\vee b_1\\ Com:c::=skip|X:=a|c_0;c_1|if\; b\;then\;c_0\;else\;c_1|while\;b\;do\;c

    （其实我觉得这里蛮好理解的，都揭示了不同集合的元变量和元变量组合起来的基本形式）

    上述规则是对 IMP 语法规则的归纳定义，由此得到的集合是对构造规则封闭的最小集合，

  • 当相同集合的两个元素e0,e1e_0,e_1 是由抽象语法用完全相同的方法构造出来时，它们具有相同的分析树结构，此时表达为e0≡e1e_0\equiv e_1。注意3+5≢5+33+5\not \equiv 5+3 因为分析树左右子树换了不相同。

  • 我们首先定义程序运行的状态，然后定义算术表达式和布尔表达式的求值，最后定义命令的执行。

# 算术表达式的求值

  • 状态集合Σ\Sigma 由存储单元到数集的函数σ:Loc→N\sigma:Loc\rightarrow N 组成。于是σ(X)\sigma(X) 是状态σ\sigma 下存储单元 X 的值或内容。下面讨论在状态σ∈Σ\sigma\in\Sigma 下算术表达式aa 的求值过程。

  • 用序偶（有序对）⟨a,σ⟩\lang a,\sigma\rang 来表示在状态σ\sigma 下表达式aa 等待求值。并把这个序偶与数集间的求值关系定义为：

    ⟨a,σ⟩→n\lang a,\sigma\rang\rightarrow n

    它表示在状态σ\sigma 下表达式aa 的求值结果为nn。而序偶⟨a,σ⟩\lang a,\sigma\rang 为算术表达式的格局。

  • 考察算术表达式a0+a1a_0+a_1 的求值过程，其顺序为：

    • 求值a0a_0 得到结果n0n_0
    • 求值a1a_1 得到结果n1n_1
    • 将n0n_0 与n1n_1 相加得到a0+a1a_0+a_1 的求值结果。

    整个过程通过分别求值加式和被加式然后相加得到求值结果，这种规范被称为语法制导下的规范。

语法制导下算术表达式的求值关系按以下规则指定：

# 整数求值

⟨n,σ⟩→n\lang n,\sigma\rang\rightarrow n

# 存储单元求值

⟨X,σ⟩→σ(X)\lang X,\sigma\rang\rightarrow\sigma(X)

  • 对存储单元求值就是取其内容

# 加法求值

⟨a0,σ⟩→n0⟨a1,σ⟩→n1⟨a0+a1,σ⟩→n,n=n0+n1\frac{\lang a_0,\sigma\rang\rightarrow n_0\quad\lang a_1,\sigma\rang\rightarrow n_1}{\lang a_0+a_1,\sigma\rang\rightarrow n},n=n_0+n_1

  • 读作 “如果⟨a0,σ⟩→n0\lang a_0,\sigma\rang\rightarrow n_0 并且⟨a1,σ⟩→n1\lang a_1,\sigma\rang\rightarrow n_1，那么⟨a0+a1,σ⟩→n\lang a_0+a_1,\sigma\rang\rightarrow n，其中n=n0+n1n=n_0+n_1”。
  • 每条规则包含一个前提和一个结论，前提通常写在上方，结论写在下方。由前提推出结论称为规则的一个应用。有时规则没有前提时也有可能在上面加个横线：⟨n,σ⟩→n‾\overline{\lang n,\sigma\rang\rightarrow n}。

# 减法求值

⟨a0,σ⟩→n0⟨a1,σ⟩→n1⟨a0−a1,σ⟩→n,n=n0−n1\frac{\lang a_0,\sigma\rang\rightarrow n_0\quad\lang a_1,\sigma\rang\rightarrow n_1}{\lang a_0-a_1,\sigma\rang\rightarrow n},n=n_0-n_1

# 乘积求值

⟨a0,σ⟩→n0⟨a1,σ⟩→n1⟨a0×a1,σ⟩→n,n=n0×n1\frac{\lang a_0,\sigma\rang\rightarrow n_0\quad\lang a_1,\sigma\rang\rightarrow n_1}{\lang a_0\times a_1,\sigma\rang\rightarrow n},n=n_0\times n_1

  • 特别地，前提为空的规则称为公理。给定任何一个算术表达式aa，状态σ\sigma 和整数nn，如果从公理开始，根据一组规则可以推出⟨a,σ⟩→n\lang a,\sigma\rang\rightarrow n 则称aa 在状态σ\sigma 下求值得到nn。而基本运算符号加减乘的运算规则不做详细讨论。

  • 将求值规则中的元变量用特定的元素代替，就得到了一个规则实例。例如一个乘法的规则实例：

    ⟨2,σ0⟩→2⟨3,σ0⟩→3⟨2×3,σ0⟩→6\frac{\lang 2,\sigma_0\rang\rightarrow 2\quad\lang 3,\sigma_0\rang\rightarrow 3}{\lang 2\times 3,\sigma_0\rang\rightarrow 6}

  • 考虑状态σ0\sigma_0 下的表达式a≡(Iint+5)+(7+9)a\equiv(Iint+5)+(7+9)，InitInit 表示状态σ0\sigma_0 下σ0(Init)=0\sigma_0(Init)=0 的存储单元。则有：

    ⟨Init,σ0⟩→0‾⟨5,σ0⟩→5‾⟨(Init+5),σ0⟩→5⟨7,σ0⟩→7‾⟨9,σ0⟩→9‾⟨(7+9),σ0⟩→16⟨(Iinit+5)+(7+9),σ0⟩→21\frac{\frac{\overline{\lang Init,\sigma_0\rang\rightarrow 0}\quad\overline{\lang 5,\sigma_0\rang\rightarrow 5}}{\lang(Init+5),\sigma_0\rang\rightarrow 5}\quad\frac{\overline{\lang 7,\sigma_0\rang\rightarrow 7}\quad\overline{\lang 9,\sigma_0\rang\rightarrow 9}}{\lang(7+9),\sigma_0\rang\rightarrow 16}}{\lang(Iinit+5)+(7+9),\sigma_0\rang\rightarrow 21}

    这就是一棵求值树，也称推导树（简称推导）。推导树由规则的实例构成，每个规则实例的前提正好是上一层实例的结论，公理位于最顶层。最底层的实例的结论为整个推导的结论。如果某个推导存在结论，则说该结论是从规则可精确推导的。

  • 在这种情况下，规则提供了基于查找推导树来计算算术表达式求值的一个算法。此时我们说这组规则（整数求值、存储单元求值、加法求值、减法求值、乘积求值）给出了表达式的操作语义。因为规则是以语法制导的方式给出的，所以称为结构化操作语义；同时，因为它的推导方式类似于自然推理，所以又称为自然语义。（现在我理解无能，书上说后续会给一些具体的例子说明）

  • 定义

    a0∼a1iff∀n∈N,σ∈Σ,⟨a0,σ⟩→n⇔⟨a1,σ⟩→na_0\sim a_1\quad iff\quad \forall n\in N,\sigma\in \Sigma, \lang a_0,\sigma\rang\rightarrow n\Leftrightarrow \lang a_1,\sigma\rang\rightarrow n

    是一个自然的算术表达式求值相等的等价关系。

# 布尔表达式求值

⟨true,σ⟩→true⟨false,σ⟩→false⟨a0,σ⟩→n⟨a1,σ⟩→m⟨a0=a1,σ⟩→true,if  n=m⟨a0,σ⟩→n⟨a1,σ⟩→m⟨a0=a1,σ⟩→false,if  n≠m⟨a0,σ⟩→n⟨a1,σ⟩→m⟨a0≤a1,σ⟩→true,if  n≤m⟨a0,σ⟩→n⟨a1,σ⟩→m⟨a0≤a1,σ⟩→false,if  n>m⟨b,σ⟩→true⟨¬b,σ⟩→false⟨b,σ⟩→false⟨¬b,σ⟩→true⟨b0,σ⟩→t0⟨b1,σ⟩→t1⟨b0∨b1,σ⟩→t,t≡{truet0≡true&t1≡truefalseelse⟨b0,σ⟩→t0⟨b1,σ⟩→t1⟨b0∧b1,σ⟩→t,t≡{truet0≡true∣t1≡truefalseelse\lang true,\sigma\rang\rightarrow true\\ \lang false,\sigma\rang\rightarrow false\\ \frac{\lang a_0,\sigma\rang\rightarrow n\quad\lang a_1,\sigma\rang\rightarrow m}{\lang a_0=a_1,\sigma\rang\rightarrow true},if\;n=m\\ \frac{\lang a_0,\sigma\rang\rightarrow n\quad\lang a_1,\sigma\rang\rightarrow m}{\lang a_0=a_1,\sigma\rang\rightarrow false},if\;n\neq m\\ \frac{\lang a_0,\sigma\rang\rightarrow n\quad\lang a_1,\sigma\rang\rightarrow m}{\lang a_0\leq a_1,\sigma\rang\rightarrow true},if\;n\leq m\\ \frac{\lang a_0,\sigma\rang\rightarrow n\quad\lang a_1,\sigma\rang\rightarrow m}{\lang a_0\leq a_1,\sigma\rang\rightarrow false},if\;n>m\\ \frac{\lang b,\sigma\rang\rightarrow true}{\lang\neg b,\sigma\rang\rightarrow false}\\ \frac{\lang b,\sigma\rang\rightarrow false}{\lang\neg b,\sigma\rang\rightarrow true}\\ \frac{\lang b_0,\sigma\rang\rightarrow t_0\quad\lang b_1,\sigma\rang\rightarrow t_1}{\lang b_0\vee b_1,\sigma\rang\rightarrow t},t\equiv\begin{cases}true & t_0\equiv true\& t_1\equiv true\\false&else\end{cases}\\ \frac{\lang b_0,\sigma\rang\rightarrow t_0\quad\lang b_1,\sigma\rang\rightarrow t_1}{\lang b_0\wedge b_1,\sigma\rang\rightarrow t},t\equiv\begin{cases}true & t_0\equiv true| t_1\equiv true\\false&else\end{cases}

b0∼b1iff∀t∈T,σ∈Σ,⟨b0,σ⟩→t⇔⟨b1,σ⟩→tb_0\sim b_1\quad iff\quad \forall t\in T,\sigma\in \Sigma,\lang b_0,\sigma\rang\rightarrow t\Leftrightarrow \lang b_1,\sigma\rang\rightarrow t

  • 然而上述规则确定的布尔表达式求值方法效率并不高。更好的策略为最左顺序计算，即：

    ⟨b0,σ⟩→false⟨b0∧b1,σ⟩→false⟨b0,σ⟩→true⟨b1,σ⟩→false⟨b0∧b1,σ⟩→false⟨b0,σ⟩→true⟨b1,σ⟩→true⟨b0∧b1,σ⟩→true\frac{\lang b_0,\sigma\rang\rightarrow false}{\lang b_0\wedge b_1,\sigma\rang\rightarrow false}\\ \frac{\lang b_0,\sigma\rang\rightarrow true\quad\lang b_1,\sigma\rang\rightarrow false}{\lang b_0\wedge b_1,\sigma\rang\rightarrow false}\\ \frac{\lang b_0,\sigma\rang\rightarrow true\quad\lang b_1,\sigma\rang\rightarrow true}{\lang b_0\wedge b_1,\sigma\rang\rightarrow true}\\

    同样，或的时候就是有一个为 true 就已经可以得出 true 了。

# 命令的执行

  • 表达式的作用是求得某一状态下的值，而程序和命令的作用则是通过执行，来改变状态。

    当我们运行一个 IMP 程序时，假定初始状态下所有的存储单元都已置 0，即初状态σ0\sigma_0 满足∀X,σ0(X)=0\forall X,\sigma_0(X)=0。

    程序在运行过程中可能终止于某一状态，也可能会发散而达不到任何状态，譬如c≡while  true  do  skipc\equiv while\;true\;do\;skip 就不存在终止状态。

  • 用序偶⟨c,σ⟩\lang c,\sigma\rang 表示命令的格局，关系：⟨c,σ⟩→σ′\lang c,\sigma\rang\rightarrow \sigma' 表示状态σ\sigma 下执行命令 c 后终止于终态σ′\sigma'。

  • 令σ\sigma 为某状态，σ[m/X]\sigma[m/X] 表示状态σ\sigma 下用 m 替换 X 中的内容后得到的新状态。这个新状态的含义是：

    σ[m/X](Y)={mY=Xσ(Y)Y≠X\sigma[m/X](Y)=\begin{cases}m&Y=X\\\sigma(Y)&Y\neq X\end{cases}

    例如⟨X:=5,σ⟩→σ′=σ[5/X]\lang X:=5,\sigma\rang\rightarrow \sigma'=\sigma[5/X]

原子命令：

⟨skip,σ⟩→σ⟨a,σ⟩→m⟨X:=a,σ⟩→σ[m/X]\lang skip,\sigma\rang\rightarrow\sigma\\ \frac{\lang a,\sigma\rang\rightarrow m}{\lang X:=a,\sigma\rang\rightarrow\sigma[m/X]}

顺序命令：

⟨c0,σ⟩→σ′′⟨c1,σ′′⟩→σ′⟨c0;c1,σ⟩→σ′\frac{\lang c_0,\sigma\rang\rightarrow \sigma''\quad\lang c_1,\sigma''\rang\rightarrow\sigma'}{\lang c_0;c_1,\sigma\rang\rightarrow \sigma'}

条件命令：

⟨b,σ⟩→true⟨c0,σ⟩→σ′⟨if  b  then  c0  else  c1,σ⟩→σ′⟨b,σ⟩→false⟨c1,σ⟩→σ′⟨if  b  then  c0  else  c1,σ⟩→σ′\frac{\lang b,\sigma\rang\rightarrow true\quad\lang c_0,\sigma\rang\rightarrow\sigma'}{\lang if\;b\;then\;c_0\;else\;c_1,\sigma\rang\rightarrow \sigma'}\\ \frac{\lang b,\sigma\rang\rightarrow false\quad\lang c_1,\sigma\rang\rightarrow\sigma'}{\lang if\;b\;then\;c_0\;else\;c_1,\sigma\rang\rightarrow \sigma'}\\

while 循环命令：

⟨b,σ⟩→false⟨while  b  do  c,σ⟩→σ⟨b,σ⟩→true⟨c,σ⟩→σ′′⟨while  b  do  c,σ′′⟩→σ′⟨while  b  do  c,σ⟩→σ′\frac{\lang b,\sigma\rang\rightarrow false}{\lang while\;b\;do\;c,\sigma\rang\rightarrow\sigma}\\ \frac{\lang b,\sigma\rang\rightarrow true\quad\lang c,\sigma\rang\rightarrow\sigma''\quad\lang while\;b\;do\;c,\sigma''\rang\rightarrow\sigma'}{\lang while\;b\;do\;c,\sigma\rang\rightarrow\sigma'}

  • 其实是个递归定义规则。

命令间的等价关系：

c0∼c1iff∀σ,σ′∈Σ,⟨c0,σ⟩→σ′⇔⟨c1,σ⟩→σ′c_0\sim c_1\quad iff\quad\forall \sigma,\sigma'\in\Sigma,\lang c_0,\sigma\rang\rightarrow\sigma'\Leftrightarrow\lang c_1,\sigma\rang\rightarrow\sigma'

# 一个简单的证明

  • 表达式的求值，命令的执行，其实都是一种关系，被称为转换关系（转换系统）。

命题：令w≡while  b  do  cw\equiv while\;b\;do\;c，则w∼if  b  do  c;w  else  skipw\sim if\;b\;do\;c;w\;else\;skip

  • 证明：需要证明对所有的状态σ,σ′\sigma,\sigma'，都有⟨w,σ⟩→σ′iff⟨if  b  then  c;w  else  skip,σ⟩→σ′\lang w,\sigma\rang\rightarrow\sigma'\quad iff\quad\lang if\;b\;then\;c;w\;else\;skip,\sigma\rang\rightarrow\sigma'。

    “⇒\Rightarrow”：因为有⟨w,σ⟩→σ′\lang w,\sigma\rang\rightarrow\sigma'，根据 while 循环命令的规则，必有：

    ⟨b,σ⟩→false⟨w,σ⟩→σ或⟨b,σ⟩→true⟨c,σ⟩→σ′′⟨w,σ′′⟩→σ′⟨w,σ⟩→σ′\frac{\lang b,\sigma\rang\rightarrow false}{\lang w,\sigma\rang\rightarrow\sigma}或 \frac{\lang b,\sigma\rang\rightarrow true\quad\lang c,\sigma\rang\rightarrow \sigma''\quad\lang w,\sigma''\rang\rightarrow\sigma'}{\lang w,\sigma\rang\rightarrow\sigma'}

    ​ 若是左侧情况，则一定有一个推导树结论为⟨b,σ⟩→false\lang b,\sigma\rang\rightarrow false，即有：

    ...⟨b,σ⟩→false⟨w,σ⟩→σ\frac{...}{\frac{\lang b,\sigma\rang\rightarrow false}{\lang w,\sigma\rang\rightarrow\sigma}}

    ​ 既然有了这样一个推导树，则可以依照 while 循环规则构造出推导树：

    ...⟨b,σ⟩→false⟨skip,σ⟩→σ⟨if  b  then  c;w  else  skip,σ⟩→σ\frac{\frac{...}{\lang b,\sigma\rang\rightarrow false}\quad\frac{}{\lang skip,\sigma\rang\rightarrow\sigma}}{\lang if\;b\;then\;c;w\;else\;skip,\sigma\rang\rightarrow\sigma}

    ​ 即得到了想要的结论。如果是右侧情况，则一定分别有推导树：

    ...⟨b,σ⟩→true,...⟨c,σ⟩→σ′′,...⟨w,σ′′⟩→σ′\frac{...}{\lang b,\sigma\rang\rightarrow true},\frac{...}{\lang c,\sigma\rang\rightarrow\sigma''},\frac{...}{\lang w,\sigma''\rang\rightarrow \sigma'}

    ​ 则可以依照 while 循环规则，顺序命令规则，条件命令规则构造出推导树：

    ...⟨b,σ⟩→true...⟨c,σ⟩→σ′′...⟨w,σ′′⟩→σ′⟨c;w,σ⟩→σ′⟨if  b  then  c:w  else  skip,σ⟩→σ′\frac{\frac{...}{\lang b,\sigma\rang\rightarrow true}\quad\frac{\frac{...}{\lang c,\sigma\rang\rightarrow\sigma''}\quad\frac{...}{\lang w,\sigma''\rang\rightarrow\sigma'}}{\lang c;w,\sigma\rang\rightarrow\sigma'}}{\lang if\;b\;then\;c:w\;else\;skip,\sigma\rang\rightarrow\sigma'}

    ”⇐\Leftarrow“：因为有⟨if  b  then  c;w  else  skip,σ⟩→σ′\lang if\;b\;then\;c;w\;else\;skip,\sigma\rang\rightarrow\sigma'，所以根据条件命令规则，必有推导：

    ...⟨b,σ⟩→false⟨skip,σ⟩→σ⟨if  b  then  c;w  else  skip,σ⟩→σ或...⟨b,σ⟩→true...⟨c,σ⟩→σ′′...⟨w,σ′′⟩→σ′⟨c;w,σ⟩→σ′⟨if  b  then  c;w  else  skip,σ⟩→σ′\frac{\frac{...}{\lang b,\sigma\rang\rightarrow false}\quad\frac{}{\lang skip,\sigma\rang\rightarrow\sigma}}{\lang if\;b\;then\;c;w\;else\;skip,\sigma\rang\rightarrow\sigma}或 \frac{\frac{...}{\lang b,\sigma\rang\rightarrow true}\quad\frac{\frac{...}{\lang c,\sigma\rang\rightarrow\sigma''}\quad\frac{...}{\lang w,\sigma''\rang\rightarrow\sigma'}}{\lang c;w,\sigma\rang\rightarrow\sigma'}}{\lang if\;b\;then\;c;w\;else\;skip,\sigma\rang\rightarrow\sigma'}

    ​ 先考虑右侧情况，根据 while 循环命令规则，我们可以构造推导：

    ...⟨b,σ⟩→true...⟨c,σ⟩→σ′′...⟨w,σ′′⟩→σ′⟨w,σ⟩→σ′\frac{\frac{...}{\lang b,\sigma\rang\rightarrow true}\quad\frac{...}{\lang c,\sigma\rang\rightarrow\sigma''}\quad\frac{...}{\lang w,\sigma''\rang\rightarrow\sigma'}}{\lang w,\sigma\rang\rightarrow\sigma'}

    ​ 如果是左侧情况，根据 while 循环命令规则，则直接可以构造推导：

    ⟨b,σ⟩→false⟨w,σ⟩→σ\frac{\lang b,\sigma\rang\rightarrow false}{\lang w,\sigma\rang\rightarrow\sigma}

    因此，得证w∼if  b  then  c;w  else  skipw\sim if\;b\;then\;c;w\;else\;skip。

  • 其实这个简单的证明表示了：在规则未被实例化的情况下，要证明操作语义的等价，需要考虑所有不同形式可能的推导树。

# 另一种语义

  • 其实我们也可以定义格局之间的求值关系：

    ⟨a,σ⟩→1⟨a′,σ′⟩\lang a,\sigma\rang\rightarrow_1\lang a',\sigma'\rang

    表示状态σ\sigma 下，表达式aa 经过了 1 个步骤即得到了状态σ′\sigma' 状态下的a′a'。

  • 对应规则：

    ⟨a0,σ⟩→1⟨a0′,σ⟩⟨a0+a1,σ⟩→1⟨a0′+a1,σ⟩⟨a1,σ⟩→1⟨a1′,σ⟩⟨n+a1,σ⟩→1⟨n+a1′,σ⟩⟨n+m,σ⟩→1⟨p,σ⟩,p=n+m\frac{\lang a_0,\sigma\rang\rightarrow_1\lang a_0',\sigma\rang}{\lang a_0+a_1,\sigma\rang\rightarrow_1\lang a_0'+a_1,\sigma\rang}\\ \frac{\lang a_1,\sigma\rang\rightarrow_1\lang a_1',\sigma\rang}{\lang n+a_1,\sigma\rang\rightarrow_1\lang n+a_1',\sigma\rang}\\ \lang n+m,\sigma\rang\rightarrow_1\lang p,\sigma\rang,p=n+m

    根据书上说，这实际上表示了把之前求值规则拆开成一步一步了 (a0+a1→a0′+a1→a0′+a1′a_0+a_1\rightarrow a_0'+a_1\rightarrow a_0'+a_1') 但我也不知道为啥要这么干。

  • 命令格局间的关系：

    实际上，⟨c,σ⟩→σ′\lang c,\sigma\rang\rightarrow\sigma' 定义了在特定状态下，命令的完全执行。同样我们可以给出执行命令的每一个步骤，譬如

    ⟨c0;c1,σ⟩→1⟨c1,σ′′⟩⟨c1,σ′′⟩→1σ′⟨c0;c1,σ⟩→σ′\frac{\lang c_0;c_1,\sigma\rang\rightarrow_1\lang c_1,\sigma''\rang\quad\lang c_1,\sigma''\rang\rightarrow_1\sigma'}{\lang c_0;c_1,\sigma\rang\rightarrow\sigma'}

    ⟨X:=5;Y:=1,σ⟩→1⟨Y:=1,σ[5/X]⟩→1σ[5/X][1/Y]\lang X:=5;Y:=1,\sigma\rang\rightarrow_1\lang Y:=1,\sigma[5/X]\rang\rightarrow_1\sigma[5/X][1/Y]

  • 有些”1 步 “是显然的，而有些又是不确定的。譬如，⟨b,σ⟩→1⟨true,σ⟩\lang b,\sigma\rang\rightarrow_1\lang true,\sigma\rang 是显然的，但是

    ⟨if  b  then  c0  else  c1,σ⟩→1⟨c0,σ⟩⟨if  b  then  c0  else  c1,σ⟩→1⟨if  true  then  c0  else  c1,σ⟩\lang if\;b\;then\;c_0\;else\;c_1,\sigma\rang\rightarrow_1\lang c_0,\sigma\rang\\ \lang if\;b\;then\;c_0\;else\;c_1,\sigma\rang\rightarrow_1\lang if\;true\;then\;c_0\;else\;c_1,\sigma\rang

    选择哪一个当作”1 步 “呢？其实对于 IMP 语言来说这不是非常重要，但是对于并行语言，选择不同的步骤可能会影响执行的终态。

# 归纳原理

# 数学归纳法

  • 数学归纳法：(P(0)&(∀m∈ω,P(m)⇒P(m+1)))⇒∀n∈ω,P(n)(P(0)\&(\forall m\in\omega,P(m)\Rightarrow P(m+1)))\Rightarrow\forall n\in\omega,P(n)

  • 串值归纳法：(∀m∈ω,(∀k<m,Q(k))⇒Q(m))⇒∀n∈ω,P(n)(\forall m\in\omega,(\forall k<m,Q(k))\Rightarrow Q(m))\Rightarrow\forall n\in\omega,P(n)

# 结构归纳法

  • 证明：

    ⟨a,σ⟩→m&⟨a,σ⟩→m′⇒m=m′\lang a,\sigma\rang\rightarrow m\&\lang a,\sigma\rang\rightarrow m'\Rightarrow m=m'

    也就是这个求值是一个函数，而不只是关系。这看起来很明显。

    结构归纳法：令P(a)P(a) 是算术表达式aa 的一个性质，要证明对所有算术表达式均有此性质，只需证明：

    • 对所有整数 m，P(m)P(m) 为真。
    • 对所有存储单元 X，P(σ(X))P(\sigma(X)) 为真。（如果有状态作用的话）
    • 对所有的算术表达式a0,a1a_0,a_1，有P(a0)&P(a1)⇒P(a0+a1)P(a_0)\&P(a_1)\Rightarrow P(a_0+a_1)。
    • 对所有的算术表达式a0,a1a_0,a_1，有P(a0)&P(a1)⇒P(a0−a1)P(a_0)\&P(a_1)\Rightarrow P(a_0-a_1)。
    • 对所有的算术表达式a0,a1a_0,a_1，有P(a0)&P(a1)⇒P(a0×a1)P(a_0)\&P(a_1)\Rightarrow P(a_0\times a_1)。

    如果写作逻辑符号：

    (∀m∈N,P(m))&(∀X∈Loc,P(X))&(∀a0,a1∈Aexp,P(a0)&P(a1)⇒P(a0+a1))&(∀a0,a1∈Aexp,P(a0)&P(a1)⇒P(a0−a1))&(∀a0,a1∈Aexp,P(a0)&P(a1)⇒P(a0×a1))&⇒∀a∈Aexp,P(a)(\forall m\in N,P(m))\&\\ (\forall X\in Loc,P(X))\&\\ (\forall a_0,a_1\in Aexp,P(a_0)\&P(a_1)\Rightarrow P(a_0+a_1))\&\\ (\forall a_0,a_1\in Aexp,P(a_0)\&P(a_1)\Rightarrow P(a_0-a_1))\&\\ (\forall a_0,a_1\in Aexp,P(a_0)\&P(a_1)\Rightarrow P(a_0\times a_1))\&\\ \Rightarrow \forall a\in Aexp,P(a)

    利用结构归纳法证明该命题。

    P(a)=∀σ,m,m′,(⟨a,σ⟩→m&⟨a,σ⟩→m′⇒m=m′)P(a)=\forall\sigma,m,m',(\lang a,\sigma\rang\rightarrow m\&\lang a,\sigma\rang\rightarrow m'\Rightarrow m=m')

    • a≡na\equiv n，因为整数求值规则，实际上有⟨a,σ⟩→m=a,⟨a,σ⟩→m′=a\lang a,\sigma\rang\rightarrow m=a,\lang a,\sigma\rang\rightarrow m'=a 所以m=m′m=m'。

    • a≡Xa\equiv X，因为存储单元求值规则，实际上有⟨a,σ⟩→m=σ(a),⟨a,σ⟩→m′=σ(a)\lang a,\sigma\rang\rightarrow m=\sigma(a),\lang a,\sigma\rang\rightarrow m'=\sigma(a)，而同一个存储单元存储的内容是相同的，所以有m=m′m=m'

    • a≡a0+a1a\equiv a_0+a_1，⟨a0+a1,σ⟩→m&⟨a0+a1,σ⟩→m′\lang a_0+a_1,\sigma\rang\rightarrow m\&\lang a_0+a_1,\sigma\rang\rightarrow m'，由加法求值规则，必存在

      ⟨a0,σ⟩→m0,⟨a1,σ⟩→m1,m0+m1=m⟨a0,σ⟩→m0′,⟨a1,σ⟩→m1′,m0′+m1′=m′\lang a_0,\sigma\rang\rightarrow m_0,\lang a_1,\sigma\rang\rightarrow m_1,m_0+m_1=m\\ \lang a_0,\sigma\rang\rightarrow m_0',\lang a_1,\sigma\rang\rightarrow m_1',m_0'+m_1'=m'\\

      然后根据归纳假设P(a0)&P(a1)P(a_0)\& P(a_1)，有m0=m0′,m1=m1′m_0=m_0',m_1=m_1'，因此有m=m′m=m'。

    • a≡a0−a1,a≡a0×a1a\equiv a_0-a_1,a\equiv a_0\times a_1 和加法情况类似。因此可以得出命题。

# 良基归纳法

  • 定义：设≺\prec 是集合 A 上的二元关系，如果不存在由 A 中元素构成的无穷下降链...≺ai≺...≺a≺a0...\prec a_i\prec ...\prec a\prec a_0 则称≺\prec 为良基关系。

    若a≺ba\prec b，则称 a 为 b 的前趋。显然，良基关系必是非自反的。记⪯\preceq 为≺\prec 的自反闭包。

  • 命题：设≺\prec 是集合 A 上的二元关系，则≺\prec 是良基关系的充要条件是，对 A 的所有非空子集 Q 都含有一个极小元 m：

    m∈Q&∀b≺m,b∉Qm\in Q\&\forall b\prec m,b\notin Q

  • 良基归纳法：

    ∀a∈A,P(a)⇔∀a∈A,([∀b≺a,P(b)]⇒P(a))\forall a\in A,P(a)\Leftrightarrow \forall a\in A,([\forall b\prec a,P(b)]\Rightarrow P(a))

    如果a≺b⇔a=b−1a\prec b\Leftrightarrow a=b-1，则就是数学归纳法，若a≺b⇔a<ba\prec b\Leftrightarrow a<b 则为串值归纳法。

  • 以欧几里得算法为例，我们证明它的终止性。

    Euclid 算法：（IMP 语言）

    Euclid≡while  ¬(M=N)  doif  M≤Nthen  N:=N−Melse  M:=M−NEuclid\equiv while\;\neg(M=N)\;do\\ if\;M\leq N\\ then\;N:=N-M\\ else\;M:=M-N

    其中，N,M 都是存储单元，赋值表示内容的赋值。我们需要证明：

    ∀σ,σ(M)≥1&σ(N)≥1⇒∃σ′,⟨Euclid,σ⟩→σ′\forall\sigma,\sigma(M)\geq 1\&\sigma(N)\geq 1\Rightarrow\exists\sigma',\lang Euclid,\sigma\rang\rightarrow\sigma'

    设性质 P 为P(σ)⇔∃σ′,⟨Euclid,σ⟩→σ′P(\sigma)\Leftrightarrow \exist\sigma',\lang Euclid,\sigma\rang\rightarrow\sigma'

    记S={σ∈Σ∣σ(M)≥1&σ(N)≥1}S=\{\sigma\in\Sigma|\sigma(M)\geq 1\&\sigma(N)\geq 1\} 是良基集。

    我们证明：∀σ∈S,P(σ)\forall\sigma\in S,P(\sigma)。

    首先定义良基关系：

    σ′≺σ⇔(σ′(M)≤σ(M)&σ′(N)≤σ(N))&(σ(M)≠σ′(M)∨σ(N)≠σ′(N))\sigma'\prec\sigma\Leftrightarrow(\sigma'(M)\leq\sigma(M)\&\sigma'(N)\leq\sigma(N))\&(\sigma(M)\neq\sigma'(M)\vee\sigma(N)\neq\sigma'(N))

    因为 M,N 的内容始终为正且不会一直减少，所以其为良基关系。

    归纳假设：对σ∈S\sigma\in S，设∀σ′≺σ,P(σ′)\forall\sigma'\prec\sigma,P(\sigma')。记σ(M)=m,σ(N)=n\sigma(M)=m,\sigma(N)=n。

    • 若m=nm=n，有⟨¬(M=N),σ⟩→false\lang\neg(M=N),\sigma\rang\rightarrow false，根据 while 规则，可以构造一个推导：

      ...⟨¬(M=N),σ⟩→false⟨Euclid,σ⟩→σ\frac{\frac{...}{\lang\neg(M=N),\sigma\rang\rightarrow false}}{\lang Euclid,\sigma\rang\rightarrow\sigma}

      即得到P(σ)P(\sigma)。注：其实从⟨M,σ⟩→m,⟨N,σ⟩→n\lang M,\sigma\rang\rightarrow m,\lang N,\sigma\rang\rightarrow n 可以构造一个推导树推出⟨¬(M=N),σ⟩→false\lang\neg(M=N),\sigma\rang\rightarrow false。也就是省略的…。

    • 若m≠nm\neq n，则有⟨¬(M=N),σ⟩→true\lang\neg(M=N),\sigma\rang\rightarrow true，根据条件命令规则，有：（单条条件命令一定可终止）

      ⟨if  M≤N  then  N:=N−M  else  M:=M−N,σ⟩→σ′′={σ[(n−m)/N]m<nσ[(m−n)/M]n<m\lang if\;M\leq N\;then\;N:=N-M\;else\;M:=M-N,\sigma\rang\rightarrow\sigma''=\begin{cases}\sigma[(n-m)/N]&m<n\\\sigma[(m-n)/M]&n<m\end{cases}

      显然，σ[(n−m)/N]≺σ,σ[(m−n)/M]≺σ\sigma[(n-m)/N]\prec \sigma,\sigma[(m-n)/M]\prec\sigma，即σ′′≺σ\sigma''\prec\sigma，由归纳假设，有P(σ′′)P(\sigma'')，即

      ∃σ′,⟨Euclid,σ′′⟩→σ′\exists\sigma',\lang Euclid,\sigma''\rang\rightarrow \sigma'

      根据 while 命令规则，可以构造推导：

      ...⟨¬(M=N),σ⟩→true...⟨if  M≤N  then  N:=N−M  else  M:=M−N,σ⟩→σ′′...⟨Euclid,σ′′⟩→σ′⟨Euclid,σ⟩→σ′\frac{\frac{...}{\lang\neg(M=N),\sigma\rang\rightarrow true}\quad\frac{...}{\lang if\;M\leq N\;then\;N:=N-M\;else\;M:=M-N,\sigma\rang\rightarrow\sigma''}\quad\frac{...}{\lang Euclid,\sigma''\rang\rightarrow\sigma'}}{\lang Euclid,\sigma\rang\rightarrow\sigma'}

    根据良基归纳假设，有∀σ∈S,P(σ)\forall\sigma\in S,P(\sigma)

  • 良基归纳法是证明含有循环和递归的程序终止性的最重要的方法。如果能证明执行过程状态沿着良基关系链下降，则必然终止。

# 对推导树的归纳

  • 一个规则实例的集合 R 由一组序偶 (X/yX/y) 所组成，其中 X 是一个有限集合，y 是一个元素。它表示：

    y‾,X=∅...x1,...,...xny,X={x1,...,xn}\overline{y},X=\emptyset\quad\frac{\frac{...}{x_1},...,\frac{...}{x_n}}{y},X=\{x_1,...,x_n\}

    用d⊩Ryd\Vdash_R y 表示 d 是结论为 y 的一个推导树，R 是一组规则实例的集合，于是有：

    (∅/y)⊩Ryif  (∅/y)∈R({d1,...,dn}/y)⊩Ryif({x1,...,xn}/y)∈R&d1⊩Rx1&...&dn⊩xn(\emptyset/y)\Vdash_R y\quad if\;(\emptyset/y)\in R\\ (\{d_1,...,d_n\}/y)\Vdash_R y\quad if(\{x_1,...,x_n\}/y)\in R\& d_1\Vdash_R x_1\&...\& d_n\Vdash x_n

    这里其实根据我的理解，d 表示的是推导树，x，y 表示的都是单条结论。而规则实例一定是形如xy\frac{x}{y} 的，而不会出现层数大于 2 的树形结构。因此注意区分规则实例和推导树的区别。

    如果存在 y 的 R 推导，即对于某个推导树dd，有d⊩Ryd\Vdash_R y，则称 y 是由 R 推导出来的（y 由一组规则实例推导出来）。在了解了规则后也可以简写为d⊩yd\Vdash y 或⊩y\Vdash y

  • 令d,d′d,d' 都是推导树，称d′d' 是dd 的直接子推导（记为d′≺1dd'\prec_1 d）当且仅当 d 形为D/yD/y，且d′∈Dd'\in D。用≺\prec 表示≺1\prec_1 的传递闭包，则称d′d' 是dd 的真子推导当且仅当d′≺dd'\prec d。

    注意这里，实际上直接子推导就是推导树 d 的结论上一层的某个前提的推导树。而真子推导的话就不限于上一层了，可以是上几层的子树。

    T=EFDGHAT=\frac{\frac{\frac{E}{F}}{D}\quad\frac{G}{H}}{A}

    譬如GH,EFD\frac{G}{H},\frac{\frac{E}{F}}{D} 都是 T 的直接子推导，EF\frac{E}{F} 是EFD\frac{\frac{E}{F}}{D} 的直接子推导，是 T 的真子推导。

  • 定理：∀σ,σ1,(⟨c,σ0⟩→σ&⟨c,σ0⟩→σ1)⇒σ=σ1\forall\sigma,\sigma_1,(\lang c,\sigma_0\rang\rightarrow\sigma\&\lang c,\sigma_0\rang\rightarrow\sigma_1)\Rightarrow\sigma=\sigma_1。

    证明：先定义对推导树 d 的性质 P：

    P(d)⇔∀c∈Com,σ0,σ,σ1∈Σ,(d⊩⟨c,σ0⟩→σ&⟨c,σ0⟩→σ1)⇒σ=σ1P(d)\Leftrightarrow\forall c\in Com,\sigma_0,\sigma,\sigma_1\in\Sigma,(d\Vdash\lang c,\sigma_0\rang\rightarrow\sigma\&\lang c,\sigma_0\rang\rightarrow\sigma_1)\Rightarrow\sigma=\sigma_1

    我们需要证明（推导出⟨c,σ0⟩→σ&⟨c,σ0⟩→σ1\lang c,\sigma_0\rang\rightarrow\sigma\&\lang c,\sigma_0\rang\rightarrow\sigma_1 的）推导树 d 满足P(d)P(d)。

    根据良基归纳法，只需要证明 d 的所有真子推导d′d' 都满足P(d′)P(d') 能推出 d 也满足P(d)P(d)，即：

    (∀d′≺d,P(d′))⇒P(d)(\forall d'\prec d,P(d'))\Rightarrow P(d)

    因为 d 推导出了⟨c,σ0⟩→σ&⟨c,σ0⟩→σ1\lang c,\sigma_0\rang\rightarrow\sigma\&\lang c,\sigma_0\rang\rightarrow\sigma_1，所以一定存在两个推导树d1,d2d_1,d_2 满足d1⊩⟨c,σ0⟩→σd_1\Vdash\lang c,\sigma_0\rang\rightarrow\sigma，d2⊩⟨c,σ0⟩→σ1d_2\Vdash\lang c,\sigma_0\rang\rightarrow\sigma_1。

    • 若c≡skipc\equiv skip，则d1=d2=⟨skip,σ0⟩→σ0‾d_1=d_2=\overline{\lang skip,\sigma_0\rang\rightarrow\sigma_0}。

    • 若c≡X:=ac\equiv X:=a，此时两个推导树形如：

      d1=...⟨a,σ0⟩→m⟨X:=a,σ0⟩→σ0[m/X]d2=...⟨a,σ0⟩→m1⟨X:=a,σ0⟩→σ0[m1/X]d_1=\frac{\frac{...}{\lang a,\sigma_0\rang\rightarrow m}}{\lang X:=a,\sigma_0\rang\rightarrow\sigma_0[m/X]}\quad d_2=\frac{\frac{...}{\lang a,\sigma_0\rang\rightarrow m_1}}{\lang X:=a,\sigma_0\rang\rightarrow\sigma_0[m_1/X]}

      且σ=σ0[m/X],σ1=σ0[m1/X]\sigma=\sigma_0[m/X],\sigma_1=\sigma_0[m_1/X]，而根据算术表达式求值的唯一性，有m=m1m=m_1，然后就可以得到

      ∀X,σ(X)=σ1(X)\forall X,\sigma(X)=\sigma_1(X)，即σ=σ1\sigma=\sigma_1。

    • 若c≡c0;c1c\equiv c_0;c_1，此时有

      d1=...⟨c0,σ0⟩→σ′...⟨c1,σ′⟩→σ⟨c0;c1,σ0⟩→σd2=...⟨c0σ0⟩→σ1′...⟨c1,σ1′⟩→σ1⟨c0;c1,σ0⟩→σ1d=d1d2d_1=\frac{\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma'}\quad\frac{...}{\lang c_1,\sigma'\rang\rightarrow\sigma}}{\lang c_0;c_1,\sigma_0\rang\rightarrow\sigma}\quad d_2=\frac{\frac{...}{\lang c_0\sigma_0\rang\rightarrow\sigma_1'}\quad\frac{...}{\lang c_1,\sigma_1'\rang\rightarrow\sigma_1}}{\lang c_0;c_1,\sigma_0\rang\rightarrow\sigma_1}\\ d=d_1\quad d_2

      注意到，实际上，我们已经有了推导树

      ...⟨c0,σ0⟩→σ′...⟨c1,σ′⟩→σ...⟨c0σ0⟩→σ1′...⟨c1,σ1′⟩→σ1\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma'}\quad\frac{...}{\lang c_1,\sigma'\rang\rightarrow\sigma}\quad\frac{...}{\lang c_0\sigma_0\rang\rightarrow\sigma_1'}\quad\frac{...}{\lang c_1,\sigma_1'\rang\rightarrow\sigma_1}

      因此，我们可以构造推导树（这里我理解为两棵树即森林）

      d1′=...⟨c0,σ0⟩→σ′...⟨c0σ0⟩→σ1′d2′=...⟨c1,σ′⟩→σ...⟨c1,σ1′⟩→σ1d_1'=\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma'}\quad\frac{...}{\lang c_0\sigma_0\rang\rightarrow\sigma_1'}\\ d_2'=\frac{...}{\lang c_1,\sigma'\rang\rightarrow\sigma}\quad\frac{...}{\lang c_1,\sigma_1'\rang\rightarrow\sigma_1}

      显然有d1′≺d,d2′≺dd_1'\prec d,d_2'\prec d 且d1′⊩(⟨c0σ0⟩→σ′&⟨c0σ0⟩→σ1′)d_1'\Vdash(\lang c_0\sigma_0\rang\rightarrow\sigma'\&\lang c_0\sigma_0\rang\rightarrow\sigma_1')，d2′⊩(⟨c0σ0⟩→σ&⟨c0σ0⟩→σ1)d_2'\Vdash(\lang c_0\sigma_0\rang\rightarrow\sigma\&\lang c_0\sigma_0\rang\rightarrow\sigma_1)

      结合P(d1′),P(d2′)P(d_1'),P(d_2') 有σ′=σ1′,σ=σ1\sigma'=\sigma_1',\sigma=\sigma_1

    • 若c≡if  b  then  c0  else  c1c\equiv if\;b\;then\;c_0\;else\;c_1，此时有推导树

      d=...⟨b,σ0⟩→true...⟨c0,σ0⟩→σ⟨c,σ0⟩→σ...⟨b,σ0⟩→true...⟨c0,σ0⟩→σ1⟨c,σ0⟩→σ1d=\frac{\frac{...}{\lang b,\sigma_0\rang\rightarrow true}\quad\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma}}{\lang c,\sigma_0\rang\rightarrow\sigma}\quad \frac{\frac{...}{\lang b,\sigma_0\rang\rightarrow true}\quad\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma_1}}{\lang c,\sigma_0\rang\rightarrow\sigma_1}

      则存在子推导树

      d′=...⟨c0,σ0⟩→σ...⟨c0,σ0⟩→σ1≺dd'=\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma}\quad\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma_1}\prec d

      结合P(d′)P(d') 得到σ=σ1\sigma=\sigma_1，而若 b 求值是 false 完全类似，只是把c0c_0 换成c1c_1

    • 若c≡while  b  do  c0c\equiv while\;b\;do\;c_0，此时有推导树：

      d=...⟨b,σ0⟩→true...⟨c0,σ0⟩→σ′...⟨c,σ′⟩→σ⟨c,σ0⟩→σ...⟨b,σ0⟩→true...⟨c0,σ0⟩→σ1′...⟨c,σ1′⟩→σ1⟨c,σ0⟩→σ1d=\frac{\frac{...}{\lang b,\sigma_0\rang\rightarrow true}\quad\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma'}\quad\frac{...}{\lang c,\sigma'\rang\rightarrow\sigma}}{\lang c,\sigma_0\rang\rightarrow\sigma}\quad \frac{\frac{...}{\lang b,\sigma_0\rang\rightarrow true}\quad\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma_1'}\quad\frac{...}{\lang c,\sigma_1'\rang\rightarrow\sigma_1}}{\lang c,\sigma_0\rang\rightarrow\sigma_1}

      显然有子推导

      d1=...⟨c0,σ0⟩→σ′...⟨c0,σ0⟩→σ1′≺dd2=...⟨c0,σ′⟩→σ...⟨c0,σ1′⟩→σ1≺dd_1=\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma'}\quad\frac{...}{\lang c_0,\sigma_0\rang\rightarrow\sigma_1'}\prec d\\ d_2=\frac{...}{\lang c_0,\sigma'\rang\rightarrow\sigma}\quad\frac{...}{\lang c_0,\sigma_1'\rang\rightarrow\sigma_1}\prec d

      结合P(d1),P(d2)P(d_1),P(d_2) 有σ′=σ1′,σ=σ1\sigma'=\sigma_1',\sigma=\sigma_1

      如果 b 求值是 false 更简单

    证明到这里结束证毕了。

  • 写一点我的理解。++ 其实我认为 “真子推导” 本身就是一个良基关系。++ 所以事实上，对推导树的归纳也就是在做：
    • 1、存在推导树 d 推导出了要证命题的前提
    • 2、证明存在 d 的子推导 d‘推导出了类似要证命题前提的不同情况
    • 3、根据归纳假设，得到不同情况下的命题结论
    • 4、通过上一步的结论，再推导出要证命题的结论。

  • 命题：对所有状态σ,σ′\sigma,\sigma'，有⟨while  true  do  skip,σ⟩↛σ′\lang while\;true\;do\;skip,\sigma\rang\not\rightarrow \sigma'。

    证明：反设存在一个推导 d，推出⟨while  true  do  skip,σ⟩→σ′\lang while\;true\;do\;skip,\sigma\rang\rightarrow \sigma'。d 只有一种形态：

    d=⟨true,σ⟩→true‾⟨skip,σ⟩→σ‾...⟨while  true  do  skip,σ⟩→σ′⟨while  true  do  skip,σ⟩→σ′d=\frac{\overline{\lang true,\sigma\rang\rightarrow true}\quad\overline{\lang skip,\sigma\rang\rightarrow\sigma}\quad\frac{...}{\lang while\;true\;do\;skip,\sigma\rang\rightarrow\sigma'}}{\lang while\;true\;do\;skip,\sigma\rang\rightarrow\sigma'}

    然后会发现子推导可以无限嵌套下去，这与子推导是良基关系矛盾。

# 归纳定义

# 规则归纳法

  • 给定一组规则实例 R，把 R 定义的集合记为IRI_R，表示由 R 可以推导出的结论：

    IR={x∣⊩Rx}I_R=\{x|\Vdash_R x\}

  • 规则归纳法：

    设IRI_R 是规则实例集合RR 定义的集合，P 是某个性质，则∀x∈IR,P(x)\forall x\in I_R,P(x) 当且仅当对 R 中所有的规则实例X/yX/y，有

    (∀x∈X,P(x))⇒P(y)(\forall x\in X,P(x))\Rightarrow P(y)

    其中X⊆IRX\subseteq I_R。

    换句话描述下，对规则实例集合RR，∀y∈IR,P(y)\forall y\in I_R,P(y) 当且仅当对所有公理实例x‾\overline{x} 满足P(x)P(x) 且对所有规则实例x1,..,xnx\frac{x_1,..,x_n}{x} 满足

    [∀i,xi∈IR&P(xi)]⇒P(x)[\forall i,x_i\in I_R\&P(x_i)]\Rightarrow P(x)

  • 我们称集合 Q 对规则实例集合 R 是封闭的当且仅当

    ∀X/y∈R,X⊆Q⇒y∈Q\forall X/y\in R,X\subseteq Q\Rightarrow y\in Q

    显然IRI_R 对 R 是封闭的，而且有对于任意对 R 封闭的集合 Q，都有IR⊆QI_R\subseteq Q。

    于是，如果我们想证明IRI_R 中所有的元素都满足性质PP，我们可以构造集合:

    Q={x∈IR∣P(x)}Q=\{x\in I_R|P(x)\}

    然后证明 Q 对 R 封闭，即对所有规则实例（X/yX/y）有：

    (∀x∈X,x∈Q)⇒P(y)(∀x∈X,x∈IR&P(x))⇒P(y)(\forall x\in X,x\in Q)\Rightarrow P(y)\\ (\forall x\in X,x\in I_R\& P(x))\Rightarrow P(y)

    实际上这就是规则归纳法。

  • 以此，我们可以对之前的操作语义求值规则进行重写定义：

    a::=...∣a0+a1∣...a0:Aexpa1:Aexpa0+a1:Aexpa::=...|a_0+a_1|...\\ \frac{a_0:Aexp\quad a_1:Aexp}{a_0+a_1:Aexp}

    c::=...∣X:=a∣...∣if  b  then  c0  else  c1∣...X:Loca:AexpX:=a:Com,b:Bexpc0:Comc1:Comif  b  then  c0  else  c1:Comc::=...|X:=a|...|if\;b\;then\;c_0\;else\;c_1|...\\ \frac{X:Loc\quad a:Aexp}{X:=a:Com},\frac{b:Bexp\quad c_0:Com\quad c_1:Com}{if\;b\;then\;c_0\;else\;c_1:Com}

# 特殊的规则归纳法

  • 规则归纳法的特殊原理：

    设IRI_R 是规则实例集 R 定义的集合，A⊆IRA\subseteq I_R，Q 是某个性质。则∀a∈A,Q(a)\forall a\in A,Q(a) 当且仅当对于 R 中所有规则实例X/yX/y，其中X⊆IR,y∈AX\subseteq I_R,y\in A，有:

    (∀x∈X∩A,Q(x))⇒Q(y)(\forall x\in X\cap A,Q(x))\Rightarrow Q(y)

    下面我们说明为什么这个特殊原理和一般原理并没什么本质不同。特殊原理想证明对 A 中所有元素都满足性质 Q，我们可以对IRI_R 中元素定义性质 P：

    P(x)⇔(x∈A⇒Q(x))P(x)\Leftrightarrow(x\in A\Rightarrow Q(x))

    因此证明 A 中所有元素满足 Q 就等价于证明IRI_R 中所有元素满足 P。按照规则归纳法一般原理，即要证：

    ∀(X/y)∈R,[X⊆IR&(∀x∈X,P(x))⇒P(y)]⇔∀(X/y)∈R,[X⊆IR&(∀x∈X,x∈A⇒Q(x))]⇒(y∈A⇒Q(y))\forall(X/y)\in R,[X\subseteq I_R\&(\forall x\in X,P(x))\Rightarrow P(y)]\\ \Leftrightarrow\\ \forall(X/y)\in R,[X\subseteq I_R\&(\forall x\in X,x\in A\Rightarrow Q(x))]\Rightarrow(y\in A\Rightarrow Q(y))

    然后考虑蕴涵条件引入，原式逻辑等价于：

    ∀(X/y)∈R,[X⊆IR&y∈A&(∀x∈X,x∈A⇒Q(x))]⇒Q(y)⇔∀(X/y)∈R,[X⊆IR&y∈A&(∀x∈X∩A,Q(x))]⇒Q(y)\forall(X/y)\in R,[X\subseteq I_R\& y\in A\&(\forall x\in X,x\in A\Rightarrow Q(x))]\Rightarrow Q(y)\\ \Leftrightarrow\\ \forall(X/y)\in R,[X\subseteq I_R\&y\in A\&(\forall x\in X\cap A,Q(x))]\Rightarrow Q(y)

    也就是规则归纳法特殊原理。

# 操作语义的证明规则

# 算术表达式的规则归纳法

  • 对所有的求值关系⟨a,σ⟩→n\lang a,\sigma\rang\rightarrow n，性质P(a,σ,n)P(a,\sigma,n) 为真当且仅当构造该算术表达式的规则都保持了性质P。逻辑化地：

    ∀a∈Aexp,σ∈Σ,n∈N,⟨a,σ⟩→n⇒P(a,σ,n)iff[∀n∈N,σ∈Σ,P(n,σ,n)&∀X∈Loc,σ∈Σ,P(X,σ,σ(X))&∀a0,a1∈Aexp,σ∈Σ,n0,n1∈N,⟨a0,σ⟩→n0&P(a0,σ,n0)&⟨a1,σ⟩→n1&P(a1,σ,n1)⇒P(a0+a1,σ,n0+n1)&∀a0,a1∈Aexp,σ∈Σ,n0,n1∈N,⟨a0,σ⟩→n0&P(a0,σ,n0)&⟨a1,σ⟩→n1&P(a1,σ,n1)⇒P(a0−a1,σ,n0−n1)&∀a0,a1∈Aexp,σ∈Σ,n0,n1∈N,⟨a0,σ⟩→n0&P(a0,σ,n0)&⟨a1,σ⟩→n1&P(a1,σ,n1)⇒P(a0×a1,σ,n0×n1)]\forall a\in Aexp,\sigma\in\Sigma,n\in N,\lang a,\sigma\rang\rightarrow n\Rightarrow P(a,\sigma,n)\\ iff\\ [\forall n\in N,\sigma\in\Sigma,P(n,\sigma,n)\\ \&\\ \forall X\in Loc,\sigma\in\Sigma,P(X,\sigma,\sigma(X))\\ \&\\ \forall a_0,a_1\in Aexp,\sigma\in\Sigma,n_0,n_1\in N,\lang a_0,\sigma\rang\rightarrow n_0\&P(a_0,\sigma,n_0)\&\lang a_1,\sigma\rang\rightarrow n_1\& P(a_1,\sigma,n_1)\Rightarrow P(a_0+a_1,\sigma,n_0+n_1)\\ \&\\ \forall a_0,a_1\in Aexp,\sigma\in\Sigma,n_0,n_1\in N,\lang a_0,\sigma\rang\rightarrow n_0\&P(a_0,\sigma,n_0)\&\lang a_1,\sigma\rang\rightarrow n_1\& P(a_1,\sigma,n_1)\Rightarrow P(a_0-a_1,\sigma,n_0-n_1)\\ \&\\ \forall a_0,a_1\in Aexp,\sigma\in\Sigma,n_0,n_1\in N,\lang a_0,\sigma\rang\rightarrow n_0\&P(a_0,\sigma,n_0)\&\lang a_1,\sigma\rang\rightarrow n_1\& P(a_1,\sigma,n_1)\Rightarrow P(a_0\times a_1,\sigma,n_0\times n_1)]\\

    因为所有的表达式都是从规则实例退出来的嘛。注意考虑 “保持性质” 的含义。

# 布尔表达式的规则归纳法

  • 不同于算术表达式规则，布尔表达式的规则需要依赖于算术表达式的求值规则（譬如计算a0=a1a_0=a_1 需要先分别对表达式a0,a1a_0,a_1 求值）。所以实际上，它的规则实例集合 R 应该包含了算术表达式求值规则实例集合。

    举个不完全的例子，例如有个算术表达式求值的规则实例集合：R={⟨3,σ0⟩→3‾}R=\{\overline{\lang 3,\sigma_0\rang\rightarrow 3}\}，那么为了推导⟨3=3,σ0⟩→true\lang 3=3,\sigma_0\rang\rightarrow true，其对应的规则实例集合为：R′={⟨3,σ0⟩→3‾,⟨3,σ0⟩→3⟨3,σ0⟩→3⟨3=3 σ0⟩→true}R'=\{\overline{\lang 3,\sigma_0\rang\rightarrow 3},\frac{\lang 3,\sigma_0\rang\rightarrow 3\quad\lang 3,\sigma_0\rang\rightarrow 3}{\lang 3=3\,\sigma_0\rang\rightarrow true}\}，即R⊆R′R\subseteq R'。

  • 因此，我们如果想证明所有求值关系⟨b,σ⟩→t\lang b,\sigma\rang\rightarrow t 满足某性质P(b,σ,t)P(b,\sigma,t)，实际上需要使用一手特殊规则归纳法，在考虑布尔表达式规则是否保持性质时，若前提中出现了算术表达式求值规则，可以不去管他是否保持性质。

    ∀b∈Bexp,σ∈Σ,t∈T,⟨b,σ⟩⇒P(b,σ,t)iff[∀σ∈Σ,P(false,σ,false)&∀σ∈Σ,P(true,σ,true)&∀a0,a1∈Aexp,σ∈Σ,m,n∈N,⟨a0σ⟩→m&⟨a1,σ⟩→n&m=n⇒P(a0=a1,σ,true)&∀a0,a1∈Aexp,σ∈Σ,m,n∈N,⟨a0σ⟩→m&⟨a1,σ⟩→n&m≠n⇒P(a0=a1,σ,false)&∀a0,a1∈Aexp,σ∈Σ,m,n∈N,⟨a0σ⟩→m&⟨a1,σ⟩→n&m≤n⇒P(a0≤a1,σ,true)&∀a0,a1∈Aexp,σ∈Σ,m,n∈N,⟨a0σ⟩→m&⟨a1,σ⟩→n&m>n⇒P(a0≤a1,σ,false)&∀b∈Bexp,σ∈Σ,t∈T,⟨b,σ⟩→t&P(b,σ,t)⇒P(¬b,σ,¬t)&∀b0,b1∈Bexp,σ∈Σ,t0,t1∈T,⟨b0,σ⟩→t0&P(b0,σ,t0)&⟨b1,σ⟩→t1&P(b1,σ,t1)⇒P(b0∧b1,σ,t0∧t1)&∀b0,b1∈Bexp,σ∈Σ,t0,t1∈T,⟨b0,σ⟩→t0&P(b0,σ,t0)&⟨b1,σ⟩→t1&P(b1,σ,t1)⇒P(b0∨b1,σ,t0∨t1)\forall b\in Bexp,\sigma\in\Sigma,t\in T,\lang b,\sigma\rang\Rightarrow P(b,\sigma,t)\\ iff\\ [\forall\sigma\in \Sigma,P(false,\sigma,false)\&\forall\sigma\in\Sigma,P(true,\sigma,true)\\ \&\\ \forall a_0,a_1\in Aexp,\sigma\in\Sigma,m,n\in N,\lang a_0\sigma\rang\rightarrow m\&\lang a_1,\sigma\rang\rightarrow n\& m=n\Rightarrow P(a_0=a_1,\sigma,true)\\ \&\\ \forall a_0,a_1\in Aexp,\sigma\in\Sigma,m,n\in N,\lang a_0\sigma\rang\rightarrow m\&\lang a_1,\sigma\rang\rightarrow n\& m\neq n\Rightarrow P(a_0=a_1,\sigma,false)\\ \&\\ \forall a_0,a_1\in Aexp,\sigma\in\Sigma,m,n\in N,\lang a_0\sigma\rang\rightarrow m\&\lang a_1,\sigma\rang\rightarrow n\& m\leq n\Rightarrow P(a_0\leq a_1,\sigma,true)\\ \&\\ \forall a_0,a_1\in Aexp,\sigma\in\Sigma,m,n\in N,\lang a_0\sigma\rang\rightarrow m\&\lang a_1,\sigma\rang\rightarrow n\& m> n\Rightarrow P(a_0\leq a_1,\sigma,false)\\ \&\\ \forall b\in Bexp,\sigma\in \Sigma,t\in T,\lang b,\sigma\rang\rightarrow t\&P(b,\sigma,t)\Rightarrow P(\neg b,\sigma,\neg t)\\ \&\\ \forall b_0,b_1\in Bexp,\sigma\in\Sigma,t_0,t_1\in T,\lang b_0,\sigma\rang\rightarrow t_0\&P(b_0,\sigma,t_0)\&\lang b_1,\sigma\rang\rightarrow t_1\&P(b_1,\sigma,t_1)\Rightarrow P(b_0\wedge b_1,\sigma,t_0\wedge t_1)\\ \&\\ \forall b_0,b_1\in Bexp,\sigma\in\Sigma,t_0,t_1\in T,\lang b_0,\sigma\rang\rightarrow t_0\&P(b_0,\sigma,t_0)\&\lang b_1,\sigma\rang\rightarrow t_1\&P(b_1,\sigma,t_1)\Rightarrow P(b_0\vee b_1,\sigma,t_0\vee t_1)\\

# 命令的规则归纳法

  • 命令的规则实例前提中可能出现布尔表达式求值和算术表达式求值。但是因为特殊规则归纳法原理，我们只需要考虑对应命令的保持性质。

∀c∈Com,σ,σ′∈Σ,⟨c,σ⟩→σ′⇒P(c,σ,σ′)iff∀σ∈Σ,P(skip,σ,σ)&∀σ∈Σ,X∈Loc,a∈Aexp,m∈N,⟨a,σ⟩→m⇒P(X:=a,σ,σ[m/X])&∀c0,c1∈Com,σ,σ′,σ′′∈Σ,⟨c0,σ⟩→σ′&P(c0,σ,σ′)&⟨c1,σ′⟩→σ′′&P(c1,σ′,σ′′)⇒P(c0;c1,σ,σ′′)&∀c0,c1∈Com,σ,σ′∈Σ,b∈Bexp,⟨b,σ⟩⇒true&⟨c0,σ⟩→σ′&P(c0,σ,σ′)⇒P(if  b  then  c0  else  c1,σ,σ′)&∀c0,c1∈Com,σ,σ′∈Σ,b∈Bexp,⟨b,σ⟩⇒false&⟨c1,σ⟩→σ′&P(c1,σ,σ′)⇒P(if  b  then  c0  else  c1,σ,σ′)&∀c∈Com,b∈Bexp,σ∈Σ,⟨b,σ⟩→false⇒P(while  b  do  c,σ,σ)∀c∈Com,b∈Bexp,σ,σ′,σ′′∈Σ,⟨b,σ⟩→true&⟨c,σ⟩→σ′&P(c,σ,σ′)&⟨while  b  do  c,σ′⟩→σ′′&P(while  b  do  c,σ′,σ′′)⇒P(while  b  do  c,σ,σ′′)\forall c\in Com,\sigma,\sigma'\in\Sigma,\lang c,\sigma\rang\rightarrow \sigma'\Rightarrow P(c,\sigma,\sigma')\\ iff\\ \forall \sigma\in\Sigma,P(skip,\sigma,\sigma)\\ \&\\ \forall\sigma\in\Sigma,X\in Loc,a\in Aexp,m\in N,\lang a,\sigma\rang\rightarrow m\Rightarrow P(X:=a,\sigma,\sigma[m/X])\\ \&\\ \forall c_0,c_1\in Com,\sigma,\sigma',\sigma''\in\Sigma,\lang c_0,\sigma\rang\rightarrow\sigma'\&P(c_0,\sigma,\sigma')\&\lang c_1,\sigma'\rang\rightarrow \sigma''\& P(c_1,\sigma',\sigma'')\Rightarrow P(c_0;c_1,\sigma,\sigma'')\\ \&\\ \forall c_0,c_1\in Com,\sigma,\sigma'\in \Sigma,b\in Bexp,\lang b,\sigma\rang\Rightarrow true\&\lang c_0,\sigma\rang\rightarrow \sigma'\& P(c_0,\sigma,\sigma')\Rightarrow P(if\;b\;then\;c_0\;else\;c_1,\sigma,\sigma')\\ \&\\ \forall c_0,c_1\in Com,\sigma,\sigma'\in \Sigma,b\in Bexp,\lang b,\sigma\rang\Rightarrow false\&\lang c_1,\sigma\rang\rightarrow \sigma'\& P(c_1,\sigma,\sigma')\Rightarrow P(if\;b\;then\;c_0\;else\;c_1,\sigma,\sigma')\\ \&\\ \forall c\in Com,b\in Bexp,\sigma\in\Sigma,\lang b,\sigma\rang\rightarrow false\Rightarrow P(while\;b\;do\;c,\sigma,\sigma)\\ \forall c\in Com,b\in Bexp,\sigma,\sigma',\sigma''\in\Sigma,\lang b,\sigma\rang\rightarrow true\&\lang c,\sigma\rang\rightarrow\sigma'\& P(c,\sigma,\sigma')\& \lang while\;b\;do\;c,\sigma'\rang\rightarrow\sigma''\& P(while\;b\;do\;c,\sigma',\sigma'')\\ \Rightarrow P(while\;b\;do\;c,\sigma,\sigma'')

# 规则归纳法的一个示例证明

  • 命题：设Y∈LocY\in Loc，对所有的命令cc 和状态σ,σ′\sigma,\sigma'，有：

    Y∉locL(c)&⟨c,σ⟩→σ′⇒σ(Y)=σ′(Y)Y\notin loc_L(c)\&\lang c,\sigma\rang\rightarrow\sigma'\Rightarrow\sigma(Y)=\sigma'(Y)

    其中，locL(c)loc_L(c) 表示出现在命令 c 中赋值命令的存储单元的集合。

    证明：设性质 P：

    P(c,σ,σ′)⇔(Y∉locL(c)⇒σ(Y)=σ′(Y))P(c,\sigma,\sigma')\Leftrightarrow (Y\notin loc_L(c)\Rightarrow \sigma(Y)=\sigma'(Y))

    使用命令的规则归纳法：

    • c≡skipc\equiv skip，则locL(c)=∅loc_L(c)=\emptyset，显然P(skip,σ,σ)P(skip,\sigma,\sigma) 满足性质

    • c≡X:=ac\equiv X:=a，设⟨a,σ⟩→m∈N\lang a,\sigma\rang\rightarrow m\in N，则Y∉locL(c)⇒Y≠X⇒σ(Y)=σ[m/X](Y)=σ′(Y)Y\notin loc_L(c)\Rightarrow Y\neq X\Rightarrow\sigma(Y)=\sigma[m/X](Y)=\sigma'(Y)，故P(X:=a,σ,σ′)P(X:=a,\sigma,\sigma') 成立

      （其实上面两种情况对应了奠基步骤）

    • 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'')

      又因为Y∉locL(c)=locL(c0)∪logL(c1)Y\notin loc_L(c)=loc_L(c_0)\cup log_L(c_1)，因此根据条件有

      P(c0,σ,σ′)&Y∉locL(c0)⇒σ(Y)=σ′(Y)P(c1,σ′,σ′′)&Y∉locL(c1)⇒σ′(Y)=σ′′(Y)⇒σ(Y)=σ′′(Y)P(c_0,\sigma,\sigma')\&Y\notin loc_L(c_0)\Rightarrow \sigma(Y)=\sigma'(Y)\\ P(c_1,\sigma',\sigma'')\& Y\notin loc_L(c_1)\Rightarrow\sigma'(Y)=\sigma''(Y)\\ \Rightarrow \sigma(Y)=\sigma''(Y)

      从而P(c0;c1,σ,σ′′)P(c_0;c_1,\sigma,\sigma'') 成立

    • c≡if  b  then  c0  else  c1c\equiv if\;b\;then\;c_0\;else\;c_1

      • 情况 1，引入条件：

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

        此时，Y∉locL(c)=locL(c0)∪logL(c1)Y\notin loc_L(c)=loc_L(c_0)\cup log_L(c_1)，可以推得：

        P(c0,σ,σ′)&Y∉locL(c0)⇒σ(Y)=σ′(Y)P(c_0,\sigma,\sigma')\&Y\notin loc_L(c_0)\Rightarrow \sigma(Y)=\sigma'(Y)

      • 情况 2，引入条件：

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

        推得：

        P(c1,σ,σ′)&Y∉locL(c1)⇒σ(Y)=σ′(Y)P(c_1,\sigma,\sigma')\&Y\notin loc_L(c_1)\Rightarrow\sigma(Y)=\sigma'(Y)

        即P(c,σ,σ′)P(c,\sigma,\sigma') 成立。

    • c≡while  b  do  c0c\equiv while\;b\;do\;c_0

      • 情况 1，引入条件：

        ⟨b,σ⟩→false&P(c,σ,σ)\lang b,\sigma\rang\rightarrow false\&P(c,\sigma,\sigma)

        此时P(c,σ,σ)P(c,\sigma,\sigma) 显然成立的。

      • 情况 2，引入条件：

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

        而Y∉locL(c)=locL(c0)Y\notin loc_L(c)=loc_L(c_0)，因此可以推得：

        P(c0,σ,σ′)&Y∉locL(c0)⇒σ(Y)=σ′(Y)P(c,σ′,σ′′)&Y∉locL(c)⇒σ′(Y)=σ′′(Y)⇒σ(Y)=σ′′(Y)P(c_0,\sigma,\sigma')\& Y\notin loc_L(c_0)\Rightarrow\sigma(Y)=\sigma'(Y)\\ P(c,\sigma',\sigma'')\&Y\notin loc_L(c)\Rightarrow\sigma'(Y)=\sigma''(Y)\\ \Rightarrow\sigma(Y)=\sigma''(Y)

        即P(c,σ,σ′′)P(c,\sigma,\sigma'') 成立，保持了性质。

    到此整完了所有规则保持性质，即证毕。

# 算子其最小不动点

  • 一组规则示例 R 确定了集合上得算子R^\hat{R}，当其作用于某集合 B 时：

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

    显然，得到的集合R^(B)\hat{R}(B) 对 R 是封闭的。

  • 命题：一个集合 B 是 R 封闭的，当且仅当R^(B)⊆B\hat{R}(B)\subseteq B。

    证明：∀y∈R^(B)\forall y\in \hat{R}(B) 都存在X/y∈R,X⊆BX/y\in R,X\subseteq B。又因为 B 对 R 封闭，所以有y∈By\in B，所以有R^(B)⊆B\hat{R}(B)\subseteq B。

    ​ 充分性更好证。

  • 我们可以记An=R^n(∅)=R^(R^(...R^(∅)))A_n=\hat{R}^n(\emptyset)=\hat{R}(\hat{R}(...\hat{R}(\emptyset)))。然后显然有一条有限的链：

    A0⊆A1⊆A2...⊆An⊆...A_0\subseteq A_1\subseteq A_2...\subseteq A_n\subseteq...

    因为实际上A1A_1 就是 R 中所有公理得结论，A2A_2 就是所有一级结论和二级结论…

    取A=⋃n∈ωAnA=\bigcup_{n\in\omega}A_n，有如下命题：

    • A 是对 R 封闭的。

      证明：显然，∀X/y∈R,X⊆A\forall X/y\in R,X\subseteq A，必定存在nn，使得X⊆AnX\subseteq A_n。再根据算子定义，有y∈R^(An)=An+1y\in \hat{R}(A_n)=A_{n+1}，因此y∈Ay\in A。

    • R^(A)=A\hat{R}(A)=A。可以证明R^(A)⊆A,A⊆R^(A)\hat{R}(A)\subseteq A,A\subseteq\hat{R}(A)。

    • A 是对 R 封闭的最小集合。

      证明：设 B 是另一个对 R 封闭的集合，我们证明A⊆BA\subseteq B。

      因为 B 对 R 封闭，所以R^(B)⊆B\hat{R}(B)\subseteq B。用数学归纳法，∅=A0⊆B\emptyset=A_0\subseteq B，然后

      ∵An⊆B⇒R^(An)⊆R^(B)∴An+1⊆R^(B)⊆B∴∀n∈ω,An⊆B∴A⊆B\because A_n\subseteq B\Rightarrow \hat{R}(A_n)\subseteq\hat{R}(B)\\ \therefore A_{n+1}\subseteq \hat{R}(B)\subseteq B\\ \therefore \forall n\in\omega,A_n\subseteq B\\ \therefore A\subseteq B

  • 其实这里我已经意识到了A=IRA=I_R。

  • 关于上面的链为什么是有限的，实际上是因为IRI_R 是R^\hat{R} 的一个不动点：

    R^(B)=B⇒IR⊆B\hat{R}(B)=B\Rightarrow I_R\subseteq B

    显然，IR=⋃n∈ωR^n(∅)I_R=\bigcup_{n\in\omega}\hat{R}^n(\emptyset) 是R^\hat{R} 的最小不动点。