Treaps in Qi
Delving back into the type system for this post, I thought I would take on the strange and wonderful Binary Search Tree known as the treap. For those that don’t know, a treap is a binary search tree that has a “priority” element attached to the key. It uses the random priority to ensure balancing of the tree. It does this by ensuring the tree is in binary search tree form with respect to the keys, and in heap form with respect to the priorities. We will create a simple type of string based treap in Qi and perhaps extend it to a more general version if I find the time to finish it. *grin*The datatype for treap can be either list based or tuple based. I’ll begin with the tuple version as it shows off a bit more of the power of Qi pattern matching, but a list version would be more readable. We can signify empty leaves with the null list in either case.
_______
[] : treap;
And now we will create the recursive type. It takes a key and a priority and has a left branch and a right branch. Using the tuple to define the leaves means we place the key and priority in their own tuple and use that as the first element. Then we can put the left and right branches in their own tuple as the second element of our treap node. We’ll use the ever handy left/right sequent operator to ensure we can prove things about treaps using the datastructure only and typing the internal parts.
Key : string; Priority : number; LeftTreap : treap; RightTreap : treap;
===============================
(@p (@p Key Priority) (@p LeftTreap RightTreap)) : treap;
Now when we wish to insert a key into the treap, we must first make a random number to assign it for heap priority.
(define treap_insert
{string --> treap --> treap}
K Tree -> (treap_insert* K (- (random 40000000) 20000000) Tree))
Now the fun begins. The base case seems simple enough, just make a treap that looks like the above definition but has LeftTreap and RightTreap set to [].
(define treap_insert*
{string --> number --> treap --> treap}
K P [] -> (@p (@p K P) (@p [] []))
Now it could be that we are trying to insert an element that we already have. If so, we simply return the treap we had to begin with.
K P (@p (@p K* P*)
(@p L R))
-> (@p (@p K* P*) (@p L R)) where (= K K*)
Note that our pattern matched definition is well typed. L is a treap and R is a treap. K is a string and P is a number. We match the new key and priority as K and P. We match the treap node’s priority as K* and P* and the branches as L and R. If you mess up using them in your definition, the complier complains loudly.
Now we know the K is not equal to the current treap node, if it is less than the tree node we insert it somewhere on the left tree. AFTER we do this, then we order the treap by heap priority, preserving the BST ordering as we move our way up the tree. We’ll use the same pattern as the element above.
K P (@p (@p K* P*)
(@p L R))
-> (let Tree (@p (@p K* P*)
(@p (treap_insert* K P L)
R))
(if (> P* P)
(rotate_right Tree)
Tree))
where(str-lt K K*)
So if our new priority is less than the old one, we move it up the treap. That makes it reverse heap ordering, but we are not splitting hairs here. *grin*
So now we need to find out how to rotate a treap node up a treap. Rotate right takes the L branch and finds its left and right treaps and their keys. It then puts the left L treap as the current left, uses the left treap node’s key/priority as the current key/priority and makes a new right treap with the original left nodes right hand treap paired with the old right hand side, placing the old key/priority there. The code below serves as our heapify.
(define rotate_right
{treap --> treap}
(@p (@p Key Priority)
(@p (@p (@p K* P*)
(@p A1 A2))
B))
-> (@p (@p K* P*)
(@p A1
(@p (@p Key Priority)
(@p A2 B)) ))
)
Pattern matching makes the change short and sweet. Type checking ensures that we have a valid treap at the end.
Now we can finish our definition of treap_insert with the right hand insert
K P (@p (@p K* P*)
(@p L R))
-> (let Tree (@p (@p K* P*)
(@p L
(treap_insert* K P R)))
(if (> P* P)
(rotate_left Tree)
Tree))
We can make a rotate_left along the lines of the rotate_right
(define rotate_left
{treap --> treap}
(@p (@p Key Priority)
(@p A
(@p (@p K* P*)
(@p B1 B2)))) -> (@p (@p K* P*)
(@p
(@p (@p Key Priority)
(@p A B1))
B2))
)
All we need to do now is define a string less than function str-lt that compares strings. And here we run into a problem. We have no type safe way of comparing strings in Qi. So we’ll have to modify Qi to know about our version of the string compare function. We’ll build it from the ground up by giving CHAR-CODE a type. In deference to Haskell, let us name the function “ord”.
You can patch it with
42c42
<> occurrences occurs-check or output prf print profile profile-results prooft
ool provable?
47c47
<> track tuple? undebug unprf union unprofile untrack value version
1527c1527
<> number? 1 occurs-check 1 occurrences 2 or 2 prf 1 print 1 profile 1 profil
e-results 1 prooftool 1
1586,1587c1586
< (boolean --> (boolean --> boolean)) ord (character --> number)
<> B) --> (A --> B))
---
> (boolean --> (boolean --> boolean)) prf ((A --> B) --> (A --> B))
2397,2398d2395
< (DEFUN ord (x) (CHAR-CODE x)) <> string --> boolean}
But it would help to simply search for the word “difference” as it is an internal function used only 3 times in the program outside its own definition and add the code yourself to learn how. There you find the arity list that you must add the ord function too and the type list where you specify the type. Then you can add the DEFUN for ord by the other system function defuns. Run the installer and you will get a version of Qi that has our “ord” function.
--- EDIT ---
I'm adding a much better way of doing this in Qi that Mark pointed out on the mailing list.
Lisp contains a function STRING<, so if you want to bring this into Qi,
then the following will do it.
(0-) (define string<
X Y -> (if (empty? (STRING< X Y)) false true))
======> Warning:
the following variables are free in string<: STRING<;
string<
(1-) (newfuntype string< (string --> string --> boolean))
string<
(2-) (tc +)
true
(3+) string<
string< : (string --> (string --> boolean))
(4+) (string< "ghgjj" "ghhhg")
true : boolean
--- EDIT END ---
Now we can define our string less than function, “str-lt”.
(define str-lt
{string --> string --> boolean}
S1 S2 -> (str-lt* (explode S1) (explode S2)))
(define str-lt*
{(list character) --> (list character) --> boolean}
[] _ -> false
_ [] -> true
[X |_] [Y | _] -> true where (< (ord X) (ord Y))
[_ |L1] [_ | L2] -> (str-lt* L1 L2)
)
And now we have a working, input-only treap. I think at this point I will take a break and perhaps return the program efficiency and changing of the syntax in another article. Let me know of any questions or comments you have so far please!
Here is the full file. I'll create a place to download my code sometime soon.
(datatype treap
_______
[] : treap;
Key : string; Priority : number; LeftTreap : treap; RightTreap : treap;
===============================
(@p (@p Key Priority) (@p LeftTreap RightTreap)) : treap;
)
(define treap_empty?
{ treap --> boolean }
Tree -> true where (= Tree [])
Tree -> false
)
(define rotate_left
{treap --> treap}
(@p (@p Key Priority)
(@p A
(@p (@p K* P*)
(@p B1 B2)))) -> (@p (@p K* P*)
(@p
(@p (@p Key Priority)
(@p A B1))
B2))
)
(define rotate_right
{treap --> treap}
(@p (@p Key Priority)
(@p (@p (@p K* P*)
(@p A1 A2))
B))
-> (@p (@p K* P*)
(@p A1
(@p (@p Key Priority)
(@p A2 B))
))
)
(define treap_insert
{string --> treap --> treap}
K T -> (treap_insert* K (- (random 40000000) 20000000) T))
(define treap_insert*
{string --> number --> treap --> treap}
K P [] -> (@p (@p K P) (@p [] []))
K P (@p (@p K* P*)
(@p L R))
-> (@p (@p K* P*) (@p L R)) where (= K K*)
K P (@p (@p K* P*)
(@p L R))
-> (let Tree (@p (@p K* P*)
(@p (treap_insert* K P L)
R))
(if (> P* P)
(rotate_right Tree)
Tree))
where(str-lt K K*)
K P (@p (@p K* P*)
(@p L R))
-> (let Tree (@p (@p K* P*)
(@p L
(treap_insert* K P R)))
(if (> P* P)
(rotate_left Tree)
Tree))
)
(define str-lt
{string --> string --> boolean}
S1 S2 -> (str-lt* (explode S1) (explode S2)))
(define str-lt*
{(list character) --> (list character) --> boolean}
[] _ -> false
_ [] -> true
[X |_] [Y | _] -> true where (< (ord X) (ord Y))
[_ |L1] [_ | L2] -> (str-lt* L1 L2)
)
0 Comments:
