		Search-engine friendly clone of the ACL2 documentation.

Mergesort

Halve-list

How we split the list for mergesort.

Originally I used the following function to split the list.

(defun split-list-old (x)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) (mv nil nil))
        ((endp (cdr x)) (mv (list (car x)) nil))
        (t (mv-let (part1 part2)
                   (split-list-old (cddr x))
                   (mv (cons (car x) part1)
                       (cons (cadr x) part2)))))))

But David Rager noted that this was not tail recursive, and accordingly it ran into trouble on large data sets. Accordingly, in Version 0.91, I rewrote this to be tail recursive:

(defun split-list (x acc acc2)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x)
         (mv acc acc2))
        ((endp (cdr x))
         (mv (cons (car x) acc) acc2))
        (t (split-list (cddr x)
                       (cons (car x) acc)
                       (cons (cadr x) acc2)))))

Since then, I wrote the defsort/defsort library, which uses some tricks to provide a faster mergesort. One key optimization is to take the first and second halves of the list, rather than splitting the list in terms of evens and odds. This allows you to split the list with half as much consing.

Defsort's approach uses a lot of arithmetic optimization. I later wrote a mergesort for Milawa, where arithmetic is expensive. Here, I implemented split-list by walking down "one cdr" and "two cdrs" at a time. I now use this same strategy in osets.

BOZO this strategy is still stupidly re-consing up half the list, when really we could avoid that by just being a bit smarter, like in defsort.

Definitions and Theorems

Function: halve-list-aux

(defun halve-list-aux (mid x acc)
       (declare (xargs :guard (<= (len x) (len mid))))
       (if (or (atom x) (atom (cdr x)))
           (mv acc mid)
           (halve-list-aux (cdr mid)
                           (cdr (cdr x))
                           (cons (car mid) acc))))

Function: halve-list

(defun halve-list (x)
       (declare (xargs :guard t))
       (halve-list-aux x x nil))