编辑“︁Lean优先队列”︁

= Lean优先队列 =

'''优先队列'''（Priority Queue）是一种抽象数据类型，它允许我们以优先级顺序存储和检索元素。在Lean中，优先队列通常基于堆（Heap）数据结构实现，确保最高优先级的元素始终位于队列前端。与普通队列的先进先出（FIFO）规则不同，优先队列遵循'''最高优先级先出'''（Highest-Priority-First）的原则。

== 基本概念 ==

优先队列的核心操作包括：
* '''插入（Insert）'''：将元素添加到队列中，并根据其优先级调整位置。
* '''提取最大值/最小值（Extract-Max/Extract-Min）'''：移除并返回优先级最高或最低的元素。
* '''查看最大值/最小值（Peek）'''：返回但不移除优先级最高或最低的元素。

在Lean中，优先队列可以基于以下结构实现：
* '''二叉堆'''（Binary Heap）
* '''斐波那契堆'''（Fibonacci Heap）
* '''配对堆'''（Pairing Heap）

== Lean中的实现 ==

以下是一个基于二叉堆的Lean优先队列实现示例：

<syntaxhighlight lang="lean">
-- 定义优先队列结构
structure PriorityQueue (α : Type) [LE α] where
  heap : List α
  deriving Repr

-- 空优先队列
def PriorityQueue.empty : PriorityQueue α :=
  { heap := [] }

-- 插入元素
def PriorityQueue.insert (pq : PriorityQueue α) (x : α) : PriorityQueue α :=
  let newHeap := x :: pq.heap
  { heap := bubbleUp newHeap (newHeap.length - 1) }

-- 辅助函数：上浮操作
def bubbleUp (heap : List α) (idx : Nat) : List α :=
  match idx with
  | 0 => heap
  | i+1 =>
    let parentIdx := (i - 1) / 2
    if heap[i] ≤ heap[parentIdx] then heap
    else
      let swapped := heap.swap i parentIdx
      bubbleUp swapped parentIdx
</syntaxhighlight>

=== 操作示例 ===
输入：
<syntaxhighlight lang="lean">
let pq := PriorityQueue.empty
let pq := pq.insert 5
let pq := pq.insert 3
let pq := pq.insert 8
</syntaxhighlight>

输出队列内部表示：
<pre>
{ heap := [8, 3, 5] }
</pre>

== 时间复杂度分析 ==

优先队列操作的渐进时间复杂度如下：

{| class="wikitable"
|-
! 操作 !! 时间复杂度
|-
| 插入 || <math>O(\log n)</math>
|-
| 提取最大值 || <math>O(\log n)</math>
|-
| 查看最大值 || <math>O(1)</math>
|}

== 可视化表示 ==

以下是一个二叉堆的mermaid图表表示：

<mermaid>
graph TD
    8 --> 3
    8 --> 5
    3 --> 1
    3 --> 2
</mermaid>

== 实际应用案例 ==

优先队列在多种算法和系统中有着广泛应用：

1. '''Dijkstra最短路径算法'''：使用优先队列高效选择下一个要处理的节点
2. '''Huffman编码'''：构建最优前缀码时使用优先队列
3. '''操作系统调度'''：按优先级调度进程
4. '''事件驱动模拟'''：按时间顺序处理事件

=== 案例：任务调度 ===
假设我们需要按优先级处理任务：

<syntaxhighlight lang="lean">
def Task := String × Nat  -- (描述, 优先级)

def scheduleTasks (tasks : List Task) : List String :=
  let pq := tasks.foldl (fun pq (desc, prio) => pq.insert (prio, desc)) PriorityQueue.empty
  List.range tasks.length |>.map fun _ =>
    match pq.extractMax with
    | (some (_, desc), newPq) => (desc, newPq)
    | (none, _) => panic! "队列为空"
</syntaxhighlight>

== 进阶主题 ==

对于更高级的用户，Lean优先队列还可以探讨：

* '''延迟合并'''（Lazy Merging）技术
* '''可持久化优先队列'''（Persistent Priority Queue）
* '''并行优先队列'''实现
* '''验证优先队列性质'''的形式化证明

== 总结 ==

Lean中的优先队列提供了高效管理优先级元素的能力，是算法设计和系统实现中的重要工具。通过二叉堆等实现，它保证了核心操作的对数时间复杂度。理解优先队列不仅有助于学习Lean数据结构，也为解决实际问题提供了有力工具。

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