• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • In
      • Defset
      • Primitives
      • Subset
      • Mergesort
        • Halve-list
        • Mergesort-exec
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Difference
      • Cardinality
      • Set
      • Double-containment
      • Intersectp
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/osets

Mergesort

(mergesort x) converts the list X into an ordered set.

Logically, (mergesort x) is exactly the same as repeated insertion, so it is fairly easy to reason about. But in the execution, mergesort is implemented with a reasonably efficient sort with O(n log n) performance instead of O(n^2) like repeated insertion.

Our implementation is probably not blisteringly fast. Folklore says we should switch to using a bubblesort when we get down to some threshold, say 40 elements. I'm not going to bother with any of that. If you find that the mergesort's performance is inadequate, which is unlikely, you can work on making it faster.

There are a few points of interest. If you look at the actual sort code, mergesort-exec, you will see that it is actually using the set library's own union function to perform the union. This is pretty slick because union is linear complexity, and yet is easy to reason about since we have already got a lot of theory in place about it.

In any case, our strategy for proving the equality of this mergesort with a simple insertion sort is the exact same trick we use everywhere else in the sets library. We begin by showing that both produce sets, and then show that membership in either is true exactly when an element is member-equal in the original list.

Definitions and Theorems

Function: mergesort

(defun mergesort (x)
       (declare (xargs :guard t))
       (mbe :logic (if (endp x)
                       nil
                       (insert (car x) (mergesort (cdr x))))
            :exec (mergesort-exec x)))

Theorem: mergesort-set

(defthm mergesort-set (setp (mergesort x)))

Theorem: in-mergesort

(defthm in-mergesort
        (equal (in a (mergesort x))
               (if (member a x) t nil)))

Theorem: mergesort-set-identity

(defthm mergesort-set-identity
        (implies (setp x)
                 (equal (mergesort x) x)))

Subtopics

Halve-list

How we split the list for mergesort.

Mergesort-exec

The implementation of mergesort.