/usr/share/acl2-6.3/books/leftist-trees/top.lisp is in acl2-books-source 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 | #|
Leftist Trees, Version 0.1
Copyright (C) 2012 by Ben Selfridge <benself@cs.utexas.edu>
FILE: top.lisp
An implementation of Leftist Trees (otherwise known as Leftist Heaps)
as described in Purely Functional Data Structures (Chris Okasaki,
Cambridge University Press 1998).
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 not
requiring the tree to be completely balanced.
Instead, a leftist tree keeps track of its own "rank," which is
defined to be the length of its right-most spine. The "shape"
requirement on leftist trees can be stated as:
(shape) The rank of a tree's left sub-tree is at least as large
as the rank of its right sub-tree.
The full list of requirements for leftist trees then becomes:
(rank) The rank of the empty tree is zero. The rank of a
non-empty tree is one more than the rank of its right
sub-tree.
(heap-ordered) The minimum element in the tree is always the root
node.
(shape) The rank of a tree's left sub-tree is at least as large
as the rank of its right sub-tree.
Of course, these requirements hold recursively for the left- and
right-subtrees of every leftist tree.
The following main functions, constants, and theorems are exported:
; ------------------------------------------------------------
; 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
; how-many-lt natural
; ** HEAPSORT **
; ltree-to-list list
; ltree-sort list
; ------------------------------------------------------------
; Theorems
; ------------------------------------------------------------
; ** BASIC OPERATIONS RESPECT STRUCTURE
(defthm proper-merge-lt
(implies (and (proper-lt tree1)
(proper-lt tree2))
(proper-lt (merge-lt tree1 tree2))))
(defthm proper-insert-lt
(implies (proper-lt tree)
(proper-lt (insert-lt x tree))))
(defthm proper-delete-min-lt
(implies (proper-lt tree)
(proper-lt (delete-min tree))))
(defthm proper-build-lt
(proper-lt (build-lt l)))
; ** RANK THEOREMS
(defthm size-rank-lt
(implies (proper-lt tree)
(<= (- (expt 2 (rank-lt tree)) 1)
(size-lt tree))))
; ** HOW-MANY THEOREMS
(defthm how-many-lt-zero
(implies (not (lexorder (root-lt tree) e))
(equal (how-many-lt e tree) 0)))
(defthm how-many-merge-lt
(implies (and (proper-lt tree1)
(proper-lt tree2))
(equal (how-many-lt e (merge-lt tree1 tree2))
(+ (how-many-lt e tree1)
(how-many-lt e tree2)))))
(defthm how-many-insert-lt
(implies (proper-lt tree)
(equal (how-many-lt e (insert-lt e tree))
(+ 1 (how-many-lt e tree)))))
(defthm how-many-delete-min-lt
(implies (and (proper-lt tree)
(consp tree))
(equal (how-many-lt e (delete-min-lt tree))
(+ (how-many-lt e (left-lt tree))
(how-many-lt e (right-lt tree))))))
(defthm how-many-build-lt
(equal (how-many-lt e (build-lt l))
(how-many e l)))
; ** HEAPSORT THEOREMS
(defthm orderedp-proper-ltree-to-list
(implies (proper-lt tree)
(orderedp (ltree-to-list tree))))
(defthm orderedp-ltree-sort
(orderedp (ltree-sort l)))
(defthm true-listp-ltree-sort
(true-listp (ltree-sort l)))
(defthm how-many-ltree-to-list
(implies (proper-lt tree)
(equal (how-many e (ltree-to-list tree))
(how-many-lt e tree))))
(defthm how-many-ltree-sort
(equal (how-many e (ltree-sort x))
(how-many e x)))
|#
(in-package "ACL2")
(include-book "leftist-tree-defuns")
(include-book "leftist-tree-defthms")
(include-book "leftist-tree-sort")
|