Home

我最喜欢吃红豆了。

单独开一篇讨论不动点在证明循环时候的作用。可恶

我选择用操作语义去证明它。回顾 while 的操作语义w=while  b  do  cw=while\;b\;do\;c：

⟨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'}

下面，我将结合C:=0;while  C<1  do  C:=C+1;C:=0;while\;C<1\;do\;C:=C+1; 这个例子来说明证明方法。

（先用顺序赋值整个⟨C:=0,σ0⟩→σ1\lang C:=0,\sigma_0\rang\rightarrow\sigma_1

  • 构造规则实例集合RR。在例子中，有：

    R={(0):∅⟨C,σ1⟩→0,(1):⟨C,σ1⟩→0⟨C<1,σ1⟩→true,(2):⟨C,σ1⟩→0⟨C:=C+1,σ1⟩→σ1[1/C],(3):∅⟨C,σ1[1/C]⟩→1,(4):⟨C,σ1[1/C]⟩→1⟨C<1,σ1[1/C]⟩→false,(5):⟨C<1,σ1[1/C]⟩→false⟨w,σ1[1/C]⟩→σ1[1/C],(6):⟨C<1,σ1⟩→true⟨C:=C+1,σ1⟩→σ1[1/C]⟨w,σ1[1/C]⟩→σ1[1/C]⟨w,σ1[1/C]⟩→σ1[1/C],}R=\{\\ (0):\frac{\emptyset}{\lang C,\sigma_1\rang\rightarrow 0},\\ (1):\frac{\lang C,\sigma_1\rang\rightarrow 0}{\lang C<1,\sigma_1\rang\rightarrow true},\\ (2):\frac{\lang C,\sigma_1\rang\rightarrow 0}{\lang C:=C+1,\sigma_1\rang\rightarrow\sigma_1[1/C]},\\ (3):\frac{\emptyset}{\lang C,\sigma_1[1/C]\rang\rightarrow 1},\\ (4):\frac{\lang C,\sigma_1[1/C]\rang\rightarrow 1}{\lang C<1,\sigma_1[1/C]\rang\rightarrow false},\\ (5):\frac{\lang C<1,\sigma_1[1/C]\rang\rightarrow false}{\lang w,\sigma_1[1/C]\rang\rightarrow\sigma_1[1/C]},\\ (6):\frac{\lang C<1,\sigma_1\rang\rightarrow true\quad\lang C:=C+1,\sigma_1\rang\rightarrow\sigma_1[1/C]\quad\lang w,\sigma_1[1/C]\rang\rightarrow\sigma_1[1/C]}{\lang w,\sigma_1[1/C]\rang\rightarrow \sigma_1[1/C]},\\ \}

    这其实是我们解这个循环需要的所有的规则实例了。

  • 构造算子R^\hat{R}：

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

    注意，关键是有这样一条链：

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

    这是为什么？先看下例子：

    R^(∅)={⟨C,σ1⟩→0,⟨C,σ1[1/C]⟩→1}，由规则实例(0),(3)R^2(∅)={⟨C,σ1⟩→0,⟨C,σ1[1/C]⟩→1,⟨C<1,σ1⟩→true,⟨C:=C+1,σ1⟩→σ1[1/C],⟨C<1,σ1[1/C]⟩→false}由规则实例(0),(3),(1),(2),(4)\hat{R}(\emptyset)=\{\lang C,\sigma_1\rang\rightarrow 0,\lang C,\sigma_1[1/C]\rang\rightarrow 1\}，由规则实例(0),(3)\\ \hat{R}^2(\emptyset)=\{\lang C,\sigma_1\rang\rightarrow 0,\lang C,\sigma_1[1/C]\rang\rightarrow 1,\lang C<1,\sigma_1\rang\rightarrow true,\lang C:=C+1,\sigma_1\rang\rightarrow\sigma_1[1/C],\lang C<1,\sigma_1[1/C]\rang\rightarrow false\}\\ 由规则实例(0),(3),(1),(2),(4)

    实际上，我们可以对得到的结论进行分层。一层为公理（由空集推出），二层为由一层结论和公理推出的，三层为前两次和公理推出的…

    于是很显然，R^(∅)\hat{R}(\emptyset) 就包含了公理，而R^2(∅)\hat{R}^2(\emptyset) 就包含了公理和一层结论（因为当然∅⊆R^(∅)\emptyset\subseteq \hat{R}(\emptyset)）。而R^3(∅)\hat{R}^3(\emptyset) 就包含了公理，一层结论和二层结论。画个图的话，就如下：

    1

    于是我们发现，随着算子R^\hat{R} 的迭代，有：

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

  • 于是我们就可以定义fix=⋃n∈ωR^n(∅)fix=\bigcup_{n\in\omega}\hat{R}^n(\emptyset) 了。

    • 首先，fixfix 是对RR 封闭的。很显然，∀X⊆fix,Xy∈R\forall X\subseteq fix,\frac{X}{y}\in R，有y∈fixy\in fix。
    • 其次，因为fixfix 是对RR 封闭的，所以R^(fix)⊆fix\hat{R}(fix)\subseteq fix。因为∀y∈R^(fix)\forall y\in\hat{R}(fix)，由R^\hat{R} 算子的定义，都有∃X⊆fix,Xy∈R\exists X\subseteq fix,\frac{X}{y}\in R。而 fix 是对 R 封闭的，所以有y∈fixy\in fix。
    • 再者，有fix⊆R^(fix)fix\subseteq \hat{R}(fix)。因为∀y∈fix\forall y\in fix，∃n,y∈R^n(∅)\exists n,y\in\hat{R}^n(\emptyset)。那么根据算子定义就有∃X,X⊆R^n−1(∅)⊆fix\exists X,X\subseteq\hat{R}^{n-1}(\emptyset)\subseteq fix。根据算子定义，就有y∈R^(fix)y\in\hat{R}(fix)。
    • 于是综上，就有了R^(fix)=fix\hat{R}(fix)=fix。而fixfix 集合就是我们要的循环的操作语义，就是一层层循环计算的过程。

为什么要整这么麻烦？为什么不能直接很显然地：

R^(fix)=⋃n=2,3,4,...R^n(∅)=⋃n=2,3,4,...R^n(∅)∪∅=⋃n∈ωR^n(∅)=fix\hat{R}(fix)=\bigcup_{n=2,3,4,...}\hat{R}^n(\empty)=\bigcup_{n=2,3,4,...}\hat{R}^n(\empty)\cup\emptyset=\bigcup_{n\in\omega}\hat{R}^n(\empty)=fix

呢？其实这牵扯到一个域收敛的问题。当这个循环是有限次截至的话，因为规则实例一定是有限个，那么这么写肯定没问题。但对一般的循环我们不清楚执行情况的话，证明将变得不严谨。其实还是用到了一个定理：

  • 完全格上的单调连续函数一定有不动点。