BinomBinomial Queues
Required Reading
The Program
From Coq Require Import Strings.String. (* for manual grading *)
From VFA Require Import Perm.
From VFA Require Import Priqueue.
Module BinomQueue <: PRIQUEUE.
Definition key := nat.
Inductive tree : Type :=
| Node: key → tree → tree → tree
| Leaf : tree.
A priority queue (using the binomial queues data structure) is a
list of trees. The i'th element of the list is either Leaf or
it is a power-of-2-heap with exactly 2^i nodes.
This program will make sense to you if you've read the Sedgewick
reading; otherwise it is rather mysterious.
Definition priqueue := list tree.
Definition empty : priqueue := nil.
Definition smash (t u: tree) : tree :=
match t , u with
| Node x t1 Leaf, Node y u1 Leaf ⇒
if x >? y then Node x (Node y u1 t1) Leaf
else Node y (Node x t1 u1) Leaf
| _ , _ ⇒ Leaf (* arbitrary bogus tree *)
end.
Fixpoint carry (q: list tree) (t: tree) : list tree :=
match q, t with
| nil, Leaf ⇒ nil
| nil, _ ⇒ t :: nil
| Leaf :: q', _ ⇒ t :: q'
| u :: q', Leaf ⇒ u :: q'
| u :: q', _ ⇒ Leaf :: carry q' (smash t u)
end.
Definition insert (x: key) (q: priqueue) : priqueue :=
carry q (Node x Leaf Leaf).
Eval compute in fold_left (fun x q ⇒insert q x) [3;1;4;1;5;9;2;3;5] empty.
= [Node 5 Leaf Leaf; Leaf; Leaf; Node 9 (Node 4 (Node 3 (Node 1 Leaf Leaf) (Node 1 Leaf Leaf)) (Node 3 (Node 2 Leaf Leaf) (Node 5 Leaf Leaf))) Leaf] : priqueue
Fixpoint join (p q: priqueue) (c: tree) : priqueue :=
match p, q, c with
[], _ , _ ⇒ carry q c
| _, [], _ ⇒ carry p c
| Leaf::p', Leaf::q', _ ⇒ c :: join p' q' Leaf
| Leaf::p', q1::q', Leaf ⇒ q1 :: join p' q' Leaf
| Leaf::p', q1::q', Node _ _ _ ⇒ Leaf :: join p' q' (smash c q1)
| p1::p', Leaf::q', Leaf ⇒ p1 :: join p' q' Leaf
| p1::p', Leaf::q',Node _ _ _ ⇒ Leaf :: join p' q' (smash c p1)
| p1::p', q1::q', _ ⇒ c :: join p' q' (smash p1 q1)
end.
Fixpoint unzip (t: tree) (cont: priqueue → priqueue) : priqueue :=
match t with
| Node x t1 t2 ⇒ unzip t2 (fun q ⇒ Node x t1 Leaf :: cont q)
| Leaf ⇒ cont nil
end.
Definition heap_delete_max (t: tree) : priqueue :=
match t with
Node x t1 Leaf ⇒ unzip t1 (fun u ⇒ u)
| _ ⇒ nil (* bogus value for ill-formed or empty trees *)
end.
Fixpoint find_max' (current: key) (q: priqueue) : key :=
match q with
| [] ⇒ current
| Leaf::q' ⇒ find_max' current q'
| Node x _ _ :: q' ⇒ find_max' (if x >? current then x else current) q'
end.
Fixpoint find_max (q: priqueue) : option key :=
match q with
| [] ⇒ None
| Leaf::q' ⇒ find_max q'
| Node x _ _ :: q' ⇒ Some (find_max' x q')
end.
Fixpoint delete_max_aux (m: key) (p: priqueue) : priqueue × priqueue :=
match p with
| Leaf :: p' ⇒ let (j,k) := delete_max_aux m p' in (Leaf::j, k)
| Node x t1 Leaf :: p' ⇒
if m >? x
then (let (j,k) := delete_max_aux m p'
in (Node x t1 Leaf::j,k))
else (Leaf::p', heap_delete_max (Node x t1 Leaf))
| _ ⇒ (nil, nil) (* Bogus value *)
end.
Definition delete_max (q: priqueue) : option (key × priqueue) :=
match find_max q with
| None ⇒ None
| Some m ⇒ let (p',q') := delete_max_aux m q
in Some (m, join p' q' Leaf)
end.
Definition merge (p q: priqueue) := join p q Leaf.
Fixpoint pow2heap' (n: nat) (m: key) (t: tree) :=
match n, m, t with
0, m, Leaf ⇒ True
| 0, m, Node _ _ _ ⇒ False
| S _, m,Leaf ⇒ False
| S n', m, Node k l r ⇒
m ≥ k ∧ pow2heap' n' k l ∧ pow2heap' n' m r
end.
t is a power-of-2 heap of depth n
Definition pow2heap (n: nat) (t: tree) :=
match t with
Node m t1 Leaf ⇒ pow2heap' n m t1
| _ ⇒ False
end.
l is the ith tail of a binomial heap
Fixpoint priq' (i: nat) (l: list tree) : Prop :=
match l with
| t :: l' ⇒ (t=Leaf ∨ pow2heap i t) ∧ priq' (S i) l'
| nil ⇒ True
end.
q is a binomial heap
Proof of Algorithm Correctness
Various Functions Preserve the Representation Invariant
Exercise: 1 star, standard (empty_priq)
Theorem smash_valid:
∀ n t u, pow2heap n t → pow2heap n u → pow2heap (S n) (smash t u).
(* FILL IN HERE *) Admitted.
☐
∀ n t u, pow2heap n t → pow2heap n u → pow2heap (S n) (smash t u).
(* FILL IN HERE *) Admitted.
☐
Theorem carry_valid:
∀ n q, priq' n q →
∀ t, (t=Leaf ∨ pow2heap n t) → priq' n (carry q t).
(* FILL IN HERE *) Admitted.
☐
∀ n q, priq' n q →
∀ t, (t=Leaf ∨ pow2heap n t) → priq' n (carry q t).
(* FILL IN HERE *) Admitted.
☐
(* This proof is rather long, but each step is reasonably straightforward.
There's just one induction to do, right at the beginning. *)
Theorem join_valid: ∀ p q c n, priq' n p → priq' n q → (c=Leaf ∨ pow2heap n c) → priq' n (join p q c).
(* FILL IN HERE *) Admitted.
☐
There's just one induction to do, right at the beginning. *)
Theorem join_valid: ∀ p q c n, priq' n p → priq' n q → (c=Leaf ∨ pow2heap n c) → priq' n (join p q c).
(* FILL IN HERE *) Admitted.
☐
Theorem merge_priq: ∀ p q, priq p → priq q → priq (merge p q).
Proof.
intros. unfold merge. apply join_valid; auto.
Qed.
Theorem delete_max_Some_priq:
∀ p q k, priq p → delete_max p = Some(k,q) → priq q.
(* FILL IN HERE *) Admitted.
☐
∀ p q k, priq p → delete_max p = Some(k,q) → priq q.
(* FILL IN HERE *) Admitted.
☐
The Abstraction Relation
Inductive tree_elems: tree → list key → Prop :=
| tree_elems_leaf: tree_elems Leaf nil
| tree_elems_node: ∀ bl br v tl tr b,
tree_elems tl bl →
tree_elems tr br →
Permutation b (v::bl++br) →
tree_elems (Node v tl tr) b.
Exercise: 3 stars, standard (priqueue_elems)
Make an inductive definition, similar to tree_elems, to relate a priority queue "l" to a list of all its elements.Inductive priqueue_elems: list tree → list key → Prop :=
(* FILL IN HERE *)
.
(* Do not modify the following line: *)
Definition manual_grade_for_priqueue_elems : option (nat×string) := None.
☐
Sanity Checks on the Abstraction Relation
Exercise: 2 stars, standard (tree_elems_ext)
Extensionality theorem for the tree_elems relationTheorem tree_elems_ext: ∀ t e1 e2,
Permutation e1 e2 → tree_elems t e1 → tree_elems t e2.
(* FILL IN HERE *) Admitted.
☐
Theorem tree_perm: ∀ t e1 e2,
tree_elems t e1 → tree_elems t e2 → Permutation e1 e2.
(* FILL IN HERE *) Admitted.
☐
tree_elems t e1 → tree_elems t e2 → Permutation e1 e2.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (priqueue_elems_ext)
To prove priqueue_elems_ext, you should almost be able to cut-and-paste the proof of tree_elems_ext, with just a few edits.Theorem priqueue_elems_ext: ∀ q e1 e2,
Permutation e1 e2 → priqueue_elems q e1 → priqueue_elems q e2.
(* FILL IN HERE *) Admitted.
☐
Theorem abs_perm: ∀ p al bl,
priq p → Abs p al → Abs p bl → Permutation al bl.
Proof.
(* FILL IN HERE *) Admitted.
☐
priq p → Abs p al → Abs p bl → Permutation al bl.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma tree_can_relate: ∀ t, ∃ al, tree_elems t al.
Proof.
(* FILL IN HERE *) Admitted.
Theorem can_relate: ∀ p, priq p → ∃ al, Abs p al.
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof.
(* FILL IN HERE *) Admitted.
Theorem can_relate: ∀ p, priq p → ∃ al, Abs p al.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem smash_elems: ∀ n t u bt bu,
pow2heap n t → pow2heap n u →
tree_elems t bt → tree_elems u bu →
tree_elems (smash t u) (bt ++ bu).
(* FILL IN HERE *) Admitted.
☐
Optional Exercises
Exercise: 4 stars, standard, optional (carry_elems)
Theorem carry_elems:
∀ n q, priq' n q →
∀ t, (t=Leaf ∨ pow2heap n t) →
∀ eq et, priqueue_elems q eq →
tree_elems t et →
priqueue_elems (carry q t) (eq++et).
(* FILL IN HERE *) Admitted.
☐
∀ n q, priq' n q →
∀ t, (t=Leaf ∨ pow2heap n t) →
∀ eq et, priqueue_elems q eq →
tree_elems t et →
priqueue_elems (carry q t) (eq++et).
(* FILL IN HERE *) Admitted.
☐
Theorem insert_relate:
∀ p al k, priq p → Abs p al → Abs (insert k p) (k::al).
(* FILL IN HERE *) Admitted.
☐
∀ p al k, priq p → Abs p al → Abs (insert k p) (k::al).
(* FILL IN HERE *) Admitted.
☐
Theorem join_elems:
∀ p q c n,
priq' n p →
priq' n q →
(c=Leaf ∨ pow2heap n c) →
∀ pe qe ce,
priqueue_elems p pe →
priqueue_elems q qe →
tree_elems c ce →
priqueue_elems (join p q c) (ce++pe++qe).
(* FILL IN HERE *) Admitted.
☐
∀ p q c n,
priq' n p →
priq' n q →
(c=Leaf ∨ pow2heap n c) →
∀ pe qe ce,
priqueue_elems p pe →
priqueue_elems q qe →
tree_elems c ce →
priqueue_elems (join p q c) (ce++pe++qe).
(* FILL IN HERE *) Admitted.
☐
Theorem merge_relate:
∀ p q pl ql al,
priq p → priq q →
Abs p pl → Abs q ql → Abs (merge p q) al →
Permutation al (pl++ql).
Proof.
(* FILL IN HERE *) Admitted.
☐
∀ p q pl ql al,
priq p → priq q →
Abs p pl → Abs q ql → Abs (merge p q) al →
Permutation al (pl++ql).
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem delete_max_None_relate:
∀ p, priq p → (Abs p nil ↔ delete_max p = None).
(* FILL IN HERE *) Admitted.
☐
∀ p, priq p → (Abs p nil ↔ delete_max p = None).
(* FILL IN HERE *) Admitted.
☐
Theorem delete_max_Some_relate:
∀ (p q: priqueue) k (pl ql: list key), priq p →
Abs p pl →
delete_max p = Some (k,q) →
Abs q ql →
Permutation pl (k::ql) ∧ Forall (ge k) ql.
(* FILL IN HERE *) Admitted.
☐
∀ (p q: priqueue) k (pl ql: list key), priq p →
Abs p pl →
delete_max p = Some (k,q) →
Abs q ql →
Permutation pl (k::ql) ∧ Forall (ge k) ql.
(* FILL IN HERE *) Admitted.
☐
Measurement.
Exercise: 5 stars, standard, optional (binom_measurement)
Adapt the program (but not necessarily the proof) to use Ocaml integers as keys, in the style shown in Extract. Write an ML program to exercise it with random inputs. Compare the runtime to the implementation from Priqueue, also adapted for Ocaml integers. ☐(* 2021-05-04 07:54 *)