编辑“︁Lean半群结构”︁

= Lean半群结构 =

'''半群'''（Semigroup）是抽象代数中的基本代数结构之一，在Lean定理证明器中，半群的定义和性质通过类型类和结构进行形式化。本章将详细介绍Lean中的半群结构，包括其数学定义、Lean实现方式、代码示例以及实际应用。

== 数学定义 ==

在数学中，半群是一个集合<math>S</math>配备一个二元运算<math>*</math>，满足以下性质：
* '''封闭性'''：对于所有<math>a, b \in S</math>，有<math>a * b \in S</math>。
* '''结合律'''：对于所有<math>a, b, c \in S</math>，有<math>(a * b) * c = a * (b * c)</math>。

在Lean中，半群通过类型类`Semigroup`定义，其核心是要求一个二元运算`mul`（通常记为`*`）并满足结合律。

== Lean中的半群实现 ==

Lean的Mathlib库中定义了`Semigroup`类型类，其结构如下：

<syntaxhighlight lang="lean">
class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
</syntaxhighlight>

这里：
* `G`是半群的载体类型。
* `extends Mul G`表示半群继承自具有乘法运算的类型。
* `mul_assoc`是结合律的公理。

=== 代码示例：定义半群实例 ===

以下是一个自定义半群的例子，使用自然数加法作为运算：

<syntaxhighlight lang="lean">
import Mathlib.Algebra.Group.Defs

instance : Semigroup Nat where
  mul := Nat.add
  mul_assoc := Nat.add_assoc
</syntaxhighlight>

解释：
* `mul := Nat.add`：将半群的乘法定义为自然数的加法。
* `mul_assoc := Nat.add_assoc`：使用`Nat.add_assoc`（自然数加法的结合律）来满足半群的结合律公理。

== 半群的实际应用 ==

半群在编程和数学中有广泛的应用，以下是一些例子：

=== 字符串拼接 ===

字符串在拼接操作下形成一个半群：

<syntaxhighlight lang="lean">
instance : Semigroup String where
  mul := String.append
  mul_assoc := by
    intros a b c
    simp [String.append_assoc]
</syntaxhighlight>

* `mul := String.append`：将半群的乘法定义为字符串的拼接。
* `mul_assoc`：证明字符串拼接满足结合律。

=== 列表拼接 ===

列表在拼接操作下也形成一个半群：

<syntaxhighlight lang="lean">
instance [α : Type] : Semigroup (List α) where
  mul := List.append
  mul_assoc := List.append_assoc
</syntaxhighlight>

* `mul := List.append`：将半群的乘法定义为列表的拼接。
* `mul_assoc := List.append_assoc`：使用`List.append_assoc`证明结合律。

== 半群的结合律图示 ==

结合律可以通过以下图示表示：

<mermaid>
graph LR
  A[ (a * b) * c ] -->|结合律| B[ a * (b * c) ]
</mermaid>

== 进阶：半群与幺半群的关系 ==

半群可以扩展为'''幺半群'''（Monoid），即增加一个单位元<math>e</math>满足<math>e * a = a * e = a</math>。在Lean中，幺半群的定义如下：

<syntaxhighlight lang="lean">
class Monoid (M : Type u) extends Semigroup M, One M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a
</syntaxhighlight>

== 总结 ==

* 半群是具有封闭性和结合律的代数结构。
* 在Lean中，半群通过`Semigroup`类型类实现，核心是`mul`和`mul_assoc`。
* 半群广泛应用于字符串、列表等数据结构的操作中。
* 半群可以扩展为幺半群，增加单位元性质。

理解半群是学习更复杂代数结构（如群、环、域）的基础。

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