Revision | 软件科学基础

Posted on Edited on In

Abstract. 软件科学基础的复习笔记。

课程网站是 https://xiongyingfei.github.io/SF/2024/，参考资料是 Software Fundations 的 Vol. 1 和 Vol. 2。

Polymorphism and High-Order Functions

多态和隐式参数声明

如下两种方法可以定义多态的列表：

1
2
3
4
5
6
7
Inductive list (X : Type) : Type := 
  | nil
  | cons (x : X) (l : list X).

Inductive list : Type -> Type :=
  | nil : forall X : Type, list X 
  | cons : forall X : X -> list X -> list X.

将 (X : Type) 直接写在 type constructor 相当于是要求在每一个 data constructor 前面都加上 (X : Type)。

用如下的方法可以将 X 声明为 nil 的隐式参数：

1
2
3
4
5
6
7
8
9
Arguments nil {X}

Inductive list' {X : Type} : Type :=
  | nil'
  | cons' (x : X) (l : list')
  
Inductive list' : Type -> Type :=
  | nil' {X : Type} : list' X
  | cons' {X : Type} (x : X) (l : list') : list' X

这样一来在推不出来 nil 类型的时候和强行给 nil 传参的时候会报错：

1
2
Fail Definition mynil := nil.
Fail Definition mynil := nil nat.

但是可以通过手动标注类型或者使用 @ 来临时禁用隐式参数：

1
2
Definition mynil : list nat :=  nil.
Definition mynil := @nil nat.

这里有一个很重要的东西是，X 不一定要是一个 Type，还可以是 nat，比如说下面这个东西定义了固定长度的列表。此时的 list n 称为一个 dependent type，它是 nat 和 nat -> Type 的 generalised sum type 的一个元素。

1
2
3
Inductive list : nat -> Type :=
  | nil : list 0
  | cons (n : nat) (l : list n) : list (S n)

回忆我们在学 Agda 的 Internal Verification 的时候[1]，有如下的定义：

1
2
data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  _,_ : (a : A) → (b : B a) → Σ A B

用这个东西来解释的话，就是 list n = ( n , list ) ∈ Σ nat list

Lambda Calculus, Church Numeral

一个 Lambda 表达式的语法如下：

$$
\begin{align}
t :=~ & x & \text{variable} \\
& \lambda x. t & \text{abstraction} \\
& t~ t & \text{application}
\end{align}
$$

只有下面两种推导规则：

  • Alpha Renaming 将变量改名。$\lambda x. x$ 可以改成 $\lambda y.y$ 实际上改名规则有点复杂，这里不写。
  • Beta Reduction 函数调用。$(\lambda x. t_1) ~t_2 \longrightarrow [x\mapsto t_2] t_1$

可以写出 Bool 类值的 Lambda 表达式（Church Boolean）

$$
\begin{align}
tru &= \lambda t. \lambda f. t \\
fls &= \lambda t. \lambda f. f
\end{align}
$$

这里两个参数的意思是你要将构造子作为参数传进来。同时下面的函数的功能是求两个 Church Boolean 的与：

$$
and = \lambda b. \lambda c. b~c~fls
$$

这里 $c$ 和 $fls$ 作为参数传给了 $b$，当 $b$ 为 true 时返回 $c$，否则将返回 $fls$。

可以写出自然数的 Church Numerals。

$$
\begin{align}
c_0 &= \lambda s. \lambda z. z \\
c_1 &= \lambda s. \lambda z. s ~ z \\
c_2 &= \lambda s. \lambda z. s (s ~ z) \\
\cdots \\
scc &= \lambda n. \lambda s. \lambda z. s (n~s~z)
\end{align}
$$

在 Coq 中我们可以翻译成如下的代码：

1
2
3
4
Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition zero : cnat := fun (X : Type) (f : X -> X) (x : X) => x.
Definition scc (n : cnat) : cnat := 
  fun (X : Type) (f : X -> X) (x : X) => f (n X f x)

接下来我们来定义各种运算。

1
2
3
4
5
Definition plus (n m : cnat) : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).

Definition mult (n m : cnat) : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => n X (m X f) x.

定义指数运算稍微有一点棘手，这里你需要注意到传给 Church Numeral 的类型不一定非要是 X。

1
2
3
Definition exp (n m : cnat) : cnat :=
  fun (X : Type) (f : X -> X) (x : X) =>
    m (X -> X) (fun g : (X -> X) => n X g) f x.

下面的 Y Combinator 用于在 Lambda Calculus 中实现递归

$$
Y = \lambda f. (\lambda x. f~(x~x)) (\lambda x. f~(x~x))
$$

简单计算一下发现

$$
\begin{align}
Y~f &= (\lambda x. f~(x~x)) (\lambda x. f~(x~x)) \\
&= f~((\lambda x. f~(x~x))~(\lambda x. f~(x~x))) \\
&= f~(Y~f)
\end{align}
$$

The Curry-Howard Correspondence, Inductively Defined Propositions

指的是命题对应类型，证明对应值的同构关系。具体地有下表：

Logic side Programming side
universal quantification generalised product type
existential quantification generalised sum type
implication function type
conjunction product type
disjunction sum type
true formula unit type
false formula bottom type

在 Coq 中，对于一个定理

1
2
3
4
Theorem name : content.
Proof.
  (* your proof *)
Qed.

这里 Theorem 实际上是 Definition 的一个别名，content 是这里的 name 的类型，Proof 和 Qed 之间的东西实际上是在构造这个类型的一个值，这个值称为该定理的一个 Proof Object。

因为 Coq 里面的证明风格很命令式，所以这里你可能不能直观地感受到这个 Curry Howard Correspondence。而在 Agda 里面这个则更明显一点。

Coq 中，诸逻辑用语的定义实际上如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Inductive and (P Q : Prop) : Prop :=
  | conj : P -> Q -> and P Q.

Inductive or (P Q : Prop) : Prop :=
  | or_introl : P -> or P Q
  | or_intror : Q -> or P Q.

