acl2-books-source 6.3-5 / usr / share / acl2-6.3 / books / leftist-trees / leftist-tree-defuns.lisp

#|

   Leftist Trees, Version 0.1
   Copyright (C) 2012 by Ben Selfridge <benself@cs.utexas.edu>

 leftist-tree-defuns.lisp

   This file contains the function definitions and lays out
   the structure of leftist trees (otherwise known as leftist
   heaps). With an eye towards heapsort, we use lexorder as
   the basic ordering function, since that is the ordering
   used in the other sorting algorithms in books/sorting.

   This implementation follows "Purely Functional Data
   Structures" by Chris Okasaki.

|#

(in-package "ACL2")

(deflabel leftist-trees :doc ":DOC-SECTION leftist-trees

An implementation of Leftist Trees.  ~/~/

Leftist trees are an efficient implementation of binary heaps. Regular
(completely balanced) binary heaps are tricky, and in most cases near
impossible, to implement in functional languages because of the need
for constant-time access to the last element in the tree (that element
being the node in the bottom-most level of the tree, furthest to the
right). Leftist trees avoid this by replacing this \"balanced\"
requirement with the requirement that the right-most spine of the tree
be small relative to the overal number of elements in the tree. Since
the fundamental heap operations (insert, delete-min) only recur on the
right spine of the tree in question, this guarantees that these
operations are O(log(n)), where n is the size of the tree.

Leftist trees look like this:

    (rank root left right)

where \"rank\" is defined to be the length of the right spine of the
tree, \"root\" is the root element of the tree, \"left\" is the left
sub-tree, and \"right\" is the right sub-tree.

Leftist trees are heap-ordered, and they are \"balanced\" in a loose
sense. In particular, the size of the tree is at least as big as an
exponential function of the rank:

    size(tree) >= 2^(rank(tree)) - 1,

or, solving for rank(tree) and noting that the rank is always an
integer,

    rank(tree) <= floor(log(size(tree) + 1)).

The important tree operations are INSERT-LT, FIND-MIN-LT, and
DELETE-MIN-LT. A useful function called BUILD-LT is also provided,
which constructs a leftist tree from a list. An important constant is
*EMPTY-LT*, which is the empty tree (for this implementation, just
NIL).

To learn how to use the trees, see :DOC LEFTIST-TREE-FNS. To see some
useful theorems about leftist trees, including the rank bound above,
see :DOC LEFTIST-TREE-THMS. 

Sources: 
  - Okasaki, Chris. Purely Functional Data Structures. Cambridge,
    U.K.: Cambridge UP, 1998. 17-20. Print.  

~/
")

(defdoc leftist-tree-fns
  ":doc-section leftist-trees
All functions and constants related to leftist trees.~/~/
------------------------------------------------------------
Functions and Constants
------------------------------------------------------------

Function/Constant Name      Result
  (supporting function)     Type
----------------------      ----

** STRUCTURE **
RANK-LT                     natural
ROOT-LT                     ?
LEFT-LT                     ltree
RIGHT-LT                    ltree
*EMPTY-LT*                  NIL
IS-EMPTY-LT                 boolean
PROPER-LT                   boolean

** OPERATIONS **
MERGE-LT                    ltree
  MAKE-LT                   ltree
INSERT-LT                   ltree
FIND-MIN-LT                 ?
DELETE-MIN-LT               ltree
BUILD-LT                    ltree

** MISCELLANEOUS **
SIZE-LT                     natural
MEMBER-LT                   boolean
LENGTH-RIGHT-SPINE-LT       natural
LENGTH-TO-NIL-LT            natural
~/")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; STRUCTURE OF LEFTIST TREES ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defdoc leftist-tree-structure
  ":doc-section leftist-tree-fns
Functions relating to building and recognizing leftist trees.
~/~/
~/")

(defun rank-lt (tree)
  ":doc-section leftist-tree-structure
rank of a leftist tree~/~/
Returns the rank of the tree. The rank of a tree is formally defined
to be the length of its right spine. Empty trees have rank 0.~/"
  (if (atom tree)
      0
    (car tree)))

(defun root-lt (tree)
  ":doc-section leftist-tree-structure
root of a leftist tree~/~/
Returns the root of a non-empty tree.~/"
  (cadr tree))

(defun left-lt (tree)
  ":doc-section leftist-tree-structure
left sub-tree of a leftist tree~/~/
Returns the left sub-tree of a non-empty tree.~/"
  (caddr tree))

(defun right-lt (tree)
  ":doc-section leftist-tree-structure
right sub-tree of a leftist tree~/~/
Returns the right sub-tree of a non-empty tree.~/"  
  (cadddr tree))

(defconst *empty-lt* NIL
  ":doc-section leftist-tree-structure
the default empty leftist tree~/~/
The default \"empty\" tree (just NIL)~/"
)

(defun is-empty-lt (tree) 
  ":doc-section leftist-tree-structure
checks if a tree is empty~/~/
Checks if a tree is empty. For simplicity, we only require (atom
tree).~/" 
  (atom tree))

(defun proper-lt (tree)
  ":doc-section leftist-tree-structure
checks that a tree is a legitimate leftist tree~/~/
Checks that a tree is a legitimate Leftist Tree.
The basic recursive requirements are:
    * both the left and right sub-trees are proper
    * (rank) the rank is 1 + the rank of the right sub-tree
    * (leftist) the rank of right sub-tree is less than or
      equal to the rank of the left sub-tree
    * (heap-ordered) if either of the sub-trees are non-trivial,
      then their roots are larger than the root of the tree
~/"
  (if (is-empty-lt tree)
      (and (null tree)
	   (equal (rank-lt tree) 0))
    (and (proper-lt (left-lt tree))
         (proper-lt (right-lt tree))
         (equal (rank-lt tree)
                (+ 1 (rank-lt (right-lt tree))))
         (<= (rank-lt (right-lt tree))
             (rank-lt (left-lt tree)))
         (implies (consp (left-lt tree))
                  (lexorder (root-lt tree) 
                            (root-lt (left-lt tree))))
         (implies (consp (right-lt tree))
                  (lexorder (root-lt tree)
                            (root-lt (right-lt tree)))))))

;;;;;;;;;;;;;;;;;;;;;
;; HEAP OPERATIONS ;;
;;;;;;;;;;;;;;;;;;;;;

(defdoc leftist-tree-ops
  ":doc-section leftist-tree-fns
The basic heap operations of leftist trees.~/~/
The core operation here is MERGE-LT. All the other operations are
defined in terms of MERGE-LT, which makes leftist trees relatively
easy to reason about.~/")

(defun make-lt (x a b)
  (if (<= (rank-lt b) (rank-lt a))
      (list (+ 1 (rank-lt b)) x a b)
    (list (+ 1 (rank-lt a)) x b a)))

(defun merge-lt (tree1 tree2)
  ":doc-section leftist-tree-ops
merge two leftist trees~/~/
Merge two leftist trees.

Two leftist trees are merged by \"merging their right spines as you
would merge two sorted lists, and then swapping the children of nodes
along this path as necessary to restore the leftist property.\"
(Okasaki)~/"
  (declare (xargs :measure (+ (acl2-count tree1)
                              (acl2-count tree2))))
  (cond ((is-empty-lt tree2) tree1)
        ((is-empty-lt tree1) tree2)
        (t (if (lexorder (root-lt tree1) (root-lt tree2))
               (make-lt (root-lt tree1)
                        (left-lt tree1)
                        (merge-lt (right-lt tree1) tree2))
             (make-lt (root-lt tree2)
                      (left-lt tree2)
                      (merge-lt tree1 (right-lt tree2)))))))

(defun insert-lt (x tree)
  ":doc-section leftist-tree-ops
insert an element into a leftist tree~/~/
Insert an element into a leftist tree. This function is defined in
terms of MERGE-LT.

Example usage:

    (INSERT-LT 2 (INSERT-LT 3 (INSERT-LT 4 *EMPTY-LT*)))

This creates a leftist tree with elements 2, 3, 4.~/"
  (merge-lt (list 1 x NIL NIL) tree))

(defun find-min-lt (tree)
  ":doc-section leftist-tree-ops
get the minimum element of a leftist tree~/~/
Get the minimum element of a nonempty tree. Assuming the tree in
question is PROPER-LT, this is just the root of the tree.~/"
  (cond ((is-empty-lt tree) nil)
        (t (root-lt tree))))

(defun delete-min-lt (tree)
  ":doc-section leftist-tree-ops
delete the minimum element of a leftist tree~/~/
Delete the minimum element of a nonempty tree. This is accomplisghed
by simply merging the two subtrees.~/"
  (cond ((is-empty-lt tree) nil)
        (t (merge-lt (left-lt tree) (right-lt tree)))))

(defun build-lt (l)
":doc-section leftist-tree-ops
build a leftist tree from a list~/~/
Builds a leftist tree from a list of elements. This is accomplished by
right-folding the INSERT-LT function over the list, starting with
*EMPTY-LT*.~/"
  (if (atom l)
      *empty-lt*
    (insert-lt (car l) (build-lt (cdr l)))))

;;;;;;;;;;;;;;;;;;;
;; MISCELLANEOUS ;;
;;;;;;;;;;;;;;;;;;;

(defdoc leftist-tree-misc
  ":doc-section leftist-tree-fns
Miscellaneous, but nonetheless useful, functions for leftist trees~/~/
~/")

(defun size-lt (tree)
  ":doc-section leftist-tree-misc
total number of elements in a leftist tree~/~/
Returns the total number of elements in the tree.~/"
  (cond ((is-empty-lt tree) 0)
	(t (+ 1 
	      (size-lt (left-lt tree))
	      (size-lt (right-lt tree))))))

(defun member-lt (x tree)
  ":doc-section leftist-tree-misc
tests membership in a leftist tree~/~/
Tests whether something is an element of the tree. Note that this is
not simply a brute-force search; if the root of the tree is greater
than what we are looking for, we return nil. So in order for this
function to work, the tree has to be PROPER-LT.~/"
  (cond ((is-empty-lt tree) nil)
	((equal x (root-lt tree)) t)
	((lexorder x (root-lt tree)) nil)
	(t (or (member-lt x (left-lt tree))
	       (member-lt x (right-lt tree))))))

(defun length-right-spine-lt (tree)
  ":doc-section leftist-tree-misc
length of the right spine of a leftist tree~/
This is equivalent to RANK-LT.~/
This function actually counts the length of the right spine of the
tree. We will prove that this equals the rank of the tree.~/"
  (if (is-empty-lt tree)
      0
    (+ 1 (length-right-spine-lt (right-lt tree)))))

(defun length-to-nil-lt (tree)
  ":doc-section leftist-tree-misc
length of the shortest path to an empty node~/
This is equivalent to RANK-LT.~/
Returns the length of the shortest path to an empty node. We will
prove that this equals the rank of the tree.~/"
  (cond ((is-empty-lt tree) 0)
        (t (+ 1 (min (length-to-nil-lt (left-lt tree))
                     (length-to-nil-lt (right-lt tree)))))))