编辑“︁Lean不可变数据结构”︁（章节）

= Lean不可变数据结构 =

== 简介 ==
'''不可变数据结构'''（Immutable Data Structures）是函数式编程中的核心概念，指一旦创建后其内容不能被修改的数据结构。在Lean（一种函数式编程语言和定理证明器）中，所有数据结构默认是不可变的。这种设计有助于编写更安全、更易于推理的代码，尤其在并发编程和形式化验证中表现突出。

不可变数据结构的主要特点包括：
* '''无副作用'''：操作不会改变原始数据，而是返回新的副本。
* '''持久性'''：旧版本的数据结构仍然可用，不会被新操作破坏。
* '''线程安全'''：由于不可变性，多线程环境下无需加锁。

== 基本原理 ==
在Lean中，当对数据结构进行操作时（如向列表添加元素），系统会创建新结构而非修改原结构。例如：

<syntaxhighlight lang="lean">
-- 定义一个列表
def originalList := [1, 2, 3]

-- "添加"元素（实际创建新列表）
def newList := 0 :: originalList

-- 输出结果
#eval originalList  -- [1, 2, 3]
#eval newList       -- [0, 1, 2, 3]
</syntaxhighlight>

注意：<code>originalList</code>未被修改，<code>::</code>操作符创建了包含新元素的新列表。

=== 内存效率 ===
Lean通过'''结构共享'''优化内存使用。新旧版本共享未修改的部分：

<mermaid>
graph LR
    A[newList] --> B[0]
    A --> C[originalList]
    C --> D[1]
    D --> E[2]
    E --> F[3]
</mermaid>

数学上，这种操作的时间复杂度为<math>O(1)</math>，因为只需分配一个新节点并指向原有结构。

== 核心数据结构示例 ==

=== 不可变列表 ===
Lean中的列表是单向链表，核心操作：

<syntaxhighlight lang="lean">
-- 创建
def emptyList : List Nat := []
def nums : List Nat := [1, 2, 3]

-- 模式匹配（递归处理）
def head : List α → Option α
  | [] => none
  | x :: _ => some x

-- 连接操作（创建新列表）
#eval [1, 2] ++ [3, 4]  -- [1, 2, 3, 4]
</syntaxhighlight>

=== 不可变数组（Array） ===
虽然内部使用可变实现，但对外表现为不可变：

<syntaxhighlight lang="lean">
def arr := #[1, 2, 3]
def newArr := arr.push 4  -- 创建新数组

#eval arr     -- #[1, 2, 3]
#eval newArr  -- #[1, 2, 3, 4]
</syntaxhighlight>

=== 不可变哈希映射 ===
使用Persistent Hash Map实现：

<syntaxhighlight lang="lean">
import Std.Data.HashMap

def map := Std.HashMap.empty.insert "a" 1
def newMap := map.insert "b" 2

#eval map.find? "a"    -- some 1
#eval newMap.find? "b" -- some 2
</syntaxhighlight>

== 实际应用案例 ==

=== 版本控制系统 ===
类似Git的版本控制工具使用不可变数据结构存储文件历史。每次提交创建新状态，旧提交保持不变：

<mermaid>
graph TB
    A[Commit A] -->|v1.txt| B["v1: 'Hello'"]
    C[Commit B] -->|v1.txt| D["v1: 'Hello world'"]
    C -->|new.txt| E["new: 'File'"]
</mermaid>

=== 撤销/重做功能 ===
编辑器中的撤销栈通过不可变数据结构实现：

<syntaxhighlight lang="lean">
structure EditorState where
  content : String
  history : List String

def applyEdit (state : EditorState) (newText : String) : EditorState :=
  { content := newText, history := state.content :: state.history }

def undo (state : EditorState) : EditorState :=
  match state.history with
  | [] => state
  | x :: xs => { content := x, history := xs }
</syntaxhighlight>

== 性能考量 ==
虽然不可变数据结构有诸多优点，但也需注意：
* '''内存压力'''：频繁修改可能产生大量临时对象
* '''访问模式'''：随机访问效率可能低于可变结构

优化策略包括：
* 使用'''批量操作'''（如<code>Array.append</code>）
* 对性能关键部分使用'''可变数据结构'''（需显式标记）

== 高级主题 ==
=== 结构归纳 ===
不可变数据结构天然支持数学归纳法，便于形式化证明：

<syntaxhighlight lang="lean">
theorem reverse_reverse : ∀ (l : List α), reverse (reverse l) = l := by
  intro l
  induction l with
  | nil => simp [reverse]
  | cons x xs ih => simp [reverse, ih]
</syntaxhighlight>

=== 惰性求值 ===
结合惰性求值可构建无限数据结构：

<syntaxhighlight lang="lean">
def fib : Stream Nat :=
  Stream.cons 0 (Stream.cons 1 (Stream.zipWith (+) fib (Stream.tail fib)))
</syntaxhighlight>

== 总结 ==
Lean的不可变数据结构提供了：
* 更安全的代码（消除意外修改）
* 更好的可组合性
* 内置的线程安全性
* 与定理证明的无缝集成

初学者应从列表和基础操作开始，逐步掌握更复杂的结构如红黑树和持久化队列。高级用户可探索如何利用不可变性优化算法和进行形式验证。

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