红黑树:Kahrs版

Question

我目前正在尝试理解Okasaki给出的Red-Black树实现并删除Kahrs的方法(无类型版本).

在删除实现中使用了一个函数app,它似乎"合并"了被删除节点的子节点.再次,算法似乎使用相同的"打破"红色 - 红色属性而不是黑色高度(请纠正我,如果我错了)..我们总是创建红色节点(即使我们打破红色 - 红色属性).沿着被删除节点的子树走下去,纠正红红色违规,一旦我们到达叶子,我们就开始上行路径(从创建的"新树"合并开始)修复路径上的红色红色违规.

app :: RB a -> RB a -> RB a
app E x = x
app x E = x
app (T R a x b) (T R c y d) =
    case app b c of
        T R b' z c' -> T R(T R a x b') z (T R c' y d)
        bc -> T R a x (T R bc y d)
app (T B a x b) (T B c y d) = 
    case app b c of
        T R b' z c' -> T R(T B a x b') z (T B c' y d)
        bc -> balleft a x (T B bc y d)
app a (T R b x c) = T R (app a b) x c
app (T R a x b) c = T R a x (app b c)

1. 我无法看到我们如何"不创造"/"修复"黑色高度违规？删除黑色节点会在路径上的某个节点创建bh-1和bh子树.
2. 本文的结果看起来这个实现非常快,"合并"方法可能是解决速度提升的关键.

任何指向这种"合并"操作的解释都会很棒.

请注意这不是作业问题或其他任何问题.我正在独立研究冈崎的实施,并填写"杂乱"删除.

谢谢.

Answer 1

鉴于在这个主题上可以说很多,我会尽可能地贴近你的问题,但如果我错过了重要的事情,请告诉我.

到底是app怎么回事？

你是正确的,app在下来的路上打破红色不变而不是黑色,并在返回的路上修复它.

它应用程序结束或合并两个遵循order属性,黑色不变量,红色不变量的子树,并且在一个新的树中具有相同的黑色深度,该树也遵循顺序属性,黑色不变量和红色不变量.一个值得注意的例外是根或app rb1 rb2有时是红色并且有两个红色子树.这种树被称为"红外线".这一点将在delete由刚刚设置的根是黑色的在这条线.

 case del t of {T _ a y b -> T B a y b; _ -> E}

权利要求1(订单属性)如果输入rb1并rb2单独服从订单属性(左子树<节点值<右子树)并且最大值in rb1小于最小值in rb2,则app rb1 rb2也遵守订单属性.

这个很容易证明.事实上,你甚至可以在看代码时看到它 - as总是停留在bs或b's的左边,它总是停留在cs或c's的左边,它始终位于ds 的左边. .并且b's和c's也遵守这个属性,因为它们是递归调用app子树b并c满足声明的结果.

权利要求2(红色不变量)如果输入rb1并rb2服从红色不变量(如果一个节点是红色,那么它的两个孩子都是黑色),那么所有节点也是如此app rb1 rb2,除了可能的根.但是,只有当其中一个参数具有红色根时,根才能为"红外".

证明证明是通过分支模式.

• 对于案件app E x = x和app x E = x索赔是微不足道的
• 因为app (T R a x b) (T R c y d),声称假设告诉我们所有的a,b和c,并且d是黑色的.因此,app b c完全服从红色不变量(它不是红外线).
  • 如果app b c匹配T R b' z c'则其子树b'和c'必须是黑色的(并服从红色不变),所以T R (T R a x b') z (T R c' y d)服从红色不变用红外根.
  • 否则,app b c产生一个黑色节点bc,所以T R a x (T R bc y d)服从红色不变量.

