Std.Queue (キュー) を紹介する

[Seasawher]

Std に存在する。あまり定理などは用意されていないようだが…。

https://leanprover-community.github.io/mathlib4_docs/Init/Data/Queue.html#Std.Queue

[Seasawher]

Std.Queue α は 永続的・関数型な FIFO キューです。内部的には 2 本の List で実装されています。

structure Std.Queue (α : Type u) where
eList : List α
dList : List α

意味はだいたい：

キューの中身 = dList ++ eList.reverse

dList は次に取り出す側、eList は追加された要素を逆順に溜める側です。公式ドキュメントも「two back-to-back lists」と説明しています。 

基本操作はこれです。

import Std
open Std
#eval (∅ : Queue Nat).isEmpty
-- true
#eval ((∅ : Queue Nat).enqueue 10).enqueue 20 |>.toArray
-- #[10, 20]
#eval (((∅ : Queue Nat).enqueue 10).enqueue 20).dequeue?
-- some (10, ...)

注意点は、enqueue の引数順です。

def Queue.enqueue (v : α) (q : Queue α) : Queue α

つまり、

q.enqueue 10

と書くと、ドット記法により実際には

Queue.enqueue 10 q

になります。

dequeue? は空なら none、空でなければ「取り出した値」と「残りのキュー」を返します。

def popTwo : Option (Nat × Nat) := do
let q := ((∅ : Queue Nat).enqueue 10).enqueue 20
let (x, q) ← q.dequeue?
let (y, _) ← q.dequeue?
return (x, y)
#eval popTwo
-- some (10, 20)

計算量は、enqueue が O(1)、dequeue? が償却 O(1)・最悪 O(n) です。dList が空になったときだけ eList.reverse が走るためです。 

要するに、Std.Queue は「取り出し順を保ちたいが、純粋関数型で Array.push + 先頭削除みたいな非効率を避けたい」ときに使うものです。BFS、タスクキュー、逐次処理待ちリストなどに向いています。