Example: Quicksort

Quicksort is a commonly employed sorting algorithm in practice. Given an array of n elements for some n > 0 and an ordering on these elements, the algorithm chooses one element in a more or less random fashion and then uses the chosen element as a pivot to shuffle the rest of the array into two parts separated by the pivot such that one part consists of all the elements that are less than or equal to the pivot (according to the given ordering) and the other part consists of the complement, that is, all the elements that are greater than the pivot; then the algorithm is applied recursively to each part unless it is empty. It is straightforward to see that the array is sorted after the algorithm terminates. In terms of time-complexity, quicksort is quadratic in the worst case and log-linear on average. Note that quicksort is not a stable sorting algorithm in the sense that the order of two equal elements may change after sorting.

The following function npivot returns the index of the element chosen to be the pivot:

fun{a:t@ype}
npivot {n:pos} {l:addr} (
  pf: !array_v (a, n, l) | p: ptr l, n: int (n), cmp: cmp (a)
) : natLt (n) = n/2

For simplicity, the index of the pivot for an array of size n is always n/2 (where integer division is used). Often a more elaborate method is to choose the index among 0, n/2 and n-1 such that the element stored at that index is between the elements stored at the other two indexes. Another possibility is to choose the index of the pivot based on a pseudo random number generator.

The function template array_ptr_exch for exchanging two elements in a given array is assgined the following interface:

extern
fun{a:t@ype}
array_ptr_exch {n:nat} {l:addr} (
  pf: !array_v (a, n, l) | p: ptr l, i: natLt n, j: natLt n
) : void // end of [array_ptr_exch]

I give no implementation of array_ptr_exch here as the reader should have no difficulty constructing one by now.

Given an array of elements, its size, an ordering on the elements and a pivot, the following function template split turns the array into two subarrays such that one subarray consists of all the elements in the array that are less than or equal to the pivot and the other subarray consists of the complement; it then returns the size of the first subarray plus proofs of the views of the two subarrays (as well as a proof for handling multiplication).

extern
fun{a:t@ype}
split {n:nat} {l:addr} (
  pf: array_v (a, n, l) | p: ptr l, n: int n, cmp: cmp a, piv: &a
) : [n1,n2:nat | n1+n2==n] [ofs:int] (
  MUL (n1, sizeof(a), ofs), array_v (a, n1, l), array_v (a, n2, l+ofs) | int n1
) // end of [split]

I postpone implementing split for the moment. Instead, let us first see an implementation of quicksort based on split:

fun{a:t@ype}
qsort {n:nat} {l:addr} .<n>. (
  pfarr: !array_v (a, n, l) | p: ptr l, n: int (n), cmp: cmp (a)
) : void =
  if n > 0 then let
    val tsz = int1_of_size1 (sizeof<a>)
    val npiv = npivot (pfarr | p, n, cmp)
    val () = array_ptr_exch (pfarr | p, 0, npiv) // move the pivot to the front
//
    val p1 = p+tsz
    prval array_v_cons (pfat, pf1arr) = pfarr
    val (pfmul, pf1arr_lte, pf1arr_gt | n1) = split (pf1arr | p1, n-1, cmp, !p)
// combining the pivot with the first segment
    prval pf1arr_lte = array_v_cons (pfat, pf1arr_lte)
// exchanging the pivot with the last element in the first segment
    val () = array_ptr_exch (pf1arr_lte | p, 0, n1)
// separating the pivot from all the elements in front of it
    prval (pf1arr_lte, pflast) = array_v_split {a} (pfmul, pf1arr_lte)
    val () = qsort (pf1arr_lte | p, n1, cmp) // recursive all to qsort
// combining the pivot with all the elements in front of it
    prval pf1arr_lte = array_v_unsplit {a} (pfmul, pf1arr_lte, pflast)
//
    val (pfmul_alt | ofs) = n1 imul2 tsz
    prval () = mul_isfun (pfmul, pfmul_alt)
    val () = qsort (pf1arr_gt | p1+ofs, n-n1-1, cmp) // recursive call to qsort
// combining the first and the second segments together
    prval () = pfarr := array_v_unsplit {a} (MULind (pfmul), pf1arr_lte, pf1arr_gt)
  in
    // nothing
  end else () // empty array
// end of [qsort]

The comments given in the implementation of qsort should make it reasonably clear as to how quicksort formally operates on a given array.

Let us now implement the function template split. Given an array, one common approach is to have two pointers pointing to the first and last elements of the array; the front pointer moves forward until an element that is not less than or equal to the pivot is encountered; the rear pointer moves backward until an element that is not greater than the pivot is encountered; the elements pointed to by the front and rear pointers are exchanged and the process is repeated; the process finishes at the moment when the front pointer either encounters or crosses over the rear one. As it is considerably involved to present an implementation based on this approach, I will use an alternative one, which I learned from the K&R book on the C programming language. This alternative approach starts with two pointers p1 and p2 pointing to the beginning of the given array and maintains the invariant that each element between p1 and p2 is greater than the pivot; first p2 moves forward until an element that is less than or equal to the pivot is encountered; then the elements stored at p1 and p2 are exchanged and both p1 and p2 move forward by one unit; the process repeats until p2 reaches the end of the array. For a slightly cleaner presentation, p1 is represented as a real pointer (p) in the implementation of the following inner function loop while p2 is represented as an integer (k):

implement{a}
split {n} (
  pfarr | p, n, cmp, piv
) = let
  fun loop
    {n1:nat}
    {k:nat | n1+k <= n}
    {l:addr} {ofs:int} .<n-n1-k>. (
    pfmul: MUL (n1, sizeof(a), ofs)
  , pf1arr: array_v (a, n1, l)
  , pf2arr: array_v (a, n-n1, l+ofs)
  | p: ptr (l+ofs), n: int n, n1: int n1, k: int k, cmp: cmp(a), piv: &a
  ) : [n1,n2:nat | n1+n2==n] [ofs:int] (
    MUL (n1, sizeof(a), ofs), array_v (a, n1, l), array_v (a, n2, l+ofs)
  | int (n1)
  ) = // [loop] is tail-recursive
    if n1+k < n then let
      val (pfat, fpf2 | pk) = array_ptr_takeout (pf2arr | p, k)
      val sgn = compare (!pk, piv, cmp)
      prval () = pf2arr := fpf2 (pfat)
    in
      if sgn > 0 then
        loop (pfmul, pf1arr, pf2arr | p, n, n1, k+1, cmp, piv)
      else let
        val () = array_ptr_exch (pf2arr | p, 0, k) // no work is done if k = 0
        prval array_v_cons (pfat, pf2arr) = pf2arr
        prval () = pf1arr := array_v_extend {a} (pfmul, pf1arr, pfat)
      in
        loop (MULind (pfmul), pf1arr, pf2arr | p+sizeof<a>, n, n1+1, k, cmp, piv)
      end (* end of [if] *)
    end else (
      pfmul, pf1arr, pf2arr | n1
    ) // end of [if]
in
  loop (MULbas (), array_v_nil (), pfarr | p, n, 0, 0, cmp, piv)
end // end of [split]

Note the proof function array_v_extend is given the following interface:

prfun array_v_extend
  {a:t@ype} {n:nat} {l:addr} {ofs:int} (
  pfmul: MUL (n, sizeof(a), ofs), pfarr: array_v (a, n, l), pfat: a @ l+ofs
) : array_v (a, n+1, l)

This proof function can be thought of as a special case of array_v_unsplit where the second array is a singleton, that is, it contains exactly one element.

Please find the entire code in this section plus some additional code for testing on-line.