SF-lean4 软件基础

Appearance

lean
import SFLean4.PLF.Maps
import SFLean4.PLF.Smallstep

软件基础 第二卷：程序语言基础 (PLF) ​

模块：类型系统 (Types) ​

我们的下一个核心主题是类型系统（Type Systems）——一种静态程序分析手段， 用于根据表达式最终计算结果的“形状”（Shape）对表达式进行分类。

我们将从最简单的一个带类型微型语言开始，介绍类型系统最基本的概念、定型规则（Typing Rules） 以及类型系统的两大基石定理：

  1. 类型保型性定理（Type Preservation / Subject Reduction）
  2. 进益定理（Progress）

进益定理指出“良类型（Well-typed）项绝不会卡住（Stuck）”，而保型定理指出“良类型项单步归约后类型不变”。 二者结合便构成了**类型安全性（Type Safety / Soundness）**的核心证明方法论（Wright & Felleisen 经典进路）。

在后续的 Stlc 章节中，我们将进一步迈向简单类型 Lambda 演算（Simply Typed Lambda-Calculus, STLC）。

lean
namespace PLF.Types

open PLF.Smallstep

namespace TM

1. 带类型的算术与布尔表达式 (Typed Arithmetic Expressions) ​

为了引入类型系统的必要性，我们需要一个可能在运行时因类型错误而“卡住”的微型语言。 仅有数值（如 Smallstep 中的常量与加法）无法体现类型不匹配； 而将**布尔值（Booleans）与自然数（Numbers）**融于一炉，便能展现丰富的类型现象。

lean
/-- 语言项（Terms）语法定义：
- `tru`: 布尔真值 `true`
- `fls`: 布尔假值 `false`
- `ite t1 t2 t3`: 条件分支 `if t1 then t2 else t3`
- `zro`: 自然数零 `0`
- `scc t`: 后继 `succ t`
- `prd t`: 前驱 `pred t`
- `iszro t`: 零测试 `iszero t`
-/
inductive tm : Type where
  | tru : tm
  | fls : tm
  | ite : tm → tm → tm → tm
  | zro : tm
  | scc : tm → tm
  | prd : tm → tm
  | iszro : tm → tm
  deriving Repr, DecidableEq

open tm

/-- 布尔值判定谓词：`true` 与 `false` 是布尔值。 -/
inductive bvalue : tm → Prop where
  | bv_true : bvalue tru
  | bv_false : bvalue fls

/-- 数值判定谓词：`0` 是数值，数值的后继依然是数值。 -/
inductive nvalue : tm → Prop where
  | nv_0 : nvalue zro
  | nv_succ (t : tm) : nvalue t → nvalue (scc t)

/-- 值（Value）：良构的规范结果，即布尔值或数值。 -/
def value (t : tm) : Prop :=
  bvalue t ∨ nvalue t

2. 操作语义 (Operational Semantics) ​

小步归约关系 t --> t'：

text
                   -------------------------------                   (ST_IfTrue)
                   if true then t1 else t2 --> t1

                   -------------------------------                  (ST_IfFalse)
                   if false then t1 else t2 --> t2

                               t1 --> t1'
            ------------------------------------------------             (ST_If)
            if t1 then t2 else t3 --> if t1' then t2 else t3

                             t1 --> t1'
                         --------------------                          (ST_Succ)
                         succ t1 --> succ t1'

                            ------------                               (ST_Pred0)
                            pred 0 --> 0

                         numeric value v
                        -------------------                        (ST_PredSucc)
                        pred (succ v) --> v

                               t1 --> t1'
                          --------------------                          (ST_Pred)
                          pred t1 --> pred t1'

                           -----------------                         (ST_IsZero0)
                           iszero 0 --> true

                          numeric value v
                       -------------------------                  (ST_IsZeroSucc)
                       iszero (succ v) --> false

                             t1 --> t1'
                        ------------------------                      (ST_IsZero)
                        iszero t1 --> iszero t1'
