haskell - Red Black Trees: Kahrs version -

i'm trying understand red-black tree implementation given okasaki , delete methods kahrs (the untyped version).

in delete implementation function app used, seems "merging" children of node being deleted. , again, algorithm seems use same "break" red-red property rather black height (please correct me if i'm wrong).. creating red nodes (even if break red-red property). walk down subtree rooted @ node being deleted, correct red-red violations, once reach leafs, start going path (starting @ "new tree" merge created) fixing red-red violation path.

app :: rb -> rb -> rb app e x = x app x e = x app (t r x b) (t r c y d) =     case app b c of         t r b' z c' -> t r(t r x b') z (t r c' y d)         bc -> t r x (t r bc y d) app (t b x b) (t b c y d) =      case app b c of         t r b' z c' -> t r(t b x b') z (t b c' y d)         bc -> balleft x (t b bc y d) app (t r b x c) = t r (app b) x c app (t r x b) c = t r x (app b c) 

1. i'm not able see how "not creating" / "fixing" black height violation? deleting black node create bh-1 , bh subtrees @ node path.
2. results this paper, looks implementation fast , "merge" method might key answering increase in speed.

any pointers explanation "merge" operation great.

please note not homework problem or else. i'm studying independently implementations given in okasaki , fill in "messy" deletes too.

thanks.

given there lot can said on topic, i'll try stick closely possible questions, let me know if missed important.

what hell app doing?

you correct in app breaks red invariant rather black 1 on way down , fixes on way up.

it appends or merges 2 subtrees obey order property, black invariant, red invariant, , have same black-depth new tree obeys order property, black invariant, , red invariant. 1 notable exception root or app rb1 rb2 red , has 2 red subtrees. such trees said "infrared". dealt in delete setting root black in line.

 case del t of {t _ y b -> t b y b; _ -> e} 

claim 1 (order property) if inputs rb1 , rb2 obey order property individually (left subtree < node value < right subtree) , max value in rb1 less min value in rb2, app rb1 rb2 obeys order property.

this 1 easy prove. in fact, can sort of see when looking @ code - as stays left of bs or b's, stay left of cs or c's, stay left of ds. , b's , c's obey property since result of recursive calls app subtrees b , c satisfying claim.

claim 2 (red invariant) if inputs rb1 , rb2 obey red invariant (if node red, both children black), nodes in app rb1 rb2, except possibly root. however, root can "infrared" when 1 of arguments has red root.

proof proof branching on patterns.

• for cases app e x = x , app x e = x claim trivial
• for app (t r x b) (t r c y d), claim hypothesis tells of a, b, c, , d black. follows app b c obeys red invariant (it not infrared).
  • if app b c matches t r b' z c' subtrees b' , c' must black (and obey red invariant), t r (t r x b') z (t r c' y d) obeys red-invariant infrared root.
  • otherwise, app b c produced black node bc, t r x (t r bc y d) obeys red invariant.

• for app (t b x b) (t b c y d) care app b c obey red-invariant

  • if app b c red node, can infrared subtrees b' , c', on other hand, must obey red invariant completely. means t r (t b x b') z (t b c' y d) obeys red invariant.

  • now, if bc turns out black, call balleft x (t b bc y d). neat thing here know 2 cases of balleft can triggered: depending on whether a red or black

    balleft (t r x b) y c = t r (t b x b) y c balleft bl x (t b y b) = balance bl x (t r y b) 

    • in first case, ends happening swap color of left subtree red black (and doing never breaks red-invariant) , put in red subtree. balleft x (t b bc y d) looks t r (t b .. ..) (t b bc y d), , obeys red invariant.

    • otherwise, call balleft turns balance x (t r bc y d) , whole point of balance fixes root level red violations.

• for app (t r b x c) know a , b must black, app b not infrared, t r (app b) x c obeys red invariant. same holds app (t r b x c) letters a, b, , c permuted.

claim 3 (black invariant) if inputs rb1 , rb2 obey black invariant (any path root leaves has same number of black nodes on way) , have same black-depth, app rb1 rb2 obeys black invariant , has same black-depth.

proof proof branching on patterns.

• for cases app e x = x , app x e = x claim trivial
• for app (t r x b) (t r c y d) know since t r x b , t r c y d have same black depth, subtrees a, b, c, , d. claim (remember, induction!) app b c obey black invariant , have same black depth. now, branch our proof on case app b c of ...
  • if app b c matches t r b' z c' red , subtrees b' , c' have same black depth app b c (itself), in turn has same black depth a , d, t r (t r x b') z (t r c' y d) obeys black invariant , has same black depth inputs.
  • otherwise, app b c produced black node bc, again node has same black depth a , d, t r x (t r bc y d) whole still obeys black invariant , has same black depth inputs.
• for app (t b x b) (t b c y d) again know subtrees a, b, c, , d have same black depth app b c. before, branch our proof on case app b c of ...
  • if app b c red node of form t r b' z c', again b', c', a, , d have same black-depth, t r (t b x b') z (t b c' y d) has same black depth
  • now, if bc turns out black, apply same reasoning in our previous claim figure out output balleft x (t b bc y d) has form either
    • t r (t b .. ..) (t b bc y d) (t b .. ..) a recolored black overall tree satisfy black invariant , have black-depth 1 more of a, b, c, or d, same black-depth inputs t b x b , t b c y d).
  • balance x (t r bc y d) , balance maintains black invariant.
• for app (t r b x c) or app (t r x b) c, know a, b, , c have same black-depth , consequently, means app b , app b c have same black-depth, means t r (app b) x c , t r (app b) x c have same black-depth

why fast?

my racket bit rusty don't have great answer this. in general, app makes delete fast allowing in 2 steps: go down target site, continue downwards merge subtrees, come fixing invariants go, way root.

in paper reference, once down target site, call min/delete (i think key difference - rotations otherwise pretty similar) recursively call find element in subtree can plop target site , state of subtree after element has been taken out. believe last part hurts performance of implementation.