编辑“︁Lean树结构”︁

= Lean树结构 =

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

== 基本概念 ==

树是由'''节点'''（nodes）和'''边'''（edges）组成的非线性数据结构，满足以下性质：
* 每个树有且仅有一个'''根节点'''（root）
* 除根节点外，每个节点有且仅有一个'''父节点'''
* 从根节点到任意节点有且仅有一条路径

数学上，树可以递归地定义为：
<math>T = \begin{cases}
\emptyset & \text{(空树)} \\
(r, \{T_1, T_2, ..., T_n\}) & \text{(根节点r和子树集合)}
\end{cases}</math>

== Lean中的树实现 ==

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

<syntaxhighlight lang="lean">
inductive BinaryTree (α : Type) where
  | leaf : BinaryTree α
  | node : BinaryTree α → α → BinaryTree α → BinaryTree α
</syntaxhighlight>

'''解释'''：
* <code>leaf</code> 表示空树
* <code>node</code> 包含左子树、节点值和右子树
* <code>α</code> 是泛型参数，允许存储任意类型数据

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

<syntaxhighlight lang="lean">
inductive Tree (α : Type) where
  | node : α → List (Tree α) → Tree α
</syntaxhighlight>

== 基本操作 ==

=== 树的高度计算 ===
递归计算树的最大深度：

<syntaxhighlight lang="lean">
def BinaryTree.depth : BinaryTree α → Nat
  | leaf => 0
  | node l _ r => max (depth l) (depth r) + 1
</syntaxhighlight>

'''示例'''：
输入：<code>node (node leaf 1 leaf) 2 (node leaf 3 leaf)</code><br>
输出：<code>2</code>

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

<syntaxhighlight lang="lean">
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]
</syntaxhighlight>

== 可视化表示 ==

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

上述图表对应示例二叉树：
* 根节点：2
* 左子节点：1
* 右子节点：3

== 应用案例 ==

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

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

'''示例计算''' <code>(2+3)*4</code>：
<syntaxhighlight lang="lean">
def sampleExpr := Expr.times (Expr.plus (Expr.const 2) (Expr.const 3)) (Expr.const 4)
#eval eval sampleExpr  -- 输出：20
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 高级主题 ==

=== 平衡二叉树 ===
保证操作效率的重要数据结构，如AVL树：

<syntaxhighlight lang="lean">
structure AVLNode (α : Type) where
  value : α
  left : AVLTree α
  right : AVLTree α
  height : Nat

inductive AVLTree (α : Type) where
  | empty : AVLTree α
  | node : AVLNode α → AVLTree α
</syntaxhighlight>

平衡因子计算公式：
<math>\text{balance\_factor} = \text{height}(left) - \text{height}(right)</math>

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

<syntaxhighlight lang="lean">
inductive Color where | red | black

inductive RBTree (α : Type) where
  | empty : RBTree α
  | node : Color → RBTree α → α → RBTree α → RBTree α
</syntaxhighlight>

== 性能分析 ==

常见树操作的渐近复杂度：
{| class="wikitable"
|-
! 操作 !! 平均情况 !! 最坏情况
|-
| 查找 || <math>O(\log n)</math> || <math>O(n)</math>
|-
| 插入 || <math>O(\log n)</math> || <math>O(n)</math>
|-
| 删除 || <math>O(\log n)</math> || <math>O(n)</math>
|}

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

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

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

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