Lean树结构

Lean树结构

Lean树结构是函数式编程和定理证明中常用的递归数据结构，用于表示层次化的数据关系。在Lean编程语言中，树结构通常通过归纳类型（inductive types）定义，并广泛应用于算法设计、数学证明和数据处理领域。

基本概念

树是由节点（nodes）和边（edges）组成的非线性数据结构，满足以下性质：

• 每个树有且仅有一个根节点（root）
• 除根节点外，每个节点有且仅有一个父节点
• 从根节点到任意节点有且仅有一条路径

数学上，树可以递归地定义为： $T=\{\begin{array}{ll}\mathrm{\varnothing }& \text{(空树)}\\ (r,\{T_1,T_2,...,T_n\})& \text{(根节点r和子树集合)}\end{array}$

Lean中的树实现

二叉树定义

最基础的树结构是二叉树，在Lean 4中可定义为：

inductive BinaryTree (α : Type) where
  | leaf : BinaryTree α
  | node : BinaryTree α → α → BinaryTree α → BinaryTree α

解释：

• leaf 表示空树
• node 包含左子树、节点值和右子树
• α 是泛型参数，允许存储任意类型数据

多叉树定义

对于子节点数量不固定的情况，可以使用列表存储子树：

inductive Tree (α : Type) where
  | node : α → List (Tree α) → Tree α

基本操作

树的高度计算

递归计算树的最大深度：

def BinaryTree.depth : BinaryTree α → Nat
  | leaf => 0
  | node l _ r => max (depth l) (depth r) + 1

示例： 输入：node (node leaf 1 leaf) 2 (node leaf 3 leaf)
输出：2

树的遍历

三种经典遍历方式的实现：

def BinaryTree.inOrder : BinaryTree α → List α
  | leaf => []
  | node l x r => inOrder l ++ [x] ++ inOrder r

def BinaryTree.preOrder : BinaryTree α → List α
  | leaf => []
  | node l x r => [x] ++ preOrder l ++ preOrder r

def BinaryTree.postOrder : BinaryTree α → List α
  | leaf => []
  | node l x r => postOrder l ++ postOrder r ++ [x]

可视化表示

graph TD A[2] --> B[1] A --> C[3] B --> D[null] B --> E[null] C --> F[null] C --> G[null]

上述图表对应示例二叉树：

• 根节点：2
• 左子节点：1
• 右子节点：3

应用案例

表达式树

在编译器设计中，算术表达式可以表示为树结构：

inductive Expr where
  | const : Nat → Expr
  | plus : Expr → Expr → Expr
  | times : Expr → Expr → Expr

def eval : Expr → Nat
  | Expr.const n => n
  | Expr.plus a b => eval a + eval b
  | Expr.times a b => eval a * eval b

示例计算 (2+3)*4：

def sampleExpr := Expr.times (Expr.plus (Expr.const 2) (Expr.const 3)) (Expr.const 4)
#eval eval sampleExpr  -- 输出：20

决策树

机器学习中的简单决策树实现：

inductive DecisionTree (α β : Type) where
  | answer : β → DecisionTree α β
  | question : (α → Bool) → DecisionTree α β → DecisionTree α β → DecisionTree α β

def classify (dt : DecisionTree α β) (input : α) : β :=
  match dt with
  | DecisionTree.answer b => b
  | DecisionTree.question f yes no => 
      if f input then classify yes input else classify no input

高级主题

平衡二叉树

保证操作效率的重要数据结构，如AVL树：

structure AVLNode (α : Type) where
  value : α
  left : AVLTree α
  right : AVLTree α
  height : Nat

inductive AVLTree (α : Type) where
  | empty : AVLTree α
  | node : AVLNode α → AVLTree α

平衡因子计算公式： 解析失败 (语法错误): {\displaystyle \text{balance\_factor} = \text{height}(left) - \text{height}(right)}

红黑树

另一种自平衡二叉搜索树，在Lean标准库中有实际应用：

inductive Color where | red | black

inductive RBTree (α : Type) where
  | empty : RBTree α
  | node : Color → RBTree α → α → RBTree α → RBTree α

性能分析

常见树操作的渐近复杂度：

操作	平均情况	最坏情况
查找	$O(\log n)$	$O(n)$
插入	$O(\log n)$	$O(n)$
删除	$O(\log n)$	$O(n)$

对于平衡树（如AVL、红黑树），最坏情况也能保持$O(\log n)$复杂度。

练习建议

1. 实现二叉树镜像翻转 2. 编写计算树节点数量的函数 3. 实现二叉搜索树的查找操作 4. 尝试序列化和反序列化树结构 5. 扩展多叉树实现文件系统目录结构

参见

• 递归数据类型
• 图论基础
• 算法复杂度分析
• 模式匹配与递归