本篇用一个端到端的案例把前 14 篇的技术串起来：定义一门带类型的小语言，给它写解释器，证明类型安全定理（progress + preservation），最后用 Extraction 把经过验证的解释器导出为可执行的 OCaml 代码。整个流程对应 Programming Language Foundations (PLF) 中 STLC 章节的精简版本，但更侧重工程实操。

语言定义：MiniLang

MiniLang 只有两种类型、五种表达式，足够展示类型安全证明的完整结构，又不至于让证明淹没在 case analysis 中。

类型与语法

1
2
3
4
5
6
7
8
9
10
Inductive ty : Type :=
  | TBool : ty
  | TNat  : ty.

Inductive expr : Type :=
  | ETrue  : expr
  | EFalse : expr
  | ENat   : nat -> expr
  | EPlus  : expr -> expr -> expr
  | EIf    : expr -> expr -> expr -> expr.

EPlus 要求两个操作数都是 TNat；EIf 要求条件是 TBool，两个分支类型一致。

值的判定

1
2
3
4
Inductive is_value : expr -> Prop :=
  | VTrue  : is_value ETrue
  | VFalse : is_value EFalse
  | VNat   : forall n, is_value (ENat n).

只有字面量是值。EPlus 和 EIf 永远不是值，即使子表达式全部求值完毕，结果也会归约到 ENat。

小步语义

选择小步语义（small-step）而非大步语义（big-step），因为 preservation 定理的陈述在小步下更自然——每一步归约都保持类型不变。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Reserved Notation "e '-->' e'" (at level 40).

