Lean格

Lean格

Lean格（Lattice in Lean）是Lean定理证明器中用于描述格结构的代数形式化工具。格是一种特殊的偏序集，其中任意两个元素都有唯一的最小上界（并）和最大下界（交）。在计算机科学中，格理论广泛应用于程序分析、类型系统和抽象解释等领域。

数学定义

在数学中，格 $(L,\le )$ 是一个偏序集，其中对于任意两个元素 $a,b\in L$，存在：

• 并（join）：$a\vee b$ 是最小上界
• 交（meet）：$a\wedge b$ 是最大下界

满足以下性质：

1. 交换律：$a\vee b=b\vee a$，$a\wedge b=b\wedge a$
2. 结合律：$a\vee (b\vee c)=(a\vee b)\vee c$，$a\wedge (b\wedge c)=(a\wedge b)\wedge c$
3. 吸收律：$a\vee (a\wedge b)=a$，$a\wedge (a\vee b)=a$

Lean中的格实现

在Lean中，格是通过类型类实现的。以下是Lean标准库中格的基本定义：

class Lattice (α : Type u) extends PartialOrder α :=
(inf : α → α → α)  -- 交运算
(sup : α → α → α)  -- 并运算
(inf_le_left : ∀ a b : α, inf a b ≤ a)
(inf_le_right : ∀ a b : α, inf a b ≤ b)
(le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ inf b c)
(le_sup_left : ∀ a b : α, a ≤ sup a b)
(le_sup_right : ∀ a b : α, b ≤ sup a b)
(sup_le : ∀ a b c : α, a ≤ c → b ≤ c → sup a b ≤ c)

基本示例

让我们定义一个简单的布尔格：

instance : Lattice Bool :=
{ le := λ a b, a → b,
  le_refl := by intros a h; exact h,
  le_trans := by intros a b c hab hbc ha; exact hbc (hab ha),
  le_antisymm := by intros a b hab hba; cases a; cases b; simp; try {contradiction}; trivial,
  inf := λ a b, a && b,
  sup := λ a b, a || b,
  inf_le_left := by intros a b; cases a; simp,
  inf_le_right := by intros a b; cases b; simp,
  le_inf := by intros a b c hab hac ha; exact hac (hab ha),
  le_sup_left := by intros a b; cases a; simp,
  le_sup_right := by intros a b; cases b; simp,
  sup_le := by intros a b c hac hbc h; cases h; exact hac h; exact hbc h }

这个实现展示了布尔值上的格结构，其中：

• 偏序关系定义为蕴含（→）
• 交运算为逻辑与（&&）
• 并运算为逻辑或（||）

格的类型

在Lean中，常见的格类型包括：

完全格

完全格是指所有子集都有上确界和下确界的格。在Lean中表示为：

class CompleteLattice (α : Type u) extends Lattice α :=
(Inf : set α → α)
(Sup : set α → α)
(Inf_le : ∀ s a, a ∈ s → Inf s ≤ a)
(le_Inf : ∀ s a, (∀ b ∈ s, a ≤ b) → a ≤ Inf s)
(le_Sup : ∀ s a, a ∈ s → a ≤ Sup s)
(Sup_le : ∀ s a, (∀ b ∈ s, b ≤ a) → Sup s ≤ a)

分配格

满足分配律的格：

$a\wedge (b\vee c)=(a\wedge b)\vee (a\wedge c)$

模格

满足模律的格：

如果 $a\le c$，则 $a\vee (b\wedge c)=(a\vee b)\wedge c$

可视化表示

graph TD A[⊤] --> B[a] A --> C[b] B --> D[⊥] C --> D

这个哈斯图表示了一个简单的两元素格，其中： - ⊤ 是最大元素 - ⊥ 是最小元素 - a 和 b 是不可比较的元素

应用案例

类型系统中的应用

在类型系统中，格用于描述类型之间的子类型关系。例如，考虑以下类型层次结构：

inductive Animal
| dog | cat | bird

inductive Pet
| dog | cat

这里可以定义一个子类型格，其中：

• 并运算表示最具体的共同超类型
• 交运算表示最一般的共同子类型

程序分析中的应用

在抽象解释中，格用于表示程序状态的可能值。例如，一个整数变量可能的状态可以构成如下格：

graph TD Top[⊤ = any integer] --> Pos[positive] Top --> Neg[negative] Top --> Zero[zero] Pos --> Bottom[⊥ = no value] Neg --> Bottom Zero --> Bottom

进阶主题

不动点定理

格理论中著名的Knaster-Tarski不动点定理指出，在完全格上的单调函数有最小不动点。这在Lean中可以形式化为：

theorem KnasterTarski (α : Type) [CompleteLattice α] (f : α → α) (mono : Monotone f) :
    ∃ a : α, isLeast (fixedPoints f) a :=
-- 证明略

格同态

格之间的结构保持映射称为格同态。在Lean中可以定义为：

structure LatticeHom (α β : Type) [Lattice α] [Lattice β] :=
(toFun : α → β)
(map_sup' : ∀ a b, toFun (a ⊔ b) = toFun a ⊔ toFun b)
(map_inf' : ∀ a b, toFun (a ⊓ b) = toFun a ⊓ toFun b)

练习

1. 证明布尔格是分配格。 2. 定义一个自然数上的整除格，其中 $a\le b$ 表示 $a$ 整除 $b$。 3. 实现一个简单的类型系统子类型关系的格结构。

参见

• 偏序集
• 布尔代数
• 抽象解释
• 类型系统