lean
inductive step : tm → tm → Prop where
  | ST_IfTrue (t1 t2 : tm) :
      step (ite tru t1 t2) t1
  | ST_IfFalse (t1 t2 : tm) :
      step (ite fls t1 t2) t2
  | ST_If (c c' t2 t3 : tm) :
      step c c' →
      step (ite c t2 t3) (ite c' t2 t3)
  | ST_Succ (t1 t1' : tm) :
      step t1 t1' →
      step (scc t1) (scc t1')
  | ST_Pred0 :
      step (prd zro) zro
  | ST_PredSucc (v : tm) :
      nvalue v →
      step (prd (scc v)) v
  | ST_Pred (t1 t1' : tm) :
      step t1 t1' →
      step (prd t1) (prd t1')
  | ST_IsZero0 :
      step (iszro zro) tru
  | ST_IsZeroSucc (v : tm) :
      nvalue v →
      step (iszro (scc v)) fls
  | ST_IsZero (t1 t1' : tm) :
      step t1 t1' →
      step (iszro t1) (iszro t1')

scoped notation:40 t " --> " t' => step t t'

3. 范式与卡住状态 (Normal Forms and Values) ​

在包含类型错误潜质的语言中，并非所有不可归约的项都是合法的值。 如果一个项既无法继续单步归约（处于范式 Normal Form），又不是值（¬ value t）， 我们就说这个项“卡住了”（Stuck）。

lean
/-- 单步归约范式：无法继续单步归约的项。 -/
def step_normal_form (t : tm) : Prop :=
  normal_form step t

/-- 卡住状态：是范式但不是值。 -/
def stuck (t : tm) : Prop :=
  step_normal_form t ∧ ¬ value t

/--
**** 练习: 2 星, standard (some_term_is_stuck)
证明存在某个项处于卡住状态（例如 `succ true`）。
-/
theorem some_term_is_stuck : ∃ t, stuck t := by
  sorry

/--
**** 练习: 3 星, standard (value_is_nf)
所有值都是单步归约范式（不可继续归约）。
-/
theorem value_is_nf (t : tm) :
  value t → step_normal_form t := by
  sorry

/--
**** 练习: 3 星, standard, optional (step_deterministic)
利用 `value_is_nf` 证明小步单步归约关系是确定性的。
-/
theorem step_deterministic :
  deterministic step := by
  sorry

4. 定型关系 (Typing Relation) ​

我们的语言包含两种类型：

  • Bool: 布尔类型
  • Nat: 自然数类型
lean
inductive ty : Type where
  | Bool : ty
  | Nat : ty
  deriving Repr, DecidableEq

/-- 项的类型判定谓词：`has_type t T` 表示项 `t` 具有类型 `T`。 -/
inductive has_type : tm → ty → Prop where
  | T_True :
      has_type tru ty.Bool
  | T_False :
      has_type fls ty.Bool
  | T_If (t1 t2 t3 : tm) (T : ty) :
      has_type t1 ty.Bool →
      has_type t2 T →
      has_type t3 T →
      has_type (ite t1 t2 t3) T
  | T_0 :
      has_type zro ty.Nat
  | T_Succ (t1 : tm) :
      has_type t1 ty.Nat →
      has_type (scc t1) ty.Nat
  | T_Pred (t1 : tm) :
      has_type t1 ty.Nat →
      has_type (prd t1) ty.Nat
  | T_Iszero (t1 : tm) :
      has_type t1 ty.Nat →
      has_type (iszro t1) ty.Bool

/-- 示例：`if false then 0 else (succ 0)` 具有类型 `Nat`。 -/
theorem has_type_1 : has_type (ite fls zro (scc zro)) ty.Nat := by
  apply has_type.T_If
  · exact has_type.T_False
  · exact has_type.T_0
  · exact has_type.T_Succ _ has_type.T_0

/-- 反例：`if false then 0 else true` 是病态的，分支类型不一致，无法定型。 -/
theorem not_has_type : ¬ has_type (ite fls zro tru) ty.Bool := by
  intro h
  cases h with
  | T_If _ _ _ _ h1 h2 h3 => cases h2

/-- 反例：`succ false` 存在类型错误，因此整个条件表达式无法定型。 -/
theorem not_has_type' : ¬ has_type (ite (iszro (scc zro)) (scc fls) tru) ty.Bool := by
  intro h
  cases h with
  | T_If _ _ _ _ h1 h2 h3 => cases h2

/--
**** 练习: 1 星, standard, optional (succ_hastype_nat__hastype_nat)
如果 `succ t` 具有类型 `Nat`，则 `t` 也必具有类型 `Nat`。
-/
theorem succ_hastype_nat__hastype_nat (t : tm) :
  has_type (scc t) ty.Nat →
  has_type t ty.Nat := by
  sorry

规范形式引理 (Canonical Forms) ​

规范形式引理表明：良类型的值必然具有由其类型所决定的具体构造形式。

lean
theorem bool_canonical (t : tm) :
  has_type t ty.Bool → value t → bvalue t := by
  intro HT Hval
  rcases Hval with (Hb | Hn)
  · exact Hb
  · cases Hn with
    | nv_0 => cases HT
    | nv_succ t' Hn' => cases HT

theorem nat_canonical (t : tm) :
  has_type t ty.Nat → value t → nvalue t := by
  intro HT Hval
  rcases Hval with (Hb | Hn)
  · cases Hb with
    | bv_true => cases HT
    | bv_false => cases HT
  · exact Hn

5. 进益定理 (Progress) ​

进益定理表明：任何良类型的项要么已经是一个值，要么可以继续向前归约至少一步。 它保证了良类型的程序绝不会陷入未定义的卡住状态。

lean
/--
**** 练习: 3 星, standard (finish_progress)
证明类型系统的进益性质。
-/
theorem progress (t : tm) (T : ty) :
  has_type t T →
  value t ∨ ∃ t', step t t' := by
  sorry

/--
**** 练习: 3 星, advanced, optional (finish_progress_informal)
补全进益定理对应的纸笔非形式化归纳证明。
-/
def manual_grade_for_finish_progress_informal : Option (Nat × String) := none

6. 类型保型性定理 (Type Preservation / Subject Reduction) ​

保型性定理表明：若一个良类型的项向前单步归约，归约后的项仍然保持相同的类型。

lean
/--
**** 练习: 2 星, standard (finish_preservation)
对定型推导树归纳证明保型性。
-/
theorem preservation (t t' : tm) (T : ty) :
  has_type t T →
  step t t' →
  has_type t' T := by
  sorry

/--
**** 练习: 3 星, advanced, optional (finish_preservation_informal)
补全保型性定理对应的纸笔非形式化归纳证明。
-/
def manual_grade_for_finish_preservation_informal : Option (Nat × String) := none

/--
**** 练习: 3 星, standard (preservation_alternate_proof)
换一种方式证明保型性：对求值归约推导树（`step t t'`）进行归纳。
-/
theorem preservation' (t t' : tm) (T : ty) :
  has_type t T →
  step t t' →
  has_type t' T := by
  sorry

7. 类型健全性 (Type Soundness) ​

综合进益定理与保型性定理，我们可以证明类型健全性（Soundness）： 从一个良类型项出发，经过任意有限步多步归约（-->*），都绝对不可能到达任何卡住状态（Stuck）。

lean
def multistep : tm → tm → Prop := multi step
scoped notation:40 t1 " -->* " t2 => multistep t1 t2

theorem soundness (t t' : tm) (T : ty) :
  has_type t T →
  multistep t t' →
  ¬ stuck t' := by
  intro HT Hmulti
  induction Hmulti with
  | multi_refl x =>
    rintro ⟨Hnf, Hnotval⟩
    have Hprog := progress x T HT
    rcases Hprog with (Hval | ⟨x', Hstep⟩)
    · exact Hnotval Hval
    · exact Hnf ⟨x', Hstep⟩
  | multi_step x y z Hstep Hmulti_yz IH =>
    have HTy := preservation x y T HT Hstep
    exact IH HTy

8. 扩展练习 (Additional Exercises) ​

lean
/--
**** 练习: 3 星, standard, especially useful (subject_expansion)
保型性的逆命题称为主词扩张（Subject Expansion）：若 `t --> t'` 且 `t'` 良类型，
是否一定有 `t` 也是良类型的？如果不成立，请给出反例。
-/
theorem subject_expansion :
  (∀ t t' T, step t t' ∧ has_type t' T → has_type t T) ∨
  ¬ (∀ t t' T, step t t' ∧ has_type t' T → has_type t T) := by
  sorry

/--
**** 练习: 2 星, standard (variation1)
若在定型关系中加入规则 `T_SuccBool : |-- t \in Bool → |-- succ t \in Bool`，
单步确定性、进益性、保型性哪些仍然成立？哪些被破坏？
-/
def manual_grade_for_variation1 : Option (Nat × String) := none

/--
**** 练习: 2 星, standard (variation2)
若在单步归约关系中加入规则 `ST_Funny1 : if true then t2 else t3 --> t3`，
哪些性质会被破坏？请给出反例。
-/
def manual_grade_for_variation2 : Option (Nat × String) := none

**** 练习: 2 星, standard, optional (variation3) 若在单步归约关系中加入规则： ST_Funny2 : t2 --> t2' → if t1 then t2 else t3 --> if t1 then t2' else t3 哪些性质会被破坏？请给出反例。

**** 练习: 2 星, standard, optional (variation4) 若在单步归约关系中加入规则： ST_Funny3 : pred false --> pred (pred false) 哪些性质会被破坏？请给出反例。

**** 练习: 2 星, standard, optional (variation5) 若在定型关系中加入公理： T_Funny4 : |-- 0 \in Bool 哪些性质会被破坏？请给出反例。

**** 练习: 2 星, standard, optional (variation6) 若在定型关系中加入公理： T_Funny5 : |-- pred 0 \in Bool 哪些性质会被破坏？请给出反例。

**** 练习: 3 星, standard, optional (more_variations) 请自行尝试构造新的规则变体，使得某些性质成立而另一些性质被精确破坏。

lean
/--
**** 练习: 1 星, standard (remove_pred0)
归约规则 `ST_Pred0` 将 `pred 0` 规约为 `0`。如果直接移除该规则，会有什么后果？
-/
def manual_grade_for_remove_pred0 : Option (Nat × String) := none

/--
**** 练习: 4 星, advanced (prog_pres_bigstep)
思考：如果在**大步语义（Big-step Semantics）**下表述进益性与保型性，命题应该如何书写？
大步语义在刻画非停机程序时有哪些局限性？
-/
def manual_grade_for_prog_pres_bigstep : Option (Nat × String) := none

end TM

end PLF.Types

基于 MIT 与 Software Foundations 原版教育许可协议开源

Copyright © 2024-2026 Ghost-Silver · Software Foundations Authors