左偏樹（leftist tree）

有些資料結構可以有效的存取任意元素，但有時候我們需要的只是高效存取最小的元素。支援這種存取模式的資料結構就叫做 priority queue 或是 heap。而 heap 經常用 heap-ordered tree 實作。

1. Heap-ordered

所謂 heap-ordered，就是每個節點的元素不大於其子節點的元素。在這個排序下，樹的最小元素總是在根節點。

2. 左偏樹

左偏樹的定義是滿足 leftist property 又符合 heap-ordered 的二元樹。

2.1. leftist property

任何左節點的 rank 都大於等於右邊兄弟節點的 rank。 rank 定義成 rightmost path 到空節點的距離。

3. 程式

左偏樹的核心結構定義是

\data Heap (A : \Set)
  | E
  | T Nat A (Heap A) (Heap A)

合併樹是左偏樹下最重要的實作，關鍵是保持兩顆樹符合左偏樹的定義

\func merge {A : Ord} (h1 h2 : Heap A) : Heap A
  | E, h => h
  | h, E => h
  | T _ x a1 b1 \as h1, T _ y a2 b2 \as h2 =>
    \case x <= y \with {
      | true => make-tree x a1 (merge b1 h2)
      | false => make-tree y a2 (merge h1 b2)
    }
  \where
    \func make-tree {A : \Set} (x : A) (left right : Heap A) : Heap A =>
      \case rank right <= rank left \with {
        | true => T (rank right + 1) x left right
        | false => T (rank left + 1) x right left
      }
    \func rank {A : \Set} (h : Heap A) : Nat
      | E => 0
      | T r _ _ _ => r

插入元素可以用 merge 實作

\func insert {A : Ord} (x : A) (h : Heap A) : Heap A => merge (T 1 x E E) h

搜尋最小元素或是刪除最小元素都可以仰賴左偏樹的特性，這裡找不到最小元素時是簡單的用 Maybe 型別包藏起來。

\func find-min {A : \Set} (h : Heap A) : Maybe A
  | E => nothing
  | T _ e _ _ => just e
\func delete-min {A : Ord} (h : Heap A) : Heap A
  | E => E
  | T _ _ l r => merge l r

檢查樹是不是空的非常的容易

\func empty? {A : \Set} (h : Heap A) : Bool
  | E => true
  | _ => false

3.1. Appendix

由於 Arend 並沒有提供程式上需要的偏序 Functor（倒是有證明用的偏序 Functor），所以需要自己定義一個

\class Ord (A : \Set)
  | \infix 6 <= : A -> A -> Bool

\func Nat<= (x y : Nat) : Bool
  | 0, n => true
  | n , 0 => false
  | suc n, suc m => Nat<= n m
\instance Nat-Ord : Ord Nat
  | <= => Nat<=

另外需要引入一些程式庫

\import Algebra.Monoid
\import Arith.Nat
\import Data.Bool
\import Data.Maybe