编辑“︁Lean队列与栈”︁（章节）

= Lean队列与栈 =

== 简介 ==
'''队列（Queue）'''和'''栈（Stack）'''是两种基础但功能强大的数据结构，广泛应用于计算机科学和编程中。它们的主要区别在于数据的添加和移除顺序：

* '''队列'''遵循'''先进先出（FIFO, First In First Out）'''原则，即最先添加的元素最先被移除。
* '''栈'''遵循'''后进先出（LIFO, Last In First Out）'''原则，即最后添加的元素最先被移除。

在Lean中，队列和栈可以通过多种方式实现，包括使用内置的List类型或自定义结构。本文将详细介绍它们的实现、操作和应用场景。

== 队列（Queue） ==

=== 基本操作 ===
队列支持以下基本操作：
* '''enqueue'''：在队列尾部添加一个元素。
* '''dequeue'''：从队列头部移除并返回一个元素。
* '''peek'''：查看队列头部的元素但不移除它。
* '''isEmpty'''：检查队列是否为空。

=== Lean实现示例 ===
以下是一个简单的队列实现，使用Lean的`List`类型：

<syntaxhighlight lang="lean">
-- 定义队列结构
structure Queue (α : Type) where
  front : List α
  back : List α

-- 创建空队列
def Queue.empty : Queue α := ⟨[], []⟩

-- 检查队列是否为空
def Queue.isEmpty : Queue α → Bool
  | ⟨[], []⟩ => true
  | _        => false

-- 入队操作
def Queue.enqueue (q : Queue α) (x : α) : Queue α :=
  match q with
  | ⟨front, back⟩ => ⟨front, x :: back⟩

-- 出队操作
def Queue.dequeue : Queue α → Option (α × Queue α)
  | ⟨[], []⟩ => none
  | ⟨x :: xs, back⟩ => some (x, ⟨xs, back⟩)
  | ⟨[], back⟩ =>
    let front := back.reverse
    match front with
    | [] => none
    | x :: xs => some (x, ⟨xs, []⟩)

-- 示例使用
def exampleQueue : Queue Nat :=
  Queue.empty
  |> Queue.enqueue 1
  |> Queue.enqueue 2
  |> Queue.enqueue 3

-- 输出：some (1, _)
#eval Queue.dequeue exampleQueue
</syntaxhighlight>

=== 队列的可视化 ===
<mermaid>
graph LR
  A[1] --> B[2] --> C[3]
</mermaid>
这是一个包含元素1、2、3的队列。执行`dequeue`操作会移除并返回1。

== 栈（Stack） ==

=== 基本操作 ===
栈支持以下基本操作：
* '''push'''：在栈顶添加一个元素。
* '''pop'''：移除并返回栈顶的元素。
* '''peek'''：查看栈顶的元素但不移除它。
* '''isEmpty'''：检查栈是否为空。

=== Lean实现示例 ===
以下是一个简单的栈实现，使用Lean的`List`类型：

<syntaxhighlight lang="lean">
-- 定义栈结构
def Stack (α : Type) := List α

-- 创建空栈
def Stack.empty : Stack α := []

-- 检查栈是否为空
def Stack.isEmpty : Stack α → Bool
  | [] => true
  | _  => false

-- 入栈操作
def Stack.push (s : Stack α) (x : α) : Stack α :=
  x :: s

-- 出栈操作
def Stack.pop : Stack α → Option (α × Stack α)
  | [] => none
  | x :: xs => some (x, xs)

-- 示例使用
def exampleStack : Stack Nat :=
  Stack.empty
  |> Stack.push 1
  |> Stack.push 2
  |> Stack.push 3

-- 输出：some (3, _)
#eval Stack.pop exampleStack
</syntaxhighlight>

=== 栈的可视化 ===
<mermaid>
graph BT
  C[3] --> B[2] --> A[1]
</mermaid>
这是一个包含元素1、2、3的栈。执行`pop`操作会移除并返回3。

== 实际应用案例 ==

=== 队列的应用 ===
* '''任务调度'''：操作系统使用队列管理进程的执行顺序。
* '''广度优先搜索（BFS）'''：在图算法中，队列用于存储待访问的节点。

=== 栈的应用 ===
* '''函数调用'''：程序使用栈管理函数调用和返回地址。
* '''表达式求值'''：编译器使用栈解析数学表达式，如后缀表达式（逆波兰表示法）。

== 数学表示 ==
队列和栈的操作可以用数学符号表示：

* 队列的入队和出队：
  <math>\text{enqueue}(Q, x) = Q'</math>
  <math>\text{dequeue}(Q) = (x, Q')</math>

* 栈的入栈和出栈：
  <math>\text{push}(S, x) = S'</math>
  <math>\text{pop}(S) = (x, S')</math>

== 总结 ==
队列和栈是编程中不可或缺的数据结构，理解它们的特性和实现方式对编写高效、清晰的代码至关重要。在Lean中，它们可以通过`List`或其他自定义结构实现，并广泛应用于算法和系统设计中。

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