Inductive ex {A : Type} (P : A -> Prop) : Prop :=
  | ex_intros : forall x : A, P x -> ex P
  where "'exists' x , p" := (ex (fun x => p)).

Inductive True : Prop :=
  | I : True.

Inductive False : Prop := .

Inductive eq {X : Type} (x : X) : X -> Prop :=
  | eq_refl : eq x x.

我们以 or 和 exists 为例简单说一下这个东西怎么解析。

  • 我们之前已经提到了直接在 type constructor 后面加的 (P Q : Prop) 意思是每一个 data constructor 都需要带上这两个参数。
  • 那么这里的 or_introl 这个 data constructor 实际上意思是，传入两个类型 P, Q（命题 $P, Q$），并传入一个 P 类型的值（命题 $P$ 的证明）就可以得到一个 or P Q 类型的值（$P\vee Q$ 的证明）。or_intror 同理。

对于 exists，这里面有一个 forall 可能不是很好理解，但是

  • 我们之前提到了 ex_intros : forall x : A, P x -> ex P 这个写法等价于 ex_intros (x : A) : P x -> ex P。
  • 那么这里的 ex_intros 读入一个 A -> Prop 函数 P（一个谓词 $P$），一个 A 类型的 x（论域中的一个具体值 $x$），一个 P x 类型的值（命题 $P~x$ 的一个证明），就可以得到一个 exists x, P x 类型的值（$\exists x, P~x$ 的证明）

这一段话不一定对

forall 的本质是什么？

从上面的表格当中我们看到 forall 在 Programming Side 对应的是 generalised producted type。下面我们来解释一下 generalised producted type 是什么东西。对于人类来说 sum type 和 product type 都是理解的，前者是可以具有成分类型中任何一种，后者是一个 tuple。

我们还是考虑第一节中提到的 generalised sigma type，也就是 exists。在 Agda 下的代码为

1
2
data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  _,_ : (a : A) → (b : B a) → Σ A B

sum type 即表示任意一个单独的 a , b 都是 Σ A B 的一个值（$\exists x\in A, B~x$ 的一个证明）。

而 product 的意思是，这里你必须给出一个大小为 $\mathrm{card}(A)$ 的 tuple：

$$
((x_0, B~x_0), (x_1, B~x_1), …) \in \Pi(A, B)
$$

那么由于集合中元素都是互异的，这里你想要在程序中写出这个 tuple 一个可操作的方法是写一个单射
$$
\begin{align}
\begin{matrix}
f : & A & \rightarrow & \mathrm{Prop} \\
& x & \mapsto & y\color{red}{\in B (x)}
\end{matrix}
\end{align}
$$

你发现我们这里怎么也没法用正常的映射写法精确的描述这个函数的类型，所以我在 mapsto 后面加上了红色的类型。这个函数在类型论里面叫做 Dependent Function Type，就是直接定义成这样子的，跳过了中间经过 tuple 的思考。

这就表明 forall 修饰的命题的 Proof Object 应当形如

1
fun x : A => ... (* which should have type `B x` *)

于是根据 Functional Extensionality Axiom 可以知道下面两个定义等价：

1
2
constructor (x : A) : something
constructor : forall x : A, something

于是，常见的 Tactics 本质上是：

  • split. 本质上是增加一个 conj，并将要传入的两个参数作为两个 Goal。
  • destruct. 本质上是添加一个 match 来匹配所有的构造子。
  • apply. 声称结果必然是某一个函数的输出，转而寻找一个输入使得输出具有该类型。

一些常见的结论的本质是：

  • ex_falso 一个空的 match 的返回值可以被推导出任何类型。

可以用 Inductive 定义一系列命题。下面定义的东西是一个经典的命题：

1
2
3
Inductive ev : nat-> Prop :=
  | ev_0 : ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).

不妨自行用上面的 Curry Howard Correspondence 来解释这两个 data constructor 是什么意思，这里不赘述。

现在我们考虑定义结构归纳法的命题，并写出其 Proof Object。这里本质上是你的 Proof Object 中可以有递归函数（fix）。

对于 Inductive Type 的递归，作为例子我们考虑下面的Peano 自然数递归，其应当具有类型：

1
2
3
4
5
Definition nat_ind_type : Type :=
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.

这个 ind_type 生成的方法是，对于每一个 data constructor，都给定从参数上谓词 $P$ 成立推导构造之后谓词 $P$ 成立。

显然下面的东西是一个具有该类型的值：

1
2
3
4
5
6
7
8
9
Definition nat_ind : nat_ind_type :=
  fun (P : nat -> Prop) => 
    fun P0 : (P 0) =>
      fun PS : (forall n : nat, P n -> P (S n)) =>
        fix f (n : nat) =>
          match n with
          | 0 => P0
          | S n' => PS n (f n')
          end.

因此我们证明了整数的结构归纳法是对的。

对于 inductively defined propositions，如果直接套用上面的归纳类型定义方式，这里 P 的类型就应当类似于

1
P : IndProp -> Prop

这是一个关于证明（注意 P 的输入是一个 IndProp 类型的值，即一个证明）的谓词。但实际上你根本不用在乎证明满足什么性质，只要证出来就好了，所以 inductive propositions 的归纳类型是用下面的方法单独定义的。

对于 inductive propositions 的结构归纳法，我们是希望辅助推导这样的结论：

1
2
forall P : Arg -> Prop,                  (* 1 *)
  forall arg : Arg, IndProp arg -> P arg (* 2 *)

不妨假设 IndProp 有几个构造子

1
2
3
Inductive IndProp : Arg -> Prop :=
  | Constructor1 (arg1 : Arg1) : IndProp (SomeF1 arg1) -> IndProp (SomeF arg2)
  | ...

这里的 Arg1 是某个类型，SomeF 是某个 Arg1 -> Arg 的函数，那么你需要在 (* 1 *) 和 (* 2 *) 之间加上：

1
forall arg1 : Arg1, IndProp (SomeF1 arg1) -> P (SomeF1 arg1) -> P (SomeF2 arg1)

