Lean幺半群

Lean幺半群

Lean幺半群（Monoid in Lean）是函数式编程和形式化验证中重要的代数结构，它表示一个带有结合性二元运算和单位元的集合。在Lean定理证明器中，幺半群是抽象代数的基础构件之一，广泛应用于算法设计、类型系统和自动化证明。

定义与数学基础

数学上，幺半群是满足以下性质的代数结构 $(M,\cdot ,e)$：

• 封闭性：$\mathrm{\forall }a,b\in M,a\cdot b\in M$
• 结合律：$\mathrm{\forall }a,b,c\in M,(a\cdot b)\cdot c=a\cdot (b\cdot c)$
• 单位元：$\mathrm{\exists }e\in M,\mathrm{\forall }a\in M,e\cdot a=a\cdot e=a$

在Lean中，幺半群通过类型类（Type Class）定义：

class Monoid (M : Type u) where
  mul : M → M → M  -- 二元运算
  one : M          -- 单位元
  mul_assoc : ∀ (a b c : M), mul (mul a b) c = mul a (mul b c)  -- 结合律
  mul_one : ∀ (a : M), mul a one = a                            -- 右单位元
  one_mul : ∀ (a : M), mul one a = a                            -- 左单位元

基本示例

自然数加法幺半群

自然数集 $\mathbb{\mathbb{N}}$ 与加法运算构成幺半群 $(\mathbb{\mathbb{N}},+,0)$：

instance : Monoid ℕ where
  mul := Nat.add
  one := 0
  mul_assoc := Nat.add_assoc
  mul_one := Nat.add_zero
  one_mul := Nat.zero_add

列表连接幺半群

列表类型 List α 与连接操作 ++ 构成幺半群：

instance {α : Type} : Monoid (List α) where
  mul := List.append
  one := []
  mul_assoc := List.append_assoc
  mul_one := List.append_nil
  one_mul := List.nil_append

高级应用

幺半群同态

两个幺半群之间的结构保持映射称为幺半群同态。例如，列表长度函数 length : List α → ℕ 是到加法幺半群的同态：

lemma length_hom (l₁ l₂ : List α) : 
  (l₁ ++ l₂).length = l₁.length + l₂.length := by
  induction l₁ <;> simp [*, Nat.add_assoc]

自由幺半群

自由幺半群是列表幺半群的推广，其元素是生成元的有限序列。在Lean中可定义为：

def FreeMonoid (α : Type) := List α

instance : Monoid (FreeMonoid α) where
  -- 实现与List相同

实际案例

日志聚合系统

分布式系统中，日志条目通过时间戳排序后形成时序幺半群：

graph LR A[Log Entry 1] --> C[Combined Log] B[Log Entry 2] --> C C --> D[Timestamp-sorted Stream]

对应的Lean模型：

structure TimestampedLog where
  timestamp : Nat
  message : String

instance : Monoid (List TimestampedLog) where
  -- 按timestamp合并的实现

并发编程中的事件序列

在CSP（Communicating Sequential Processes）模型中，进程的事件历史形成幺半群：

inductive Event | Send | Receive

instance : Monoid (List Event) where
  -- 标准列表幺半群

性质验证

使用Lean证明幺半群的性质，例如单位元的唯一性：

theorem one_unique (M : Type) [Monoid M] (e₁ e₂ : M) 
  (h₁ : ∀ a, mul e₁ a = a) (h₂ : ∀ a, mul a e₂ = a) : e₁ = e₂ := by
  rw [←h₂ e₁, h₁ e₂]

扩展阅读

• 幺半群与范畴论的关系
• 带交换律的交换幺半群（Commutative Monoid）
• 幂等幺半群（Idempotent Monoid）在数据库中的应用