Inductive step : expr -> expr -> Prop :=
  | SPlus : forall n1 n2,
      (EPlus (ENat n1) (ENat n2)) --> (ENat (n1 + n2))
  | SPlusL : forall e1 e1' e2,
      e1 --> e1' ->
      (EPlus e1 e2) --> (EPlus e1' e2)
  | SPlusR : forall n1 e2 e2',
      e2 --> e2' ->
      (EPlus (ENat n1) e2) --> (EPlus (ENat n1) e2')
  | SIfTrue : forall e1 e2,
      (EIf ETrue e1 e2) --> e1
  | SIfFalse : forall e1 e2,
      (EIf EFalse e1 e2) --> e2
  | SIfCond : forall e0 e0' e1 e2,
      e0 --> e0' ->
      (EIf e0 e1 e2) --> (EIf e0' e1 e2)

where "e '-->' e'" := (step e e').

SPlusL 和 SPlusR 规定了从左到右的求值顺序。SPlusR 的前提要求左操作数已经是 ENat n1，保证不会同时归约两侧。

类型系统

MiniLang 没有变量，不需要类型环境（typing context）。类型判断的形式是 |- e : T。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Reserved Notation "'|-' e ':' T" (at level 40).

Inductive has_type : expr -> ty -> Prop :=
  | T_True  : |- ETrue : TBool
  | T_False : |- EFalse : TBool
  | T_Nat   : forall n, |- (ENat n) : TNat
  | T_Plus  : forall e1 e2,
      |- e1 : TNat ->
      |- e2 : TNat ->
      |- (EPlus e1 e2) : TNat
  | T_If : forall e0 e1 e2 T,
      |- e0 : TBool ->
      |- e1 : T ->
      |- e2 : T ->
      |- (EIf e0 e1 e2) : T

where "'|-' e ':' T" := (has_type e T).

类型唯一性

每个合法表达式恰好有一个类型。这个引理在后面的证明中虽然不直接被引用，但它确认了类型系统没有歧义。

1
2
3
4
5
6
7
8
9
Lemma type_unique : forall e T1 T2,
  |- e : T1 -> |- e : T2 -> T1 = T2.
Proof.
  intros e T1 T2 HT1 HT2.
  generalize dependent T2.
  induction HT1; intros T2 HT2; inversion HT2; subst; auto.
  - apply IHHT1_1 in H2. discriminate.
    (* 这个分支不会出现，因为 T_Plus 和 T_If 对 e1 的类型要求不同 *)
Abort.

上面的尝试卡在了 T_Plus 与 T_If 的交叉 case 上。问题在于 inversion 之后残留的假设需要更细致的处理。正确做法是对 HT1 做归纳时，在每个 case 里对 HT2 做 inversion 并立即 subst：

1
2
3
4
5
6
7
8
9
10
11
12
Lemma type_unique : forall e T1 T2,
  |- e : T1 -> |- e : T2 -> T1 = T2.
Proof.
  intros e T1 T2 HT1.
  generalize dependent T2.
  induction HT1; intros T2 HT2; inversion HT2; subst; auto.
  (* T_If case: 两个分支类型相同，用 IHHT1_2 得到 T = T0 *)
  - apply IHHT1_2. assumption.
Qed.

Print Assumptions type_unique.
(* Closed under the global context — 没有使用公理 *)

失败尝试和修正的对比说明了一件事：inversion 在多构造子的归纳类型上容易产生过多的子目标，需要在 generalize dependent 的时机上做选择。

类型安全：Progress

Progress 定理：如果 |- e : T，那么 e 要么是值，要么存在 e' 使得 e --> e'。

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
Theorem progress : forall e T,
  |- e : T ->
  is_value e \/ exists e', e --> e'.
Proof.
  intros e T HT.
  induction HT.
  - (* T_True *)  left. constructor.
  - (* T_False *) left. constructor.
  - (* T_Nat *)   left. constructor.
  - (* T_Plus *)
    right.
    destruct IHHT1 as [Hv1 | [e1' Hs1]].
    + destruct IHHT2 as [Hv2 | [e2' Hs2]].
      * (* 两侧都是值 *)
        inversion Hv1; subst; inversion HT1.
        (* e1 必须是 ENat n *)
        inversion Hv2; subst; inversion HT2.
        (* e2 必须是 ENat n0 *)
        exists (ENat (n + n0)). constructor.
      * (* e2 可以归约 *)
        inversion Hv1; subst; inversion HT1.
        exists (EPlus (ENat n) e2'). apply SPlusR. assumption.
    + (* e1 可以归约 *)
      exists (EPlus e1' e2). apply SPlusL. assumption.
  - (* T_If *)
    right.
    destruct IHHT1 as [Hv0 | [e0' Hs0]].
    + inversion Hv0; subst; inversion HT1.
      * exists e1. constructor.
      * exists e2. constructor.
    + exists (EIf e0' e1 e2). constructor. assumption.
Qed.

T_Plus 的 case 是最复杂的，需要对两个子表达式分别讨论是否是值。inversion Hv1; subst; inversion HT1 这个组合拳的作用是：先从"e1 是值"推出 e1 的具体形式（ETrue/EFalse/ENat n），再用 inversion HT1 排除类型不匹配的情况（ETrue 和 EFalse 的类型是 TBool，与 TNat 矛盾），只留下 ENat n 这一个可能。

类型安全：Preservation

Preservation 定理：如果 |- e : T 且 e --> e'，那么 |- e' : T。

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
Theorem preservation : forall e e' T,
  |- e : T ->
  e --> e' ->
  |- e' : T.
Proof.
  intros e e' T HT Hstep.
  generalize dependent T.
  induction Hstep; intros T HT; inversion HT; subst.
  - (* SPlus *)
    constructor.
  - (* SPlusL *)
    apply T_Plus.
    + apply IHHstep. assumption.
    + assumption.
  - (* SPlusR *)
    apply T_Plus.
    + assumption.
    + apply IHHstep. assumption.
  - (* SIfTrue *)
    assumption.
  - (* SIfFalse *)
    assumption.
  - (* SIfCond *)
    apply T_If.
    + apply IHHstep. assumption.
    + assumption.
    + assumption.
Qed.

Preservation 的证明比 Progress 简单。关键手法是对 Hstep（归约步骤）做归纳而非对 HT（类型推导）做归纳——对归约步骤归纳时，每个 case 的结构与语义规则一一对应，inversion HT 能直接拆出子表达式的类型信息。

多步归约与类型安全

把 Progress 和 Preservation 组合起来，可以得到完整的类型安全定理：合法程序在任意步归约后要么是值，要么还能继续归约。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Inductive multi_step : expr -> expr -> Prop :=
  | MSRefl : forall e, multi_step e e
  | MSTrans : forall e1 e2 e3,
      e1 --> e2 ->
      multi_step e2 e3 ->
      multi_step e1 e3.

Theorem type_safety : forall e e' T,
  |- e : T ->
  multi_step e e' ->
  is_value e' \/ exists e'', e' --> e''.
Proof.
  intros e e' T HT Hmulti.
  induction Hmulti.
  - apply progress with T. assumption.
  - apply IHHmulti.
    eapply preservation; eassumption.
Qed.

Show Proof.

Show Proof. 输出的证明项展示了 preservation 和 progress 如何在 multi_step 的归纳中配合工作：每一步先用 preservation 维持类型不变，最终用 progress 判断终态。

可判定的类型检查器

上面的类型系统是关系式（relational）的——它描述"什么是合法的类型推导"，但不能直接作为程序执行。下面写一个函数式的类型检查器，然后证明它与关系式定义等价。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Fixpoint typecheck (e : expr) : option ty :=
  match e with
  | ETrue      => Some TBool
  | EFalse     => Some TBool
  | ENat _     => Some TNat
  | EPlus a b  =>
      match typecheck a, typecheck b with
      | Some TNat, Some TNat => Some TNat
      | _, _ => None
      end
  | EIf c t f  =>
      match typecheck c, typecheck t, typecheck f with
      | Some TBool, Some t1, Some t2 =>
          if ty_eqb t1 t2 then Some t1 else None
      | _, _, _ => None
      end
  end.

其中 ty_eqb 是类型的布尔相等判定：

1
2
3
4
5
6
7
8
9
10
11
12
Definition ty_eqb (t1 t2 : ty) : bool :=
  match t1, t2 with
  | TBool, TBool => true
  | TNat, TNat   => true
  | _, _         => false
  end.

Lemma ty_eqb_eq : forall t1 t2, ty_eqb t1 t2 = true <-> t1 = t2.
Proof.
  destruct t1, t2; simpl; split; intros; try reflexivity;
    try discriminate; try assumption.
Qed.

类型检查器的正确性

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
Theorem typecheck_sound : forall e T,
  typecheck e = Some T -> |- e : T.
Proof.
  induction e; simpl; intros T HTC.
  - inversion HTC. constructor.
  - inversion HTC. constructor.
  - inversion HTC. constructor.
  - (* EPlus *)
    destruct (typecheck e1) eqn:E1; try discriminate.
    destruct (typecheck e2) eqn:E2; try discriminate.
    destruct t; try discriminate.
    destruct t0; try discriminate.
    inversion HTC; subst. constructor; auto.
  - (* EIf *)
    destruct (typecheck e1) eqn:E1; try discriminate.
    destruct t; try discriminate.
    destruct (typecheck e2) eqn:E2; try discriminate.
    destruct (typecheck e3) eqn:E3; try discriminate.
    destruct (ty_eqb t t0) eqn:Heq; try discriminate.
    apply ty_eqb_eq in Heq. subst.
    inversion HTC; subst. constructor; auto.
Qed.

Theorem typecheck_complete : forall e T,
  |- e : T -> typecheck e = Some T.
Proof.
  intros e T HT.
  induction HT; simpl; auto.
  - rewrite IHHT1, IHHT2. reflexivity.
  - rewrite IHHT1, IHHT2, IHHT3.
    assert (ty_eqb T T = true) as ->
      by (apply ty_eqb_eq; reflexivity).
    reflexivity.
Qed.

soundness 和 completeness 合在一起意味着 typecheck e = Some T 与 |- e : T 完全等价。函数式的 typecheck 可以被提取为可执行代码，关系式的 has_type 用来做证明推理。

求值器与提取

燃料驱动的求值函数

Coq 的 Fixpoint 要求结构递减，无法直接写 while (!is_value e) { e = step e; }。标准做法是引入"燃料"（fuel）参数：

1
2
3
4
5
6
7
8
9
10
Fixpoint eval (fuel : nat) (e : expr) : option expr :=
  match fuel with
  | O => None  (* 燃料耗尽 *)
  | S fuel' =>
      if is_value_dec e then Some e
      else match step_dec e with
           | Some e' => eval fuel' e'
           | None    => None  (* stuck，理论上不应出现 *)
           end
  end.

is_value_dec 和 step_dec 是值判定和单步归约的可判定版本。step_dec 的返回类型是 option expr 而非 {e' | e --> e'} + {forall e', ~ (e --> e')}——后者更精确但定义繁琐，对提取而言 option 足够。

提取到 OCaml

1
2
3
4
5
6
7
Require Extraction.
Require Import ExtrOcamlBasic ExtrOcamlNatInt.

Extraction Language OCaml.
Extract Inductive bool => "bool" ["true" "false"].

Extraction "minilang.ml" typecheck eval.

ExtrOcamlNatInt 把 Coq 的 nat 映射到 OCaml 的 int，避免一元编码导致的性能灾难。提取后的 minilang.ml 可以直接编译运行：

1
2
3
4
5
6
7
8
9
(* 使用示例 *)
let () =
  let e = EPlus (ENat 3, EIf (ETrue, ENat 4, ENat 5)) in
  match typecheck e with
  | Some TNat ->
    (match eval 100 e with
     | Some (ENat n) -> Printf.printf "result: %d\n" n
     | _ -> print_endline "evaluation failed")
  | _ -> print_endline "type error"

运行结果是 result: 7。类型检查器拒绝 EPlus (ETrue, ENat 1) 这类表达式，求值器保证合法表达式在足够燃料下归约到值。

提取后代码的信任边界

Print Assumptions type_safety 输出 Closed under the global context，说明类型安全定理不依赖任何公理。但提取环节引入了两个信任假设：

  1. ExtrOcamlNatInt 的映射正确性：Coq 的 nat 是无界的，OCaml 的 int 有溢出风险。MiniLang 的数值运算只有加法，实际使用中如果操作数足够大仍然会溢出。CompCert 的做法是使用 ZArith 配合 ExtrOcamlZInt，在 Coq 端就用有限位整数建模。
  2. 提取框架本身的正确性：Coq 的 Extraction 命令并非经过验证的编译器。CertiCoq 项目致力于提供经过验证的提取路径，但目前仍在开发中。

扩展方向

MiniLang 只覆盖了类型安全证明的最小骨架。以下是三个自然的扩展方向，每个都会显著增加证明的复杂度：

变量与绑定。引入 EVar 和 ELet（或 lambda），需要类型环境 Gamma，preservation 的证明需要 substitution lemma。Software Foundations 的 STLC 章节详细覆盖了这条路径。

可变状态。引入赋值和引用（ref/!/:=），语义从纯表达式变为 (store, expr) --> (store', expr')，类型系统需要 store typing。这是理解命令式语言形式化的关键一步。

子类型。引入 TTop 和子类型关系 <:，preservation 的证明需要 subsumption rule，progress 需要 canonical forms lemma 的扩展版本。

练习

  1. 给 MiniLang 添加 EMul（乘法）节点，更新语法、语义、类型规则，并修改 progress 和 preservation 的证明使其通过。提示：模仿 EPlus 的所有相关定义即可。

  2. 把求值顺序从"先左后右"改为"先右后左"：修改 SPlusL 和 SPlusR 的定义，使 EPlus 先归约右操作数。验证 progress 和 preservation 是否仍然成立（答案是成立的——类型安全与求值顺序无关）。

3.（挑战）给 MiniLang 添加 ELet (x : string) (e1 e2 : expr) 节点，引入类型环境 Gamma : string -> option ty，证明 substitution lemma 和新的 preservation 定理。Software Foundations 的 STLC 章节是这个练习的完整参考。

参考资料