Lean队列与栈

Lean队列与栈

简介

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

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

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

队列（Queue）

基本操作

队列支持以下基本操作：

• enqueue：在队列尾部添加一个元素。
• dequeue：从队列头部移除并返回一个元素。
• peek：查看队列头部的元素但不移除它。
• isEmpty：检查队列是否为空。

Lean实现示例

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

-- 定义队列结构
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

队列的可视化

graph LR A[1] --> B[2] --> C[3]

这是一个包含元素1、2、3的队列。执行`dequeue`操作会移除并返回1。

栈（Stack）

基本操作

栈支持以下基本操作：

• push：在栈顶添加一个元素。
• pop：移除并返回栈顶的元素。
• peek：查看栈顶的元素但不移除它。
• isEmpty：检查栈是否为空。

Lean实现示例

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

-- 定义栈结构
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

栈的可视化

graph BT C[3] --> B[2] --> A[1]

这是一个包含元素1、2、3的栈。执行`pop`操作会移除并返回3。

实际应用案例

队列的应用

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

栈的应用

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

数学表示

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

• 队列的入队和出队：

 $\text{enqueue}(Q,x)=Q^{\prime }$
 $\text{dequeue}(Q)=(x,Q^{\prime })$

• 栈的入栈和出栈：

 $\text{push}(S,x)=S^{\prime }$
 $\text{pop}(S)=(x,S^{\prime })$

总结

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