Uniquep
Sometimes better than no-duplicatesp: first sorts the list and
then looks for adjacent duplicates.
- Signature
(uniquep x) → *
(uniquep x) is provably equal to (no-duplicatesp x), but
has different performance characteristics. It operates by sorting its argument
and then scanning for adjacent duplicates.
Note: we leave this function enabled. You should never write a theorem
about uniquep. Reason about no-duplicatesp instead.
Since we use a mergesort, the complexity of uniquep is O(n log n).
By comparison, no-duplicatesp is O(n^2).
It is not always better to use uniquep than no-duplicatesp:
- It uses far more memory than no-duplicatesp because it sorts the
list.
- On a list with lots of duplicates, no-duplicatesp may find a duplicate
very quickly and stop early, but uniquep has to sort the whole list before
it looks for any duplicates.
However, if your lists are sometimes long with few duplicates, uniquep
is probably a much better function to use.
Definitions and Theorems
Function: uniquep$inline
(defun uniquep$inline (x)
(declare (xargs :guard t))
(let ((__function__ 'uniquep))
(declare (ignorable __function__))
(mbe :logic (no-duplicatesp x)
:exec (no-adjacent-duplicates-p (<<-sort x)))))
Subtopics
- No-adjacent-duplicates-p
