编辑“︁Lean幺半群”︁（章节）

= Lean幺半群 =

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

== 定义与数学基础 ==

数学上，'''幺半群'''是满足以下性质的代数结构 <math>(M, \cdot, e)</math>：
* '''封闭性'''：<math>\forall a,b \in M, a \cdot b \in M</math>
* '''结合律'''：<math>\forall a,b,c \in M, (a \cdot b) \cdot c = a \cdot (b \cdot c)</math>
* '''单位元'''：<math>\exists e \in M, \forall a \in M, e \cdot a = a \cdot e = a</math>

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

<syntaxhighlight lang="lean">
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                            -- 左单位元
</syntaxhighlight>

== 基本示例 ==

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

<syntaxhighlight lang="lean">
instance : Monoid ℕ where
  mul := Nat.add
  one := 0
  mul_assoc := Nat.add_assoc
  mul_one := Nat.add_zero
  one_mul := Nat.zero_add
</syntaxhighlight>

=== 列表连接幺半群 ===
列表类型 <code>List α</code> 与连接操作 <code>++</code> 构成幺半群：

<syntaxhighlight lang="lean">
instance {α : Type} : Monoid (List α) where
  mul := List.append
  one := []
  mul_assoc := List.append_assoc
  mul_one := List.append_nil
  one_mul := List.nil_append
</syntaxhighlight>

== 高级应用 ==

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

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

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

<syntaxhighlight lang="lean">
def FreeMonoid (α : Type) := List α

instance : Monoid (FreeMonoid α) where
  -- 实现与List相同
</syntaxhighlight>

== 实际案例 ==

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

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

对应的Lean模型：

<syntaxhighlight lang="lean">
structure TimestampedLog where
  timestamp : Nat
  message : String

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

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

<syntaxhighlight lang="lean">
inductive Event | Send | Receive

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

== 性质验证 ==

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

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

== 扩展阅读 ==

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

[[Category:Lean代数结构]]
[[Category:函数式编程]]
[[Category:抽象代数]]

[[Category:计算机科学]]
[[Category:Lean]]