言下之意就是，在 (* 2 *) 中你希望证明的这个蕴含关系的前提的证明是由 arg1 这些参数用某种方式组合（SomeF2），用 Constructor1 这个构造子构造出来的，并且 IndProp -> P 在子结构上也成立（IndProp (SomeF1 arg1)），那么 P 必须要在 SomeF2 这种组合上面成立。

以 ev 为例，其定义为

1
2
3
Inductive ev : nat -> Prop :=
  | ev_0 : ev 0
  | ev_SS forall n : nat, ev n -> ev (S (S n)).

于是 ev_ind 希望辅助推导 forall n : nat, ev n -> P n，其类型应当是：

1
2
3
forall P : nat -> Prop,
  (* insert something *)
  forall n : nat, ev n -> P n

观察 ev 的两个构造子的形状，可以发现在 (* insert something *) 的部分插入合适的东西之后应该得到：

1
2
3
4
forall P : nat -> Prop,
  P 0 ->
  (forall n : nat, ev n -> P n -> P (S (S n))) ->
  forall n : nat, ev n -> P n

另一个比较有意思的东西是 eq_ind。考虑 eq 的定义 

1
2
Inductive eq (X : Type) (n : X) : X -> Prop :=
  | eq_refl : eq n n

按照上面的推法应该写出

1
2
3
Definition eq_ind_type : Type :=
  forall (X : Type) (n : X) (X -> Prop),
    P n -> (forall m, n = m -> P m)

这给出了 rewrite 的本质：rewrite n m 时，把除了 $m$ 以外的地方都看成谓词 P 的表达式。

接下来是经典的三个问题。

  • 什么时候我们会输入命题，输出命题？

    考虑一些作用到 Prop 上的 type constructor。比如说 or 就是读入两个命题，生成一个命题。

  • 什么时候我们会输入证明，输出证明？

    考虑经典的 data contructor ev_SS，就是输入了 ev n 的证明然后输出了 ev (S (S n)) 的证明。

  • 什么时候我们会输入命题，输出证明？

    考虑那几个将命题作为显式参数输入的命题逻辑公式，比如 

    1
    2
    Definition and_comm (P Q : Prop) : (P /\ Q) -> (Q /\ P)
      := (* omitted. *).

注意 coq 屏蔽了输入一个证明，输出一个命题。Informally 这是因为我们得到的结论不应当随着证明的方法变化而变化。

Simple Imperative Programs

我们定义了一个简单的命令式语言 IMP。这个语言没有很严格的类型系统，包含以下要素：

  • 自然数和布尔值，算数和逻辑运算。
  • 变量（英文大写字母），赋值（Assign），包含一个内存池（用一个 Total Map 表出，称为状态）。
  • 基本的程序结构：顺序执行（Seq），条件（If），循环（While）

为了节约篇幅我们这里并不写出这种语言的 BNF，你可以根据下面的语义定义自动补全一下。

考虑如何建模语义。一个直观的想法是建模成函数，比如说定义：

1
2
3
4
5
6
Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus a1 a2 => (aeval a1) + (aeval a2)
  | AMinus a1 a2 => (aeval a1) - (aeval a2)
  | AMult a1 a2 => (aeval a1) * (aeval a2)

或者建模成关系，比如定义 

1
2
3
Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n : nat) : aeval (ANum n) n 
  | ...

表示一个 aexp 求值之后得到 $n$。在最顶层，我们定义了一个关系 st =[ prog ]=> st' 表示对状态 st 执行程序 prog 之后得到 st'。抽象地，有如下几条推导规则：

$$
\begin{matrix}
\dfrac{}{\texttt{st =[ skip ]=> st}} & \color{blue}{\text{(E_Skip)}} \\
\\
\dfrac{\texttt{aeval st a = n}}{\texttt{st =[ x := a ]=> (x !-> a ; st)}} & \color{blue}{\text{(E_Ass)}} \\
\\
\dfrac{\texttt{st =[ c1 ]=> st1}\quad\texttt{st1 =[ c2 ]=> st2}}{\texttt{st =[ c1 ; c2 ]=> st2}} & \color{blue}{\text{(E_Seq)}} \\
\\
\dfrac{\begin{matrix}
\texttt{beval st b = true} \\
\texttt{st =[ c1 ]=> st’}
\end{matrix}}{\texttt{st =[ if b then c1 else c2 ]=> st’}} & \color{blue}{\text{(E_IfTrue)}}\\
\\
\dfrac{\begin{matrix}
\texttt{beval st b = false} \\
\texttt{st =[ c2 ]=> st’}
\end{matrix}}{\texttt{st =[ if b then c1 else c2 ]=> st’}} & \color{blue}{\text{(E_IfFalse)}} \\
\\
\dfrac{\begin{matrix}
\texttt{beval st b = true} \\
\texttt{st =[ c ]=> st’} \\
\texttt{st’ =[ while b do c end ]=> st’’}
\end{matrix}}{\texttt{st =[ while b do c end ]=> st’’}} & \color{blue}{\text{(E_WhileTrue)}} \\
\\
\dfrac{\texttt{beval st b = false}}{\texttt{st =[ while b do c ]=> st}} & \color{blue}{\text{(E_WhileFalse)}}
\end{matrix}
$$

Automation

除了各种 exxx 之外可以采用如下的方式来智能化地证明：

1
2
3
4
5
6
7
Ltac find_rwd :=
  match goal with
    H0: ?P ?E,
    H1: forall x, ?P x-> ?E = ?R,
    H2: ?P ?X
  |- _ => rewrite (H1 X H2)
 end.

这里 ?P 可以匹配某一个谓词，?E 可以匹配某个式子，在你加的分支足够多的时候是可以匹配上唯一的前提的。|- 匹配要证明的式子，=> 后面是执行的操作。

Hoare Logic

Hoare Logic 用 Hoare 三元组来描述程序的性质，$\{P\} c \{Q\}$ 表示一开始 $P$ 成立，执行 $c$ 之后 $Q$ 成立。

