编辑“︁Lean映射与字典”︁（章节）

= Lean映射与字典 =

== 介绍 ==

在Lean编程语言中，'''映射（Map）'''和'''字典（Dictionary）'''是两种重要的数据结构，用于存储键值对（key-value pairs）。它们允许用户通过唯一的键来高效地访问、插入或删除对应的值。虽然这两个术语有时可以互换使用，但在Lean中通常使用'''Std.HashMap'''和'''Lean.Data.HashMap'''等实现来表示这类结构。

映射与字典的核心特点是：
* '''键的唯一性'''：每个键只能出现一次
* '''高效的查找'''：通过哈希或树结构实现快速访问
* '''可变/不可变版本'''：Lean同时支持函数式（不可变）和命令式（可变）风格

== 基本操作 ==

=== 创建映射 ===
<syntaxhighlight lang="lean">
-- 使用Std.HashMap
import Std.Data.HashMap

def myMap : Std.HashMap String Nat := 
  Std.HashMap.empty
    |>.insert "apple" 3
    |>.insert "banana" 5

-- 使用Lean.Data.HashMap
import Lean.Data.HashMap

def myDict : Lean.HashMap String Nat :=
  Lean.mkHashMap 
    |>.insert "apple" 3
    |>.insert "banana" 5
</syntaxhighlight>

=== 常见操作示例 ===
<syntaxhighlight lang="lean">
-- 查找
#eval myMap.find? "apple"  -- some 3
#eval myMap.find? "orange" -- none

-- 更新
def updatedMap := myMap.insert "apple" 10
#eval updatedMap.find? "apple"  -- some 10

-- 删除
def reducedMap := myMap.erase "banana"
#eval reducedMap.find? "banana" -- none

-- 大小
#eval myMap.size  -- 2
</syntaxhighlight>

== 内部实现 ==

Lean中的映射通常使用以下两种实现方式：

=== 哈希表实现 ===
<mermaid>
graph LR
    A[键] --> B[哈希函数]
    B --> C[哈希值]
    C --> D[桶数组索引]
    D --> E[存储桶]
    E --> F[键值对链表]
</mermaid>

* 平均时间复杂度：
** 插入：<math>O(1)</math>
** 查找：<math>O(1)</math>
** 删除：<math>O(1)</math>

=== 持久化数据结构实现 ===
对于不可变映射，Lean使用'''哈希数组映射尝试树（HAMT）'''：
<mermaid>
graph TD
    Root --> L1[Level 1]
    Root --> L2[Level 2]
    L1 --> N1[Node]
    L1 --> N2[Node]
    N1 --> K1[Key1-Value1]
    N1 --> K2[Key2-Value2]
</mermaid>

== 高级用法 ==

=== 合并映射 ===
<syntaxhighlight lang="lean">
def map1 := Std.HashMap.empty.insert "a" 1 |>.insert "b" 2
def map2 := Std.HashMap.empty.insert "b" 3 |>.insert "c" 4

-- 合并（后者优先）
def merged := map1.merge map2
#eval merged.find? "b"  -- some 3
</syntaxhighlight>

=== 映射转换 ===
<syntaxhighlight lang="lean">
-- 使用fold
def sumValues (m : Std.HashMap String Nat) : Nat :=
  m.fold (fun acc _ v => acc + v) 0

#eval sumValues myMap  -- 8 (3 + 5)
</syntaxhighlight>

== 实际应用案例 ==

=== 词频统计 ===
<syntaxhighlight lang="lean">
import Std.Data.HashMap

def countWords (text : String) : Std.HashMap String Nat :=
  let words := text.splitOn " "
  words.foldl (fun map word => 
    map.insert word (map.findD word 0 + 1)
    Std.HashMap.empty

#eval countWords "hello world hello lean"
-- {hello => 2, world => 1, lean => 1}
</syntaxhighlight>

=== 配置管理系统 ===
<syntaxhighlight lang="lean">
def defaultConfig : Std.HashMap String String :=
  Std.HashMap.empty
    |>.insert "theme" "dark"
    |>.insert "font_size" "14"

def userConfig : Std.HashMap String String :=
  Std.HashMap.empty
    |>.insert "theme" "light"
    |>.insert "auto_save" "true"

-- 合并配置（用户配置覆盖默认值）
def finalConfig := defaultConfig.merge userConfig
</syntaxhighlight>

== 性能考虑 ==

* '''负载因子'''：哈希表的性能与填充程度密切相关，通常保持在0.7以下
* '''不可变vs可变'''：
  * 不可变映射适合函数式编程，支持持久化
  * 可变映射（如'''Std.RBMap'''）在需要频繁更新时效率更高
* '''键类型'''：必须实现正确的Hashable和BEq类型类

== 最佳实践 ==

1. 对于大型数据集，考虑使用'''Std.RBMap'''（基于红黑树）
2. 当需要频繁更新时，使用可变版本
3. 为自定义类型正确实现哈希函数
4. 使用'''findD'''提供默认值避免Option处理
5. 考虑使用'''fromList'''从列表直接构造映射

== 参见 ==

* Lean中的列表处理
* 自定义类型的哈希实现
* 持久化数据结构原理

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