• 因为app (T B a x b) (T B c y d)我们只关心自己app b c会遵守红色不变量

  • 如果app b c是一个红色的节点,也可以是红外线,但其子树b'和c',在另一方面,必须完全服从红色不变.这意味着T R (T B a x b') z (T B c' y d)也服从红色不变量.

  • 现在,如果bc结果是黑色,我们打电话balleft a x (T B bc y d).这里的巧妙之处在于我们已经知道balleft可以触发哪两种情况:取决于a是红色还是黑色

    balleft (T R a x b) y c = T R (T B a x b) y c
    balleft bl x (T B a y b) = balance bl x (T R a y b)
    

    • 在第一种情况下,最终发生的事情是我们将左子树的颜色从红色交换为黑色(这样做从不打破红色不变量)并将所有内容都放在红色子树中.然后balleft a x (T B bc y d)看起来像T R (T B .. ..) (T B bc y d),并遵守红色不变量.

    • 否则,balleft转入的调用balance a x (T R bc y d)和整个问题balance是它修复了根级红色违规.

• 因为app a (T R b x c)我们知道a并且b必须是黑色的,所以app a b不是红外线,所以T R (app a b) x c服从红色不变量.这同样适用于app a (T R b x c),但用字母a,b和c置换.

权利要求3(黑色不变量)如果输入rb1并rb2服从黑色不变量(从根到叶子的任何路径在路上具有相同数量的黑色节点)并且具有相同的黑色深度,app rb1 rb2也服从黑色不变量并具有相同的黑色深度.

证明证明是通过分支模式.

• 对于案件app E x = x和app x E = x索赔是微不足道的
• 因为app (T R a x b) (T R c y d)我们知道,因为T R a x b并且T R c y d具有相同的黑色深度,所以他们的子树a,b和c,和d.声称(记住,这是感应!)app b c也将服从黑色不变量并具有相同的黑色深度.现在,我们将证明分支case app b c of ...
  • 如果app b c匹配的T R b' z c'是红色和它的子树b',并c'有相同的黑色深度app b c(本身),这反过来又具有同样的黑色深度a和d,所以T R (T R a x b') z (T R c' y d)服从黑不变,并具有相同的黑色深度作为它的输入.
  • 否则,app b c所产生的黑点bc,但同样该节点具有相同的黑色深度a和d,所以T R a x (T R bc y d)作为一个整体仍然服从黑不变,并具有相同的黑色深度作为它的输入.
• 对于app (T B a x b) (T B c y d)我们再次立即知道,子树a,b,c,并且d都具有相同的黑色深度app b c.和以前一样,我们分支证明了case app b c of ...
  • 如果app b c是形式的红点T R b' z c',我们再次拿到b',c',a,并且d具有相同的黑色深度,所以T R (T B a x b') z (T B c' y d)也有这同样的黑色深度
  • 现在,如果bc结果是黑色,我们应用与我们之前的声明中相同的推理,以确定输出balleft a x (T B bc y d)实际上具有以下形式:
    • T R (T B .. ..) (T B bc y d)这里(T B .. ..)只是a重新着色为黑色,所以整体的树将满足黑不变,并有黑色的深度比任何一个以上a,b,c,或者d,这是说同样的黑色,深作为输入T B a x b和T B c y d).
  • balance a x (T R bc y d)并balance保持黑色不变.
• 对于app a (T R b x c)或app (T R a x b) c,我们知道a,b和c所有具有相同的黑色深度,因此,这意味着app a b和app b c这个同样的黑色深度,这意味着T R (app a b) x c和T R (app a b) x c也有这种同样的黑色深度

为什么快？

我的球拍有点生疏,所以我对此没有很好的答案.一般来说,app通过允许您分两步完成所有操作来快速删除:您转到目标站点,然后继续向下合并子树,然后您回来修复不变量,一直到根.

在你引用的论文中,一旦你到达目标站点,你就会调用min/delete(我认为这是关键的区别 - 旋转看起来非常相似),它会递归地调用自己来找到你可以插入的子树中的元素取出该元素后的目标站点和子树的状态.我相信最后一部分会伤害该实现的性能.