Hoare Logic 的规则如下

$$
\begin{matrix}
\dfrac{}{\{P\} \texttt{skip} \{P\}} & \color{blue}{\text{(Skip)}} \\
\\
\dfrac{}{\{[a/x] P\} \texttt{x := a} \{P\}} & \color{blue}{\text{(Assign)}} \\
\\
\dfrac{\{P\} \texttt{c1} \{R\}\quad \{R\} \texttt{c2} \{Q\}}{\{P\} \texttt{c1; c2} \{Q\}} & \color{blue}{\text{(Seq)}} \\
\\
\dfrac{\{P \wedge b\} \texttt{c1} \{Q\} \quad \{P \wedge\neg b\} \texttt{c2} \{Q\}}{\{P\} \texttt{if b then c1 else c2} \{Q\}} & \color{blue}{\text{(If)}} \\
\\
\dfrac{P_1\rightarrow P_2\quad Q_2\rightarrow Q_1\quad \{P_2\} \texttt{c} \{Q_2\}}{\{P_1\} \texttt{c} \{Q_1\}} & \color{blue}{\text{(Consequence)}} \\
\\
\dfrac{\{P \wedge b\} \texttt{c} \{P\}}{\{P\} \texttt{while b do c end} \{P \wedge \neg b\}} & \color{blue}{\text{(While)}}
\end{matrix}
$$

注意 Asgn 的写法是在前提中置换，所以说下面这个 Hoare triple 是不合法的：

$$
\{ True \} \texttt{ X := a } \{ X = a \}
$$

反例是 $a = X + 1$。

注意在 If 当中 $b$ 是一个 bool 值，前件中的 $b$ 是从 bool 值提升来的命题（成立若 $b$ 为 true）。

在模型论的观点下研究 Hoare Logic 的语义，考虑用上文定义的 IMP，将几条规则证明成定理。

在 Coq 当中定义 Hoare triple $P, Q$ 是关于状态的命题，也就是

1
2
3
4
5
6
7
Definition Assertion := state -> Prop

Definition assert_implies (P Q : Assertion) : Prop :=
  forall st, P st -> Q st

Notation "P ->> Q" := (assert_implies P Q)
                     (at level 80) : hoare_spec_scope.

那么可以用 IMP 用关系建模的语义来定义合法的 Hoare triple：

1
2
3
4
5
6
7
Definition valid_hoare_triple (P : Assertion) (c : com) (Q : Assertion) : Prop :=
  forall st st',
    st =[ c ]=> st' -> P st -> Q st

Notation "{{ P }} c {{ Q }}" :=
  (valid_hoare_triple P c Q) (at level 90, c custom com at level 99)
  : hoare_spec_scope.

然后容易验证所有的 Hoare Logic 规则都成立。

此外可以证明死循环可以推出任何后条件。这称为 Hoare Logic 的部分正确性，即允许写错误的代码，如果写了死循环那么可以推出任何条件。

如果在语言中加入下面的语句，也可以写出对应的 Hoare 规则：

  • if b then c 相当于 if b then c else skip，不需要额外的规则。

  • repeat c until b 相当于 c; while !b do c，不需要额外的规则。

  • assume b

    $$
    \dfrac{\texttt{beval st b = true}}{ \texttt{st =[ assume b ]=> st} }
    $$

    这句话的意思是在 $b$ 为真的时候 assume b 等价于 skip，其余时候程序会卡在这一句不能往后执行（stuck），行为上相当于 while true，能够推出任何后条件。其 Hoare 规则为

    $$
    \dfrac{}{\{P\} \texttt{assume b} \{P\wedge b\}}
    $$

  • assert b 当 $b$ 不成立时，程序崩溃（crash / error），在一个 error 的状态上不能得到任何结论。其 Hoare 规则为

    $$
    \dfrac{}{\{P \wedge b\} \texttt{assert b} \{P \wedge b\}}
    $$

现在可以通过霍尔规则，用称为 Decorated Program 的风格推导大段程序的正确性。

比如要推导

1
2
3
4
5
  {{ X <= 3 }}
while X <= 2 do
  X := X + 1
end
  {{ X = 3 }}

其 Decorated Program 如下：

1
2
3
4
5
6
7
8
9
  {{ X <= 3 }}
while X <= 2 do
    {{ X <= 3 /\ X <= 2 }} ->>
    {{ X + 1 <= 3 }}
  X := X + 1
    {{ X <= 3 }}
end
  {{ X <= 3 /\ ~(X <= 2) }} ->>
  {{ X = 3 }}

将 Hoare 规则改成 Decorated Program，有

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
// Skip
{{ P }} skip {{ P }}

// Seq
{{ P }} c1; {{ R }} c2 {{ Q }}

