Lean映射与字典

Lean映射与字典

介绍

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

映射与字典的核心特点是：

• 键的唯一性：每个键只能出现一次
• 高效的查找：通过哈希或树结构实现快速访问
• 可变/不可变版本：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

常见操作示例

-- 查找
#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

内部实现

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

哈希表实现

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

• 平均时间复杂度：
  • 插入：$O(1)$
  • 查找：$O(1)$
  • 删除：$O(1)$

持久化数据结构实现

对于不可变映射，Lean使用哈希数组映射尝试树（HAMT）：

graph TD Root --> L1[Level 1] Root --> L2[Level 2] L1 --> N1[Node] L1 --> N2[Node] N1 --> K1[Key1-Value1] N1 --> K2[Key2-Value2]

高级用法

合并映射

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

映射转换

-- 使用fold
def sumValues (m : Std.HashMap String Nat) : Nat :=
  m.fold (fun acc _ v => acc + v) 0

#eval sumValues myMap  -- 8 (3 + 5)

实际应用案例

词频统计

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}

配置管理系统

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

性能考虑

• 负载因子：哈希表的性能与填充程度密切相关，通常保持在0.7以下
• 不可变vs可变：

 * 不可变映射适合函数式编程，支持持久化
 * 可变映射（如Std.RBMap）在需要频繁更新时效率更高

• 键类型：必须实现正确的Hashable和BEq类型类

最佳实践

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

参见

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