/
WBL.hs
180 lines (154 loc) · 6.66 KB
/
WBL.hs
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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
-----------------------------------------------------------------------
-- Weight-Biased Leftist Heap, verified using LiquidHaskell -----------
-----------------------------------------------------------------------
-- ORIGINAL SOURCE ----------------------------------------------------
-----------------------------------------------------------------------
-- Copyright: 2014, Jan Stolarek, Politechnika Łódzka --
-- --
-- License: See LICENSE file in root of the repo --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps-hs --
-- --
-- Basic implementation of weight-biased leftist heap. No proofs --
-- and no dependent types. Uses a two-pass merging algorithm. --
-----------------------------------------------------------------------
{-@ LIQUID "--no-termination" @-}
module WBL where
type Priority = Int
type Rank = Int
type Nat = Int
data Heap a = Empty | Node { pri :: a
, rnk :: Rank
, left :: Heap a
, right :: Heap a
}
{-@ data Heap a <q :: a -> a -> Bool> =
Empty | Node { pri :: a
, rnk :: Nat
, left :: {v: Heap<q> (a<q pri>) | ValidRank v}
, right :: {v: Heap<q> (a<q pri>) | ValidRank v}
}
@-}
{-@ predicate ValidRank V = okRank V && realRank V = rank V @-}
{-@ type PHeap a = {v:OHeap a | ValidRank v} @-}
{-@ type OHeap a = Heap <{\root v -> root <= v}> a @-}
{-@ measure okRank @-}
okRank :: Heap a -> Bool
okRank Empty = True
okRank (Node p k l r) = ((realRank l >= realRank r) && k == (1 + (realRank l) + (realRank r)))
{-@ measure realRank @-}
realRank :: Heap a -> Int
realRank Empty = 0
realRank (Node p k l r) = 1 + realRank l + realRank r
{-@ invariant {v:Heap a | rank v == realRank (left v) + realRank (right v) && realRank v >= 0 } @-}
{-@ measure rank @-}
{-@ assume rank :: h:Heap a -> {v:Nat | v = realRank h} @-}
rank Empty = 0
rank (Node _ r _ _) = r
-- Creates heap containing a single element with a given Priority
{-@ singleton :: a -> PHeap a @-}
singleton p = Node p 1 Empty Empty
-- Note [Two-pass merging algorithm]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- We use a two-pass implementation of merging algorithm. One pass,
-- implemented by merge, performs merging in a top-down manner. Second
-- one, implemented by makeT, ensures that rank riant of weight
-- biased leftist tree is not violated after merging.
--
-- Notation:
--
-- h1, h2 - heaps being merged
-- p1, p2 - priority of root element in h1 and h2
-- l1 - left subtree in the first heap
-- r1 - right subtree in the first heap
-- l2 - left subtree in the second heap
-- r2 - right subtree in the second heap
--
-- Merge function analyzes four cases. Two of them are base cases:
--
-- a) h1 is empty - return h2
--
-- b) h2 is empty - return h1
--
-- The other two cases form the inductive definition of merge:
--
-- c) priority p1 is higher than p2 - p1 becomes new root, l1
-- becomes its one child and result of merging r1 with h2
-- becomes the other child:
--
-- p1
-- / \
-- / \
-- l1 r1+h2 -- here "+" denotes merging
--
-- d) priority p2 is higher than p2 - p2 becomes new root, l2
-- becomes its one child and result of merging r2 with h1
-- becomes the other child.
--
-- p2
-- / \
-- / \
-- l2 r2+h1
--
-- Note that there is no guarantee that rank of r1+h2 (or r2+h1) will
-- be smaller than rank of l1 (or l2). To ensure that merged heap
-- maintains the rank invariant we pass both childred - ie. either l1
-- and r1+h2 or l2 and r2+h1 - to makeT, which creates a new node by
-- inspecting sizes of children and swapping them if necessary.
-- makeT takes an element (Priority) and two heaps (trees). It
-- constructs a new heap with element at the root and two heaps as
-- children. makeT ensures that WBL heap rank invariant is maintained
-- in the newly created tree by reversing left and right subtrees when
-- necessary (note the inversed r and l in the False alternative of
-- case expression).
{-@ makeT :: p:a -> h1:PHeap {v:a | p <= v} -> h2:PHeap {v:a | p <= v}
-> {v:PHeap a | realRank v = 1 + realRank h1 + realRank h2} @-}
makeT p l r = case rank l >= rank r of
True -> Node p (1 + rank l + rank r) l r
False -> Node p (1 + rank l + rank r) r l
-- merge combines two heaps into one. There are two base cases and two
-- recursive cases - see [Two-pass Merging algorithm]. Recursive cases
-- call makeT to ensure that rank invariant is maintained after
-- merging.
{-@ merge :: (Ord a) => h1:PHeap a -> h2:PHeap a -> {v:PHeap a | realRank v = realRank h1 + realRank h2} @-}
merge Empty h2 = h2
merge h1 Empty = h1
merge h1@(Node p1 k1 l1 r1) h2@(Node p2 k2 l2 r2) = case p1 < p2 of
True -> makeT p1 l1 (merge r1 (Node p2 k2 l2 r2))
False -> makeT p2 l2 (merge (Node p1 k1 l1 r1) r2)
-- Inserting into a heap is performed by merging that heap with newly
-- created singleton heap.
{-@ insert :: (Ord a) => a -> PHeap a -> PHeap a @-}
insert p h = merge (singleton p) h
-- findMin returns element with highest priority, ie. root
-- element. Here we encounter first serious problem: we can't return
-- anything sensible for empty node.
{-@ findMin :: PHeap a -> a @-}
findMin Empty = undefined
findMin (Node p _ _ _) = p
-- and write a safer version of findMinM
{-@ findMinM :: PHeap a -> Maybe a @-}
findMinM Empty = Nothing
findMinM (Node p _ _ _) = Just p
-- deleteMin removes the element with the highest priority by merging
-- subtrees of a root element. Again the case of empty heap is
-- problematic. We could give it semantics by returning Empty, but
-- this just doesn't feel right. Why should we be able to remove
-- elements from an empty heap?
{-@ deleteMin :: (Ord a) => PHeap a -> PHeap a @-}
deleteMin Empty = undefined -- should we insert empty?
deleteMin (Node _ _ l r) = merge l r
-- As a quick sanity check let's construct some examples. Here's a
-- heap constructed by inserting following priorities into an empty
-- heap: 3, 0, 1, 2.
{-@ heap :: PHeap Int @-}
heap = insert (2 :: Int)
(insert 1
(insert 0
(insert 3 Empty)))
-- Example usage of findMin
findMinInHeap :: Priority
findMinInHeap = findMin heap
-- Example usage of deleteMin
deleteMinFromHeap :: Heap Int
deleteMinFromHeap = deleteMin heap