编辑“︁Lean格”︁

= Lean格 =

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

== 数学定义 ==

在数学中，格 <math>(L, \leq)</math> 是一个偏序集，其中对于任意两个元素 <math>a, b \in L</math>，存在：
* '''并'''（join）：<math>a \vee b</math> 是最小上界
* '''交'''（meet）：<math>a \wedge b</math> 是最大下界

满足以下性质：
# 交换律：<math>a \vee b = b \vee a</math>，<math>a \wedge b = b \wedge a</math>
# 结合律：<math>a \vee (b \vee c) = (a \vee b) \vee c</math>，<math>a \wedge (b \wedge c) = (a \wedge b) \wedge c</math>
# 吸收律：<math>a \vee (a \wedge b) = a</math>，<math>a \wedge (a \vee b) = a</math>

== Lean中的格实现 ==

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

<syntaxhighlight lang="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)
</syntaxhighlight>

=== 基本示例 ===

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

<syntaxhighlight lang="lean">
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 }
</syntaxhighlight>

这个实现展示了布尔值上的格结构，其中：
* 偏序关系定义为蕴含（<code>→</code>）
* 交运算为逻辑与（<code>&&</code>）
* 并运算为逻辑或（<code>||</code>）

== 格的类型 ==

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

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

<syntaxhighlight lang="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)
</syntaxhighlight>

=== 分配格 ===
满足分配律的格：

<math>a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)</math>

=== 模格 ===
满足模律的格：

如果 <math>a \leq c</math>，则 <math>a \vee (b \wedge c) = (a \vee b) \wedge c</math>

== 可视化表示 ==

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

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

== 应用案例 ==

=== 类型系统中的应用 ===

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

<syntaxhighlight lang="lean">
inductive Animal
| dog | cat | bird

inductive Pet
| dog | cat
</syntaxhighlight>

这里可以定义一个子类型格，其中：
* 并运算表示最具体的共同超类型
* 交运算表示最一般的共同子类型

=== 程序分析中的应用 ===

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

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

== 进阶主题 ==

=== 不动点定理 ===

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

<syntaxhighlight lang="lean">
theorem KnasterTarski (α : Type) [CompleteLattice α] (f : α → α) (mono : Monotone f) :
    ∃ a : α, isLeast (fixedPoints f) a :=
-- 证明略
</syntaxhighlight>

=== 格同态 ===

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

<syntaxhighlight lang="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)
</syntaxhighlight>

== 练习 ==

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

== 参见 ==

* [[偏序集]]
* [[布尔代数]]
* [[抽象解释]]
* [[类型系统]]

[[Category:Lean定理证明器]]
[[Category:格理论]]
[[Category:代数结构]]

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean代数结构]]