A priority queue is an abstract data type with the following operations:

• empty: priqueue
• insert: key -> priqueue -> priqueue
• delete_max: priqueue -> option (key * priqueue)

The idea is that you can find (and remove) the highest-priority element. Priority queues have applications in:

• Discrete-event simulations: The highest-priority event is the one whose scheduled time is the earliest. Simulating one event causes new events to be scheduled in the future.
• Sorting: heap sort puts all the elements in a priority queue, then removes them one at a time.
• Computational geometry: algorithms such as convex hull use priority queues.
• Graph algorithms: Dijkstra's algorithm for finding the shortest path uses a priority queue.

We will be considering mergeable priority queues, with one additional operator:

• merge: priqueue -> priqueue -> priqueue

The classic data structure for priority queues is the "heap", a balanced binary tree in which the the key at any node is bigger than all the keys in nodes below it. With heaps, empty is constant time, insert and delete_max are logN time. But merge takes NlogN time, as one must take all the elements out of one queue and insert them into the other queue. Another way to do priority queues is by balanced binary search trees (such as red-black trees); again, empty is constant time, insert and delete_max are logN time, and merge takes NlogN time, as one must take all the elements out of one queue and insert them into the other queue. In the Binom chapter we will examine an algorithm in which empty is constant time, insert, delete_max, and merge are logN time. In this chapter we will consider a much simpler (and slower) implementation, using unsorted lists, in which:

• empty takes constant time
• insert takes constant time
• delete_max takes linear time
• merge takes linear time

Module Signature

This is the "signature" of a correct implementation of priority queues where the keys are natural numbers. Using nat for the key type is a bit silly, since the comparison function Nat.ltb takes linear time in the value of the numbers! But you have already seen in the Extract chapter how to define these kinds of algorithms on key types that have efficient comparisons, so in this chapter (and the Binom chapter) we simply won't worry about the time per comparison.

Take some time to consider whether this is the right specification! As always, if we get the specification wrong, then proofs of "correctness" are not so useful.

Implementation

Now we are responsible for providing Definitions of all those Parameters, and proving Theorems for all those Axioms, so that the values in the Module match the types in the Module Type. If we try to End List_Priqueue before everything is provided, we'll get an error. Uncomment the next line and try it!

Some Preliminaries

A copy of the select function from Selection.v, but getting the max element instead of the min element:

Exercise: 3 stars (select_perm_and_friends)

☐

The Program

Predicates on Priority Queues

The Representation Invariant

In this implementation of priority queues as unsorted lists, the representation invariant is trivial.

The abstraction relation is trivial too.

Sanity Checks on the Abstraction Relation

When the Abs relation says, "priority queue p contains elements al", it is free to report the elements in any order. It could even relate p to two different lists al and bl, as long as one is a permutation of the other.

Characterizations of the Operations on Queues

Exercise: 2 stars (simple_priq_proofs)

☐