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

# IMP 的指称语义

# 目的

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

以 IMP 语言为例:

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

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

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

# 指称语义

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

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

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

# 算术表达式的指称

结构归纳法定义:

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

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

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

# 布尔表达式的指称

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

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

# 命令的指称

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


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

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

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

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

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

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

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

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

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

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

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

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

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

其中,Γ(f)={(σ,σ)β(σ)=true,(σ,σ)fγ}{(σ,σ)β(σ)=false}\Gamma(f)=\{(\sigma,\sigma')|\beta(\sigma)=true,(\sigma,\sigma')\in f\circ\gamma\}\cup\{(\sigma,\sigma)|\beta(\sigma)=false\}

# 语义的等价性

  • 引理:对所有的aAexpa\in Aexp,有

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

    对所有的bBexpb\in Bexp,有

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

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

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

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

    证明:定义性质 P:

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

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

    • cc0;c1c\equiv c_0;c_1,引入前提:

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

      然后有

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

      所以

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

    • 其他情况类似

    • 再讨论下wwhile  b  do  cw\equiv while\;b\;do\;c,条件为真的情况。引入前提:

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

      根据前提和性质,推得:

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

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

      再由指称语义的定义,有

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

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

  • 事实上,有:

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

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

# 完全偏序与连续函数

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

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

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

    以及考察如何用集合链

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

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

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

  • 定义,如果集合 P 上的二元关系\sqsubseteq 满足:

    • 自反性:pP,pp\forall p\in P,p\sqsubseteq p
    • 传递性:p,q,rP,pq&qrpr\forall p,q,r\in P,p\sqsubseteq q\&q\sqsubseteq r\Rightarrow p\sqsubseteq r
    • 反对称性:p,qP,pq&qpp=q\forall p,q\in P,p\sqsubseteq q\& q\sqsubseteq p\Rightarrow p=q

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

  • 定义,对于偏序(P,)(P,\sqsubseteq) 和子集XPX\subseteq P,称 p 是XX上界,当且仅当:

    qX,qp\forall q\in X,q\sqsubseteq p

    称 p 是 X 的最小上界,当且仅当:

    • p 是 X 的上界
    • 对于所有 X 的上界qq,有pqp\sqsubseteq q

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

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

    d0Dd1D...DdnD...d_0\sqsubseteq_D d_1\sqsubseteq_D...\sqsubseteq_D d_n\sqsubseteq_D...

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

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

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

  • 考察用规则实例集合RR 定义的算子,若B0B1...Bn...B_0\subseteq B_1\subseteq ...\subseteq B_n\subseteq ...,则有:

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

    又因为n,BnnωBnn,R^(Bn)R^(nωBn)\forall n,B_n\subseteq\bigcup_{n\in\omega} B_n\Rightarrow \forall n,\hat{R}(B_n)\in\hat{R}(\bigcup_{n\in\omega}B_n),所以有:

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

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

    n,XBnyR^(Bn)ynωR^(Bn)\exists n,X\subseteq B_n\\ \therefore y\in\hat{R}(B_n)\\ \therefore y\in\bigcup_{n\in\omega}\hat{R}(B_n)

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

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

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

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

    d,dD,dDdf(d)Ef(d)\forall d,d'\in D,d\sqsubseteq_D d'\Rightarrow f(d)\sqsubseteq_Ef(d')

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

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

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

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

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

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

    证明:由连续性,

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

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

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

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

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

# Knaster-Tarski 定理

  • 对一组规则实例 R,有

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

    命题等价为:

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

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

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

    qX,pq\forall q\in X,p\sqsubseteq q

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

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

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

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

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

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

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

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

    证明,以最小前缀不动点为例:

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

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

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

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

# IMP 的公理语义

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

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

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

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

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

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

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

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

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

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

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

# 断言语言 Assn

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

    a::=nXia0+a1a0a1a0×a1a::=n|X|i|a_0+a_1|a_0-a_1|a_0\times a_1

    其中nN,XLoc,iIntvarn\in N,X\in Loc,i\in IntvarIntvarIntvar 为整型变量集。

    然后,扩充BexpBexp

    b::=truefalsea0=a1a0a1b0b1b0b1¬b0b0b1i,bi,bb::=true|false|a_0=a_1|a_0\leq a_1|b_0\vee b_1|b_0\wedge b_1|\neg b_0|b_0\Rightarrow b_1|\forall i,b|\exists i,b

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

# 自由变量与约束变量

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

  • FV(a)FV(a) 为算术表达式aAexpva\in Aexpv(扩充集合)中的自由变量集合,有:

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

    对断言(布尔表达式)的定义为:

    FV(true)=FV(false)=FV(a0=a1)=FV(a0a1)=FV(a0)FV(a1)FV(b0b1)=FV(b0b1)=FV(b0)FV(b1)FV(¬b0)=FV(b0)FV(i,b0)=FV(i,b0)=FV(b0)/{i}FV(true)=FV(false)=\emptyset\\ FV(a_0=a_1)=FV(a_0\leq a_1)=FV(a_0)\cup FV(a_1)\\ FV(b_0\vee b_1)=FV(b_0\wedge b_1)=FV(b_0)\cup FV(b_1)\\ FV(\neg b_0)=FV(b_0)\\ FV(\forall i,b_0)=FV(\exists i,b_0)=FV(b_0)/\{i\}

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

# 代入

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

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

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

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

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

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

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

# 断言的语义

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

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

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

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

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

    这个结构归纳一下就好。

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

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

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

    σItrueσI(a0=a1)ifAv[a0]Iσ=Av[a1]IσσI(a0a1)ifAv[a0]IσAv[a1]IσσIABifσIA  and  σIBσIABifσIA  or  σIBσI¬Aifnot  σIAσIABif(not  σIA)  or  σIBσIi,Aifnn,σI[n/i]AσIi,Aifnn,σI[n/i]AIA\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

    bBexpb\in BexpσΣ\sigma\in\Sigma 和任一解释 I,有B[b]σ=true\mathscr{B}[b]\sigma=true 当且仅当σIb\sigma\models^I b

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

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

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

  • 部分正确性断言形如

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

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

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

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

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


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

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

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

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

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

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

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

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

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

  • 例,若有(AB)\models(A\Rightarrow B),则有

    σΣ,((σIA)(σIB))\forall\sigma\in\Sigma_\perp,((\sigma\models^I A)\Rightarrow(\sigma\models^I B))

    AIBIA^I\subseteq B^I。(在解释 I 下,A 成立的状态集合为 B 成立的状态集合的子集)

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

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

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

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

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

  • skip 规则:

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

  • 赋值规则:

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

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

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

  • 条件规则:

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

  • while 循环规则:

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

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

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

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

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

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


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

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

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

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

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

  • 引理:对a,a0Aexpv,XLoca,a_0\in Aexpv,X\in Loc,则对所有的解释II 和状态σ\sigma,有:

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

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

  • 引理:设II 是一个解释,BAssn,XLoc,aAexpB\in Assn,X\in Loc,a\in Aexp,则对所有的状态σΣ\sigma\in\Sigma,有:

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

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

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

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

    • skip:显然{A}skip{A}\models\{A\}skip\{A\} 成立,因此该规则可靠。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      wwhile  b  do  cw\equiv while\;b\;do\;c,回忆之前的指称语义,有

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

      其中

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

      定义性质 P:

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

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

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

      σΣ,σIAC[w]σIA¬b\forall\sigma\in \Sigma,\sigma\models^I A\Rightarrow\mathscr{C}[w]\sigma\models^I A\wedge\neg b,即有{A}w{A¬b}\models \{A\}w\{A\wedge\neg b\}

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

      • P(n)P(n) 成立,考虑

        B[b]σ=false&σ=σ\mathscr{B}[b]\sigma=false\& \sigma'=\sigma,于是B[b]σ=false\mathscr{B}[b]\sigma'=false,于是σIAσIA¬b\sigma\models^I A\Rightarrow\sigma'\models^I A\wedge\neg b

        B[b]σ=true&(σ,σ)θnC[c]\mathscr{B}[b]\sigma=true\&(\sigma,\sigma')\in\theta_n\circ\mathscr{C}[c],于是σ,(σ,σ)C[c]\exists\sigma'',(\sigma,\sigma'')\in\mathscr{C}[c]

        C[b]σ=trueσIAσIAb{Ab}c{A}σIAσIA(σ,σ)θn,P(n)σIAσIA¬b\because \mathscr{C}[b]\sigma=true\\ \therefore\sigma\models^I A\Rightarrow\sigma\models^I A\wedge b\\ \because\models\{A\wedge b\}c\{A\}\\ \therefore \sigma\models^I A\Rightarrow\sigma''\models^I A\\ \because (\sigma'',\sigma')\in\theta_n,P(n)\\ \therefore \sigma\models^I A\Rightarrow\sigma'\models^I A\wedge\neg b

        因此得到证明成立。

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

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

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

      于是有

      σIAσIAC[c]σIBC[c]σIBσ,I,σIAC[c]σIB\sigma\models^IA\Rightarrow \sigma\models^I A'\Rightarrow\mathscr{C}[c]\sigma\models^I B'\Rightarrow\mathscr{C}[c]\sigma\models^I B\\ \therefore \forall\sigma,I,\sigma\models^I A\Rightarrow\mathscr{C}[c]\sigma\models^I B

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

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

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

换为数学语言,我们要证明:

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

考虑一个不变式

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

先证明它确实是一个不变式,即{IX>0}w{I}\{I\wedge X>0\}w\{I\}(当然,{IX0}w{I}\{I\wedge X\leq 0\}w\{I\} 是显然的,结合起来就有{I}w{I}\{I\}w\{I\}

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

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

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

其中,I[(X1)/X]=Y×(X1)!=n!(X1)0I[(X-1)/X]=Y\times(X-1)!=n!\wedge(X-1)\geq 0。再根据赋值规则,有:

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

这样,由顺序规则,有:

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

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

于是根据推论规则,有:

(IX>0Y×X!=n!(X1)0){Y×X!=n!(X1)0}Y:=X×Y;X:=X1{I}II{IX>0}Y:=X×Y;X=X1{I}\frac{\models(I\wedge X>0 \Rightarrow Y\times X!=n!\wedge(X-1)\geq 0)\quad\{Y\times X!=n!\wedge(X-1)\geq 0\}Y:=X\times Y;X:=X-1\{I\}\quad\models I\Rightarrow I}{\{I\wedge X>0\}Y:=X\times Y;X=X-1\{I\}}

于是根据 while 循环规则,有:

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

显然有

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

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

于是根据推论规则,有

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


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

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

# 霍尔规则的完备性

# 哥德尔不完备性定理

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

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

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

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

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

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

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

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

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

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

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

  • cCom,BAssn,Ic\in Com,B\in Assn,I 是解释,则 B 关于解释 I 对应于 c 的最弱前置条件wpI[c,B]wp^I[c,B](空心中括号)定义为:

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

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

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

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

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

    于是对所有的解释II,有

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

    AIA0IA^I\subseteq A_0^I。于是有

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

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

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


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

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

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

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

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

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

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

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

    证明:令m=(max{k,n0,...,nk})!,pi=1+(1+i)×mm=(max\{k,n_0,...,n_k\})!,p_i=1+(1+i)\times m,于是有pi,pjp_i,p_j 两两互质,因为pi,pjpip_i,p_j-p_i 是互质的(欧几里得辗转相减)。

    继续令ci=t=0kptpic_i=\frac{\prod_{t=0}^{k} p_t}{p_i}。显然cic_ipip_i 是互质的。(因为kk 个与pip_i 互质的数乘起来仍与pip_i 互质)因此存在唯一的cic_i 的乘法逆元did_i 使得

    ci×di1(mod  pi)c_i\times d_i\equiv 1(mod\; p_i)

    于是令n=i=0kci×di×nin=\sum_{i=0}^k c_i\times d_i\times n_i,就会有

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

    因为jij\neq i 时,cj×dj×nj  mod  pi=0c_j\times d_j\times n_j\;mod\;p_i=0。(cjc_jpip_i 的倍数)

    ci×di×ni  mod  pi=ni  mod  pic_i\times d_i\times n_i\;mod\;p_i=n_i\;mod\;p_i,所以nni(mod  pi)n\equiv n_i(mod\;p_i)


  • 定义谓词:

    F(x,y)x0&z0,[(x=2×zy=z)&(x=2×z1y=z)]x,y,zNF(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 为:

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

    说人话就是,若β±(n,m,j,x)\beta^\pm(n,m,j,x) 为真时,有:

    nj={x/2=n  mod  (1+(1+j)×m)x%2=0(x+1)/2=(n  mod  (1+(1+j)×n))x%2=1n_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 是可表达的

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

wpI[c,B]=w[c,B]Iwp^I[c,B]=w[c,B]^I

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

σIw[c,B]iffC[c]σIB\sigma\models^I w[c,B]\quad iff\quad \mathscr{C}[c]\sigma\models^I B

  • cskipc\equiv skip,此时取w[skip,B]Bw[skip,B]\equiv B。显然对所有的状态σ\sigma 和解释II

    σwpI[skip,B]iffC[skip]σIBiffσIBiffσIw[skip,B]\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]

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

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

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

  • cX:=ac\equiv X:=a,此时取w[X:=a,B]B[a/X]w[X:=a,B]\equiv B[a/X]。于是

    σwpI[X:=a,B]iffσ[A[a]σ/X]IBiffσIB[a/X]iffσIw[X:=a,B]\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]

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

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

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

  • cc0;c1c\equiv c_0;c_1,此时归纳定义取w[c,B]=w[c0,w[c1,B]]w[c,B]=w[c_0,w[c_1,B]]。对任意σ,I\sigma,I,有

    σwpI[c0;c1,B]iffC[c0;c1]σIBiffC[c1](C[c0](σ))IBiffC[c0]σIw[c1,B]iffσIw[c0,w[c1,B]]iffσIw[c0;c1,B]\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[c1,B]I=wpI[c1,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[c0,B]I=wpI[c0,B]w[c_0,B]^I=wp^I[c_0,B],以及最弱前置条件的定义。

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

  • cif  b  then  c0  else  c1c\equiv if\;b\;then\;c_0\;else\;c_1,归纳定义

    w[if  b  then  c0  else  c1,B][(bw[c0,B])(¬bw[c1,B])]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])]

    于是,对所有σ,I\sigma,I,有

    σwpI[c,B]iffC[c]σIBiff(B[b]σ=true&C[c0]σIB)  or  (C[b]σ=false&C[c1]σIB)iff(σIb&σwI[c0,B])  or  (σI¬b&σwI[c1,B])iffσI((bw[c0,B])(¬bw[c1,B]))iffσIw[c,B]\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 下C[b]σ=true\mathscr{C}[b]\sigma=true 当且仅当σIb\sigma\models^I b

    第四行是恒等变换,根据σIw[c0,B]σwI[c0,B]\sigma\models^I w[c_0,B]\Leftrightarrow \sigma\in w^I[c_0,B]

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

  • cwhile  b  do  c0c\equiv while\;b\;do\;c_0 太复杂了(略(看书


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

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

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

  • 定理,若{A}c{B}\models\{A\}c\{B\},则有{A}c{B}\vdash\{A\}c\{B\}

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

# 验证条件

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

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

    c::=skipX:=ac0;(X:=a)c0;{D}c1if  b  then  c0  else  c1while  b  do  {D}cc::=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

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

  • 考虑部分性断言:

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

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

    AD,D¬bBA\Rightarrow D,D\wedge\neg b\Rightarrow B

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

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

    vc({A}skip{B})={AB}vc({A}X:=a{B})={AB[a/X]}vc({A}c0;X:=a{B})=vc({A}c0{B[a/X]})vc({A}c0;{D}c1{B})=vc({A}c0{D})vc({D}c1{B})vc({A}if  b  then  c0  else  c1{B})=vc({Ab}c0{B})vc({A¬b}c1{B})vc({A}while  b  do  {D}c{B})=vc({Db}c{D}){AD}{D¬bB}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}\{A\}c\{B\} 是有效的,只需要证明vc({A}c{B})vc(\{A\}c\{B\}) 集合中每条断言都是有效的即可。

# 谓词转换器 *

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

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

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

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

  • 定义,设f:ΣΣf:\Sigma\rightarrow\Sigma_\perp 是状态的部分函数,定义:

    Wf:Pred(Σ)Pred(Σ)(Wf)(Q)=(f1Q){}即,(Wf)(Q)={σΣf(σ)Q}{}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 指称状态状态转换器:C[c]:ΣΣ\mathscr{C}[c]:\Sigma\rightarrow\Sigma_\perp,设 B 是一个断言,对应于解释 I 有:

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

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

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

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

# 不完备性和不可判定性

# 可计算性

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

    {c}(n)={σ(X1)σ=C[c]σ0[n/X1]undefinedC[c]σ0[n/X1]  is  undefined\{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}

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

    {c}(n1,...,nk)={σ(X1)σ=C[c]σ0[n1/X1,...,nk/Xk]undefinedC[c]σ0[n1/X1,...,nk/Xk]  is  undefined\{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+1f(n)=n+1,则有对应nf(n)=n+1={X1:=n+1}(n)n\longmapsto f(n)=n+1=\{X_1:=n+1\}(n)

    • 这是什么概念呢,根据我的理解,实际上意思就是抽象的数学函数的内容可以用 IMP 命令来描述。也就是 “借用了”X1X_1 存储单元,先把函数输入 n 存进去得到σ0[n/X1]\sigma_0[n/X_1],然后执行命令 c(相当于函数操作),然后再取出X1X_1 的值,得到函数的输出值。
  • 定义,称 IMP 命令 c 是整洁的当且仅当对所有的状态σ\sigma 和数nn,有

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

    根据我的理解,cc 执行后内容发生改变的存储单元只能有X1X_1

  • 命题,设c0,c1c_0,c_1 是命令,且c0c_0 是整洁的。对任意n,mNn,m\in N,有

    {c1}({c0}(n))=miff{c0;c1}(n)=m\{c_1\}(\{c_0\}(n))=m\quad iff\quad \{c_0;c_1\}(n)=m

    为什么要求c0c_0 是整洁的呢?因为c0c_0 是整洁的,所以{c0}(n)\{c_0\}(n) 取出X1X_1 的内容后,剩下的状态就正好是σ0[{c0}(n)/X1]\sigma_0[\{c_0\}(n)/X_1](其他单元格都没发生内容变化),正好符合了{c1}({c0}(n))\{c_1\}(\{c_0\}(n)) 外层要求的σ=C[c1]σ0[{c0}(n)/X1]\sigma=\mathscr{C}[c_1]\sigma_0[\{c_0\}(n)/X_1]

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

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

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

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

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

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

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

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

    很显然地,若命令 c 可以用来 “判定” 是否nMn\in M,那么命令:

    c;if  X1=1  then  skip  else  Divergec;if\;X_1=1\;then\;skip\;else\;Diverge

    (其中Diverge=while  true  do  skipDiverge=while\;true\;do\;skip)就可以用来 “检查” 是否nMn\in M

    所以可判定集合一定是可检查的。而且MM 是可判定的话,有Mˉ=NM\bar{M}=N-M 也是可判定的(命令最后加一个X1:=1X1X_1:=1-X_1)。

  • 反之,若c1c_1 可以用来检查 M,c2c_2 可以用来检查Mˉ\bar{M},则可以通过使c1,c2c_1,c_2 来构造命令cc,从而得到MM 的判定者:

    T,F,ST,F,S 是不属于Loc(c1)Loc(c2)Loc(c_1)\cup Loc(c_2) 的其他存储单元,把Loc(ci){Xi}Loc(c_i)-\{X_i\} 清零的赋值命令记为CleariClear_i,于是命令 c 为:

    T:=X1;T:=X_1;

    F:=0;F:=0;

    S:=1;S:=1;

    while  F=0  dowhile\;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;$
    

    Clear1;Clear2;T:=0;F:=0;S:=0;Clear_1;Clear_2;T:=0;F:=0;S:=0;

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

  • 定理,集合MM 是可判定的当且仅当MMMˉ\bar{M} 都是可检查的。

# 不可判定性

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

  • mkpairmkpair 是整数对的配对函数,譬如

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

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

    left(mkpair(n,m))=nright(mkpair(n,m))=mleft(mkpair(n,m))=n\\ right(mkpair(n,m))=m

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

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

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

    #(Xi)=mkloc(i)=mkpair(0,i)#(n)=mknum(n)=mkpair(1,n)#(a1+a2)=mksum(#a1,#a2)=mkpair(2,mkpair(#a1,#a2))\#(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 的标志对布尔表达式编码,例如

    #(a1a2)=mkpair(5,mkpair(#a1,#a2))\#(a_1\leq a_2)=mkpair(5,mkpair(\# a_1,\# a_2))

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

    #(Xi:=a)=mkpair(10,mkpair(#Xi,#a))#(if  b  then  c0  else  c1)=mkpair(12,mkpair(#b,mkpair(#c0,#c1)))\#(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) 也称为 c 的哥德尔数。我查到的是,任意一个命令的哥德尔数实际上就是

    enc(x1,x2,...,xn)=2x13x2...pnxnenc(x_1,x_2,...,x_n)=2^{x_1}3^{x_2}...p_n^{x_n}

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

  • 我们称ComCom 的一个子集SS 是可检查的(或可判定的),如果它们的编码集合

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

    是可检查的(或可判定的)。

  • 设 H 为 “自停(self-halting)” 命令集:

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

    Hˉ=ComH\bar{H}=Com-H

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

    证明:反设存在一个命令 C 来检查Hˉ\bar{H},有

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

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

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

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

    CHˉ{C}{#C}↓̸C\in\bar{H}\Rightarrow \{C\}\{\#C\}\not\downarrow

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

    推论HH 不是 IMP 可判定的。因为定理:集合MM 是可判定的当且仅当MMMˉ\bar{M} 都是可检查的。

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

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

# 哥德尔不完备性定理

如果存在一个能力足够强的定理证明系统,可以证明所有的 Assn 有效断言,那么我们就希望写一个这样的程序,当给定一个输入断言 A 的编码后该程序就毫无遗漏地取搜索 A 的证明,并且 halt 当且仅当找到了这样的一个证明。这个程序就是一个有效的检查者。

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

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

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

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


  • 定理ValidValid 是不可检查的。

证明:构造函数函数hh,满足对所有的命令cc

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

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

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

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

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

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

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

w[c,false][0/Loc(c)]σ,I,σIw[c,false][0/Loc(c)]σ,I,σ[0/Loc(c)]Iw[c,false]σ,C[c]σ[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

于是

AValidiffσ,C[c]σ[0/Loc(c)]=iff{C}(#A)iff{C}({W}(#c))iff{W;C}(#c)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

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

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

σ0={(X1,0),(X2,0),...,(Xn,0)}\sigma_0=\{(X_1,0),(X_2,0),...,(X_n,0)\}

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

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

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

实际上,就是要证明H0ˉ={cCom{c}(0)↓̸}\bar{H_0}=\{c\in Com|\{c\}(0)\not\downarrow\} 是不可检查的。

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

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

    cHˉiff{c}(#c)iff{X1:=#c;c}(0)iff(X1:=#c;c)H0ˉiff{C}(#(X1:=#c;c))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)=#(X1:=#c;c)\{W\}(\# c)=\#(X_1:=\#c;c)。(挺好构造的)于是

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

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


所以实际上,我们有:

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

实际上,还可以定义:

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

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