liquidhaskell-0.8.2.0: docs/blog/todo/red-black-order.lhs
---
layout: post
title: "Red-Black Trees: Order"
date: 2014-04-05 16:12
author: Ranjit Jhala
published: false
comments: true
external-url:
categories: measures, abstract-refinements
demo: RBTree-ord.hs
---
A data structure that implements a *set* interface, must
provide an efficient way to determine *membership*, i.e.
a function
\begin{code}
member :: a -> RBTree a -> Bool
\end{code}
where `elem x xs` returns `True` iff `x` is in the set denoted by `xs`.
Red Black trees are use
To enable effici
Abstract Refinements vs. Indices
--------------------------------
Most formal accounts of Red Black trees eschew the order
invariant as it is rather cumbersome to encode using GADTs
and indexed-types -- one must index the structure with lower
and upper bounds, and appropriately adjust these bounds at
rotations.
TODO: **Conjoining Specifications** lamport.
TODO: composing, and, for example,
TODO: red-black trees.
[Red Black trees][RBTwiki] trees are a classic, cold-war era,
data structure used to efficiently represent sets, using trees
whose nodes are labeled by the set's elements, and additionally,
are colored *red* or *black*.
The key to efficiency is that the the trees be *balanced*.
Of course, the easiest way to do this is to just add a *height*
label and check that the difference of heights at each node is
bounded (cf. [AVL trees][AVLTwiki]). But, back in the olden
days, every bit counted -- the super cunning thing about
Red-Black Trees is that they ensure balancedness, at the
throwaway price of a *single bit* per node.
The catch is that the invariants are devilishly tricky.
<!-- more -->
1. **Order:** Each node's value is between those in its left and right subtrees,
2. **Color:** Each red node's children are colored black,
3. **Height:** Each root-to-leaf path has the same number of black nodes.
There are ways to encode various subsets of these using
GADTs and such, but, like [Appel][RBTappel], I find the
encodings rather too clever as they require a variety
of different types and constructors to capture each
invariant.
One advantage of refinements is we fix the data type,
and can then *pick and choose* which invariants we want
to verify, and *compose* them, quite trivially, via
conjunction.
Continue to:
* [Order][rbtOrder]
* [Color][rbtColor]
* [Height][rbtHeight]
* [Composition][rbtAll]
[rbtOrder] : /blog/2014/04/07/red-black-order.lhs/
[rbtColor] : /blog/2014/04/14/red-black-color.lhs/
[rbtHeight] : /blog/2014/04/21/red-black-height.lhs/
[rbtCompose] : /blog/2014/04/28/red-black-compose.lhs/
Red-Black Trees
---------------
Abstract Refinements
--------------------
Ordered Trees
-------------
Over the next several posts, lets see how to develop an
RBTree library, using LiquidHaskell to directly and
compositionally specify and enforce the above invariants.
<div class="hidden">
\begin{code}
{-@ LIQUID "--no-termination" @-}
module Foo (add, remove, deleteMin, deleteMin') where
import Language.Haskell.Liquid.Prelude
\end{code}
</div>
ADD
\begin{code}
data Color = B -- ^ Black
| R -- ^ Red
deriving (Eq,Show)
\end{code}
\begin{code}
data RBTree a = Leaf
| Node Color a !(RBTree a) !(RBTree a)
deriving (Show)
\end{code}
---------------------------------------------------------------------------
-- | Add an element -------------------------------------------------------
---------------------------------------------------------------------------
{-@ add :: (Ord a) => a -> ORBT a -> ORBT a @-}
add x s = makeBlack (ins x s)
{-@ ins :: (Ord a) => a -> ORBT a -> ORBT a @-}
ins kx Leaf = Node R kx Leaf Leaf
ins kx s@(Node B x l r) = case compare kx x of
LT -> let t = lbal x (ins kx l) r in t
GT -> let t = rbal x l (ins kx r) in t
EQ -> s
ins kx s@(Node R x l r) = case compare kx x of
LT -> Node R x (ins kx l) r
GT -> Node R x l (ins kx r)
EQ -> s
---------------------------------------------------------------------------
-- | Delete an element ----------------------------------------------------
---------------------------------------------------------------------------
{-@ remove :: (Ord a) => a -> ORBT a -> ORBT a @-}
remove x t = makeBlack (del x t)
{-@ del :: (Ord a) => a -> ORBT a -> ORBT a @-}
del x Leaf = Leaf
del x (Node _ y a b) = case compare x y of
EQ -> append y a b
LT -> case a of
Leaf -> Node R y Leaf b
Node B _ _ _ -> lbalS y (del x a) b
_ -> let t = Node R y (del x a) b in t
GT -> case b of
Leaf -> Node R y a Leaf
Node B _ _ _ -> rbalS y a (del x b)
_ -> Node R y a (del x b)
{-@ append :: y:a -> ORBT {v:a | v < y} -> ORBT {v:a | y < v} -> ORBT a @-}
append :: a -> RBTree a -> RBTree a -> RBTree a
append _ Leaf r
= r
append _ l Leaf
= l
append piv (Node R lx ll lr) (Node R rx rl rr)
= case append piv lr rl of
Node R x lr' rl' -> Node R x (Node R lx ll lr') (Node R rx rl' rr)
lrl -> Node R lx ll (Node R rx lrl rr)
append piv (Node B lx ll lr) (Node B rx rl rr)
= case append piv lr rl of
Node R x lr' rl' -> Node R x (Node B lx ll lr') (Node B rx rl' rr)
lrl -> lbalS lx ll (Node B rx lrl rr)
append piv l@(Node B _ _ _) (Node R rx rl rr)
= Node R rx (append piv l rl) rr
append piv l@(Node R lx ll lr) r@(Node B _ _ _)
= Node R lx ll (append piv lr r)
---------------------------------------------------------------------------
-- | Delete Minimum Element -----------------------------------------------
---------------------------------------------------------------------------
{-@ deleteMin :: ORBT a -> ORBT a @-}
deleteMin (Leaf) = Leaf
deleteMin (Node _ x l r) = makeBlack t
where
(_, t) = deleteMin' x l r
{-@ deleteMin' :: k:a -> ORBT {v:a | v < k} -> ORBT {v:a | k < v} -> (a, ORBT a) @-}
deleteMin' k Leaf r = (k, r)
deleteMin' x (Node R lx ll lr) r = (k, Node R x l' r) where (k, l') = deleteMin' lx ll lr
deleteMin' x (Node B lx ll lr) r = (k, lbalS x l' r ) where (k, l') = deleteMin' lx ll lr
---------------------------------------------------------------------------
-- | Rotations ------------------------------------------------------------
---------------------------------------------------------------------------
lbalS k (Node R x a b) r = Node R k (Node B x a b) r
lbalS k l (Node B y a b) = let t = rbal k l (Node R y a b) in t
lbalS k l (Node R z (Node B y a b) c) = Node R y (Node B k l a) (rbal z b (makeRed c))
lbalS k l r = error "nein"
rbalS k l (Node R y b c) = Node R k l (Node B y b c)
rbalS k (Node B x a b) r = let t = lbal k (Node R x a b) r in t
rbalS k (Node R x a (Node B y b c)) r = Node R y (lbal x (makeRed a) b) (Node B k c r)
rbalS k l r = error "nein"
lbal k (Node R y (Node R x a b) c) r = Node R y (Node B x a b) (Node B k c r)
lbal k (Node R x a (Node R y b c)) r = Node R y (Node B x a b) (Node B k c r)
lbal k l r = Node B k l r
rbal x a (Node R y b (Node R z c d)) = Node R y (Node B x a b) (Node B z c d)
rbal x a (Node R z (Node R y b c) d) = Node R y (Node B x a b) (Node B z c d)
rbal x l r = Node B x l r
---------------------------------------------------------------------------
---------------------------------------------------------------------------
---------------------------------------------------------------------------
makeRed (Node _ x l r) = Node R x l r
makeRed Leaf = error "nein"
makeBlack Leaf = Leaf
makeBlack (Node _ x l r) = Node B x l r
---------------------------------------------------------------------------
-- | Specifications -------------------------------------------------------
---------------------------------------------------------------------------
-- | Ordered Red-Black Trees
{-@ type ORBT a = RBTree <{\root v -> v < root }, {\root v -> v > root}> a @-}
-- | Binary Search Ordering
{-@ data RBTree a <l :: a -> a -> Prop, r :: a -> a -> Prop>
= Leaf
| Node (c :: Color)
(key :: a)
(left :: RBTree <l, r> (a <l key>))
(left :: RBTree <l, r> (a <r key>))
@-}