// Consequence
{{ P }} ->> {{ P' }}

// Assign
{{ P [X |-> a] }}
  X := a 
{{ P }}

// If
{{ P }}
if b then 
  {{ P /\ b }}
  c1
  {{ Q }}
else 
  {{ P /\ ~b }}
  c2
  {{ Q }}
end
{{ Q }}

// While
{{ P }}
while b do
  {{ P /\ b }}
  c 
  {{ P }}
end
{{ P /\ ~b }}

一个困难的点是，如何获得 while 的循环不变式 $P$。PPT 上面的例子都比较显然，只需要把变量之间的关系往上套就行了。

Definition（最弱前条件）. $P$ 是 $\texttt{c}\{Q\}$ 的最弱前条件若

  1. $\{P\} \texttt{c} \{Q\}$
  2. $\forall P’. \{P’\} \texttt{c} \{Q\} \rightarrow (P’ \rightarrow P)$

记为 $wp(c, Q)$。

Definition（最强后条件）. $Q$ 是 $\{P\}\texttt{c}$ 的最弱前条件若

  1. $\{P\} \texttt{c} \{Q\}$
  2. $\forall Q’. \{P\} \texttt{c} \{Q’\} \rightarrow (Q \rightarrow Q’)$

记为 $sp(P, c)$。

sp 和 wp 都可以递归地计算，但是式子略微复杂，所以我不想写。wp 有一个很精妙的构造（注意前条件是一个 Assertion，即 state -> Prop）：

$$
wp(c, Q) = \lambda st. \forall st’, \texttt{st =[ c ]=> st’} \rightarrow Q~st’
$$

还有一个我上课想到的不一定正确的 sp 的构造（imformally 可以证明是对的）

$$
sp(c, Q) = \lambda st’. \exists st, \texttt{st =[ c ]=> st’} \wedge P~st
$$

可以证明一个重要的 Hoare triple

$$
\{wp(\texttt{while b do c endl}, Q) \wedge b\} \texttt{c} \{wp(\texttt{while b do c endl}, Q)\}
$$

也就是说最弱前条件是循环不变式。

现在我们将 Hoare Logic 看作一个形式系统，验证其

  1. Soundness，在 IMP 模型下，Hoare Logic 是正确的。（这里前面已经证明了）
  2. Completeness，所有在 IMP 模型下的 valide hoare triple 都可以被 Hoare 规则推出。

唯一的难点是 Seq 和 While 的证明。这里我们均可以用 wp 作为中间条件。比如说对于 While，你可以先证明

$$
\{wp(\texttt{while b do c end}, Q)\} \texttt{while b do c end} \{Q\}
$$

这里用到了重要的 Hoare triple $(26)$。然后根据最弱前条件的定义和 Hoare Consequence 得证。

可以证明 Hoare Logic 是不可判定的。因为停机问题可以规约到 Hoare triple 的判定：

$$
\{\mathrm{True}\} \texttt{c} \{\mathrm{False}\}
$$

Small-Step Operational Semantics

小步法语义，简而言之就是对于程序的 AST，每次选择中序遍历的第一个叶子进行 evaluate。语义建模成关系，称为

$$
x / st \longrightarrow y / st’
$$

意为程序 $x$，变量的状态为 $st$ 展开一步得到 $y$，变量状态为 $st’$。比如说对于

$$
\texttt{if b then c1 else c2}
$$

重复执行 $\longrightarrow$ 的过程中，我们将首先一直对 $b$ 进行单步地求值（每次算一次运算的结果）直到它变成 true 或者 false，此时中序遍历到的第一个节点就是根。然后如果是 true，那么根将被化为 $\texttt{c1}$，反之同理。IMP 的小步法语义形式化定义如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
Inductive cstep : (com * state) -> (com * state) -> Prop :=
  | CS_AsgnStep : forall st i a1 a1',
      a1 / st -->a a1' ->
      <{ i := a1 }> / st --> <{ i := a1' }> / st
  | CS_Asgn : forall st i (n : nat),
      <{ i := n }> / st --> <{ skip }> / (i !-> n ; st)
  | CS_SeqStep : forall st c1 c1' st' c2,
      c1 / st --> c1' / st' ->
      <{ c1 ; c2 }> / st --> <{ c1' ; c2 }> / st'
  | CS_SeqFinish : forall st c2,
      <{ skip ; c2 }> / st --> c2 / st
  | CS_IfStep : forall st b1 b1' c1 c2,
      b1 / st -->b b1' ->
      <{ if b1 then c1 else c2 end }> / st
      -->
      <{ if b1' then c1 else c2 end }> / st
  | CS_IfTrue : forall st c1 c2,
      <{ if true then c1 else c2 end }> / st --> c1 / st
  | CS_IfFalse : forall st c1 c2,
      <{ if false then c1 else c2 end }> / st --> c2 / st
  | CS_While : forall st b1 c1,
      <{ while b1 do c1 end }> / st
      -->
      <{ if b1 then c1; while b1 do c1 end else skip end }> / st

  where " t '/' st '-->' t' '/' st' " := (cstep (t,st) (t',st')).

这里我们省略了 -->a 和 -->b 之类的东西，这两个东西意思是对一个 nat 表达式或者一个 bool 表达式单步展开。

在此基础上定义任意多步执行的关系

$$
st \longrightarrow_* st’
$$

有

$$
\begin{matrix}
\dfrac{}{st\longrightarrow_* st} & \color{blue}{\text{(multi-refl)}} \\
\\
\dfrac{st \longrightarrow st_1\quad st_1{\longrightarrow_*} st_2}{st{\longrightarrow_*} st_2} & \color{blue}{\text{(multi-step)}}
\end{matrix}
$$

在小步法语义中我们主要关注三个性质：

  • determinstic $(x \longrightarrow y \wedge x \longrightarrow z) \rightarrow y = z$。
  • strong progress $\forall x, \mathrm{value}(x) \vee (\exists y, x\longrightarrow y)$。
  • normal form $~\exists t, x \longrightarrow t$。可以证明 $\mathrm{normal~form} = \mathrm{value}$。
  • normalizing $\forall t, \exists t’, t {\longrightarrow_*}t’ \wedge \mathrm{normalform}(t’)$

上面三个性质是好的，我们总是希望我们的编程语言有上面的性质。但是一般的语言总是存在卡住的项，比如说你在 if 的判断条件里面加入了不是 Bool 的东西。因此我们引入 Type system 来防止这一点。

定义

$$
\vdash v \in T
$$

表示在类型系统下 $v$ 具有类型 $T$。

然后可以定义一系列推导规则，这个不是很重要。仅以 if 为例，我们定义

$$
\begin{matrix}
\dfrac{\vdash a \in \texttt{Bool}\quad \vdash b\in T \quad \vdash c \in T}{\vdash \texttt{if a then b else c end}\in T} & \color{blue}{\text{(T_if)}}
\end{matrix}
$$

之后我们可以将 strong progress 改为 progress：

$$
\forall t~T, \vdash t\in T \rightarrow \mathrm{value}(t)\vee \exists t’, t\longrightarrow t’
$$

并且有一个新的性质是 preservation：

$$
\forall t~t’~T, \vdash t\in T \rightarrow t\longrightarrow t’\rightarrow \vdash t\in T’
$$

Simply Typed Lambda Calculus

我们定义 STLC 表达式的语法：

$$
\begin{aligned}
t =~ & \texttt{$x$} & \color{blue}{\text{(variable)}} \\
& \texttt{$\lambda x$ : $T$, }t & \color{blue}{\text{(abstraction)}} \\
& \textit{t t} & \color{blue}{\text{(application)}} \\
& \mathtt{true} & \color{blue}{\text{(constant)}} \\
& \mathtt{false} & \color{blue}{\text{(constant)}} \\
& \texttt{if $t$ then $t$ else $t$} & \color{blue}{\text{(conditional)}} \\
T =~ & \texttt{Bool} \\
& T \rightarrow T
\end{aligned}
$$

可以用小步法定义 STLC 的语义。注意现在的 STLC 是一种纯函数式语言，所以在小步法定义的时候不会带上一个 $st$ 作为状态。视常量和裸露的 abstraction 为 value。那么规则如下：

$$
\begin{matrix}
\dfrac{\mathrm{value}(v_2)}{(\lambda x : T_2, t_1)~ v_2 \longrightarrow [x := v_2] t_1}& \color{blue}{\text{(ST_AppAbs)}} \\
\\
\dfrac{t_1 \longrightarrow t_1’}{t_1~t_2 \longrightarrow t_1’~t_2} & \color{blue}{\text{(ST_App1)}}
\\
\dfrac{t_2 \longrightarrow t_2’}{t_1~t_2 \longrightarrow t_1~t_2’} & \color{blue}{\text{(ST_App2)}} \\
\\
\dfrac{t_1 \longrightarrow t_2}{\texttt{if $t_1$ then $t_2$ else $t_3$}\longrightarrow \texttt{if $t_1’$ then $t_2$ else $t_3$}} & \color{blue}{\text{(ST_If)}} \\
\\
\dfrac{}{\texttt{if true then $t_2$ else $t_3$}\longrightarrow t_2} & \color{blue}{\text{(ST_IfTrue)}}\\
\\
\dfrac{}{\texttt{if false then $t_2$ else $t_3$}\longrightarrow t_3} & \color{blue}{\text{(ST_IfFalse)}}\\
\end{matrix}
$$

上面涉及到了 $[x := v_2]$ 这样的改名操作。这个操作的意义是将所有的自由变量 $x$ 修改为 $v_2$。举例来说

$$
[x := y](\lambda x, x) = \lambda x, x
$$

这是因为 $x$ 在此处是约束变量。

这里并不涉及 Alpha Renaming，因为在 Coq 里面太难实现。因此需要注意，这样的一条规则和上面的语法是不相容的：

$$
\begin{matrix}
\dfrac{t_1\longrightarrow t_1’}{\lambda x : T, t_1 \longrightarrow \lambda x : T, t_2} & \color{gray}{\text{(ST_Abs)}}
\end{matrix}
$$

如果加上你就可以得到

$$
\lambda y : \texttt{Bool}, ((\lambda x : \texttt{Bool}, (\lambda y : \texttt{Bool}, x)), y) \longrightarrow \lambda y : \texttt{Bool}, (\lambda y, y)
$$

而在原来的系统里面，这东西按照 Functional Extensionality，行为上相当于

$$
\lambda y : \texttt{Bool}, (\lambda z : \texttt{Bool}, y)
$$

到现在为止你的表达式还是可以随便乱写的，因此需要加上类型系统。

$$
\Gamma \vdash t\in T
$$

表示在上下文 $\Gamma$（用一个从变量名到类型的映射给出，表示变量名 $x$ 具有类型 $\Gamma x$，$\varepsilon$ 为空映射）下，表达式 $t$ 具有类型 $t$。

$$
\begin{matrix}
\dfrac{\Gamma x = T_1}{\Gamma \vdash x \in T_1} & \color{blue}{\text{(T_Var)}} \\
\dfrac{x \mapsto t_2; \Gamma \vdash t_1\in T_1}{\Gamma \vdash \lambda x : T_2, T_1 \in T_2\rightarrow T_1} & \color{blue}{\text{(T_Abs)}} \\
\\
\dfrac{\Gamma \vdash t_1 \in T_2\rightarrow T_1\quad \Gamma\vdash t_2\in T_2}{\Gamma \vdash t_1~t_2\in T_1} & \color{blue}{\text{(T_App)}} \\
\\
\dfrac{}{\Gamma \vdash \texttt{true} \in \texttt{Bool}} & \color{blue}{\text{(T_True)}} \\
\\
\dfrac{}{\Gamma \vdash \texttt{false} \in \texttt{Bool}} & \color{blue}{\text{(T_False)}} \\
\\
\dfrac{\Gamma\vdash t_1 \in \texttt{Bool}\quad \Gamma\vdash t_2 \in T_1\quad \Gamma \vdash t_3\in T_1}{\Gamma \vdash \texttt{if $t_1$ then $t_2$ else $t_3$ end} \in T_1 } & \color{blue}{\text{(T_If)}}
\end{matrix}
$$

可以证明 STLC 有如下性质：

Progress

$$
\forall t~T, \varepsilon \vdash t \in T \rightarrow (\mathrm{value}(t) \vee \exists t’, t\longrightarrow t’)
$$

Weakening

$$
\forall \Gamma~t~T, \varepsilon \vdash t\in T \rightarrow \Gamma \vdash t \in T
$$

这里前件蕴含着 $t$ 里面没有自由变元。

Substitution preserves typing

$$
\forall \Gamma~x~U~t~v~T, x\mapsto U; \Gamma \vdash t\in T \rightarrow \varepsilon \vdash v\in U \rightarrow \Gamma\vdash [x:=v]t\in T
$$

Preservation

$$
\forall t~t’~T, \varepsilon \vdash t\in T \rightarrow t\longrightarrow t’ \rightarrow \varepsilon \vdash t’\in T
$$

Unique Type

$$
\forall \Gamma~t~T~T’, \Gamma \vdash t \in T\rightarrow\Gamma \vdash t\in T’\rightarrow T=T’
$$

这个性质重要度实际上不高，因为后面引入子类之后就失效了。但是在这里还是可以说明表达式到 Type 有函数关系。

此外可以向语言中添加 nat，let … in …，Pairs，Unit，Sums，Lists，Fix，Records 等成分。

这里直接将 fix 的行为定义出来的原因是 fix 的类型是无穷阶的递归类型，在 STLC 中无法写出。

经典的操作是用 fix 写递归：

1
2
3
4
5
fact = \self : Nat -> Nat,
  \x : Nat,
    if x = 0 then 1 else x * (self (pred x))

fix fact

在小步法求值的过程中，我们顺次展开 fix 和带入 n，以求 3 的阶乘为例

1
2
3
4
5
6
7
8
9
10
11
  fix fact 3
--> 
  fact (fix fact) 3
--> 
  \x : Nat, if x = 0 then 1 else x * (fix fact) (pred x) 3
-->
  if 3 = 0 then 1 else 3 * (fix fact) 2
--> 
  3 * (fix fact) 2
--> 
  ......

$(49)$ 指出程序到类型之间存在函数关系，因此我们可以写出一个 Typechecker。由于类型检查可以失败，所以说我们最好用 Maybe Monad 写一个 Monadic Typechecker

在 Coq 中写 

1
2
3
4
5
6
7
8
9
Notation " x <- e1 ;; e2" := (match e1 with
                              | Some x => e2
                              | None => None
                              end)
                             (right associativity, at level 60).
Notation " 'return' e "
  := (Some e) (at level 60).
Notation " 'fail' "
  := None.

回忆在 Haskell 里面

1
2
e1 >>= (\x -> e2) = do x <- e1
                       e2

其中在 Maybe Monad 里面有 

1
2
3
4
5
6
return :: a -> m a 
return = pure

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b 
Nothing >>= _ = Nothing
(Just x) >>= f = f x

和上面的定义是极其类似的。

那么以 Pair 的类型检查为例，可以像下面这样写：

1
2
3
4
5
6
7
8
9
10
11
12
Fixpoint type_check (Gamma : context) (t : tm) : option ty :=
  match t with
  (* ... *)
  | <{ (x, y) }> => T1 <- type_check x ;;
                    T2 <- type_check y ;;
                    return <{{ T1 * T2 }}>
  | <{ x.fst }> => T1 <- type_check x ;;
                   match T1 with 
                   | <{{ T1 * T2 }}> => return T1
                   | _ => fail
                   end
  | <{ x.snd }> => (* ... *)

Typing Mutable References

为了编码指针和引用，我们增加一些项：

$$
\begin{aligned}
t = ~ & … & \\
& \texttt{ref } t & \color{blue}{\text{(allocation)}} \\
& !t & \color{blue}{\text{(dereference)}} \\
& t := t & \color{blue}{\text{(assignment)}} \\
& \texttt{loc } n & \color{blue}{\text{(location)}}
\end{aligned}
$$

注意引入指针之后 STLC 不再是纯函数式语言，所以在描述小步法的时候要带上内存池 $st$。几条规则如下：

$$
\begin{matrix}
\dfrac{t_1 / st \longrightarrow t_1’ / st’}{\texttt{ref }t_1/st\longrightarrow \texttt{ref }t_1’/st’} & \color{blue}{\text{(ST_Ref)}} \\
\\
\dfrac{}{\texttt{ref } v / st\longrightarrow \texttt{loc } |st| / st, v} & \color{blue}{\text{(ST_RefValue)}} \\
\\
\dfrac{t_1 / st \longrightarrow t_1’ / st’}{!t_1 / st \longrightarrow !t_1’ / st’} & \color{blue}{\text{(ST_Deref)}} \\
\\
\dfrac{l < |st|}{!(\texttt{loc } l) / st \longrightarrow st_l / st} & \color{blue}{\text{(ST_DerefLoc)}} \\
\\
\dfrac{t_1 / st \longrightarrow t_1’ / st’}{t_1 := t_2 /st\longrightarrow t_1’ := t_2 /st’} & \color{blue}{\text{(ST_Assign1)}} \\
\\
\dfrac{t_2 / st \longrightarrow t_2’ / st’}{t_1 := t_2 /st\longrightarrow t_1 := t_2’ /st’} & \color{blue}{\text{(ST_Assign1)}} \\
\\
\dfrac{l < |st|}{\texttt{loc }l := v / st \longrightarrow \texttt{unit} [l := v]st}& \color{blue}{\text{(ST_Assign)}}
\end{matrix}
$$

注意你不一定能推导出内存池中每一位的类型，比如对于

$$
st = [\lambda x : \texttt{Nat}, (!(\texttt{loc }1)) x, \lambda x : \texttt{Nat}, (!(\texttt{loc }0)) x]
$$

你无法知道 $st_0$ 和 $st_1$ 分别是什么类型。但是程序中不会出现 loc，所以类型检查时我们不需要试图知道地址的类型。只需要定义

$$
\begin{matrix}
\dfrac{\Gamma \vdash t_1 \in T_1}{\Gamma \vdash \texttt{ref }t_1\in \texttt{Ref } T_1} & \color{blue}{\text{(T_Ref)}} \\
\\
\dfrac{\Gamma \vdash t_1 \in \texttt{Ref } T_1}{\Gamma \vdash !t_1 \in T_1} & \color{blue}{\text{(T_Deref)}} \\
\\
\dfrac{\Gamma \vdash t_1 \in \texttt{Ref }T_2\quad\Gamma \vdash t_2\in T_2}{\Gamma \vdash t_1:=t_2\in \texttt{Unit}} & \color{blue}{\text{(T_Assign)}}
\end{matrix}
$$

但是在求值过程中会产生 loc，因此为了证明 Progress 和 Preservation 你不得不知道每一位是什么类型。所以说这里我们只能弱化 Progress 和 Preservation，只证明你能推出 $st$ 每一位的类型时，这两个性质成立。具体地，我们定义数组 $ST$ 存储 $st$ 对应位上的类型。此时对于一个表达式，$\Gamma$ 和 $ST$ 将共同决定其类型，记作 $\Gamma; ST \vdash t \in T$。称 $ST$ 对于 $st$ 是 well-typed，若他们长度相等并且所有的 $st_i$ 都可以推出类型 $ST_i$。

于是我们可以推到 loc 的类型：

$$
\begin{matrix}
\dfrac{l < |ST|}{\Gamma; ST\vdash \texttt{loc }l \in \texttt{Ref } ST_l} & \color{blue}{\text{(ST_Loc)}}
\end{matrix}
$$

注意 well-typed 的 $ST$ 不是唯一的：

$$
st = [!(\texttt{loc} 0)]
$$

对于任意的 $ST$ 都是 well-typed 的。

然后 preservation 和 progress 的定义在 Coq 下面是

1
2
3
4
5
6
7
8
9
10
11
12
13
Theorem preservation : forall ST t t' T st st',
  empty ; ST |- t \in T->
  store_well_typed ST st->
  t/st --> t'/st' ->
  exists ST',
    extends ST' ST /\
    empty; ST' |- t' \in T /\
    store_well_typed ST' st'.

Theorem progress : forall ST t T st,
  empty ; ST |- t \in T ->
  store_well_typed ST st ->
  (value t \/ exists t' st', t / st --> t' / st').

第 6 行的谓词 extends 判定 $ST$ 是否是 $ST’$ 的前缀。

有了引用之后我们无需 fix 也可以编写递归。方法是把函数存到内存里面去。下面的东西将一个阶乘函数存在了内存池的末尾，并返回 $n!$：

$$
\begin{aligned}
&(\lambda r : (\texttt{Ref } \texttt{Nat}\rightarrow \texttt{Nat}), \\
&\quad r := (\lambda n : \texttt{Nat}, \texttt{if $n=0$ then $1$ else $n \times (!r)(n - 1)$}); \\
&\quad (!r)) \\
&(\lambda n : \texttt{Nat}, 0)~n
\end{aligned}
$$

在 evaluate 这个语句的时候，首先调用 $\mathrm{ST\_App2}$ 开一个 $\texttt{Nat}\rightarrow\texttt{Nat}$ 的新内存，然后向 lambda abstraction 中带入这个地址，并将该地址上的值修改为递归调用自己的阶乘函数，然后返回这个函数。

有了引用、Record、let in 之后我们可以模拟封装，注意对象内部的变量只能用成员函数访问。对于这个类

1
2
3
4
5
6
7
8
class counter {
    private:
    int c;
    counter() { c = 0; }
    public:
    int i() { c++; return c; }
    int d() { c--; return c; }
}

可以这样模拟：

1
2
3
4
5
6
7
let newcounter = \_ : Unit,
  let c = ref 0 in

  let incc = \_: Unit, (c := succ (!c); !c) in
  let decc = \_: Unit, (c := pred (!c); !c) in
  {i = incc, d = decc}
in ...

那么下面的代码（写在 ... 后面即可）

1
2
3
4
5
let c1 = newcounter unit in
let c2 = newcounter unit in
let r1 = ci.i unit in let r1 = c1.i unit in
let r2 = c2.i unit in let r2 = c2.i unit in
r2

返回值是 $2$。

需要注意 let x = A in B 相当于

$$
(\lambda x : \mathrm{type}(A), B)~A
$$

行为上，会首先彻底展开 $A$，然后把 $B$ 中所有 $x$ 换成 $A$。

如果不写第一个 \_: Unit，就会导致 let c = ref 0 in ... 在最开始被展开，此时 c = ref 0 将被彻底展开（开一个新内存 l），然后下面的所有 c 将被换成 loc l，变成单例模式，返回 $4$。

如果在此基础上不写第二个 \_: Unit，展开完第一段代码第 $2$ 行之后 (c := succ (!c); !c) 被彻底展开，变成常数 $1$。之后调用 i 只是调用这个常数，因此返回 $1$。

Subtyping

Liskov 替换原则 如果在任意使用 T 类型的值的场合都可以传入 S 类型的任意值，那么 S 是 T 的子类。

$S$ 是 $T$ 的子类记为 $S <: T$。

有两个注意点。对于两个函数类型 $S_1\rightarrow T_1 <: S_2\rightarrow T_2$。将 $S_2$ 类型的值传入一个 $S_2\rightarrow T_2$ 是函数类型的一个使用场合，Liskov 原则表明此处可以使用 $S_1\rightarrow T_1$ 类型的函数。也就是任意的 $S_2$ 类的值都可以传入 $S_1\rightarrow T_1$ 类型的函数。$S_2$ 是 $S_1$ 的子类是这里的一个充分条件。

这里子部分与整体子类关系相反，称为逆变式（contravariance），对应为了提供容器而存在的类型（输入类型）；而子部分与整体关系相同，称为协变式（convariance），对应为了提供值而存在的类型（输出类型）。

对于引用 $\texttt{Ref }T$ 的子部分 $T$，有

  • $T$ 是输入类型：a := b。
  • $T$ 是输出类型：!a。

因此引用的子类推导关系是

$$
\frac{S <: T\quad T <: S}{\texttt{Ref }S <: \texttt{Ref }T}
$$

增加 $\texttt{Top}$ 表示所有类型的父类。这样可以做到父子类直接有不同的结构，比如说可以构造一条链：

$$
\texttt{Top}\rightarrow\texttt{Top} <: (\texttt{Top}\rightarrow\texttt{Top})\rightarrow\texttt{Top} <: \cdots
$$

注意这里所有的推导都是充分的。即使子类是一个偏序关系，你也没有很好的办法证明两个类是不可比的。

  1. 1.https://zhenjiang888.github.io/FP/2023/slides/ch20_internal.pdf，Page 11. ↩