红黑树：卡尔斯版

Question

我目前正在尝试理解 Okasaki 给出的红黑树实现和 Kahrs (the untyped version) 给出的删除方法。

在删除实现中使用了函数app，它似乎“合并”了被删除节点的子节点。再一次，该算法似乎使用相同的“破坏” Red-Red 属性而不是黑色高度（如果我错了，请纠正我）.. 我们总是在创建红色节点（即使我们破坏了 Red-Red 属性）。沿着以被删除节点为根的子树向下走，纠正红红违规，一旦我们到达叶子，我们开始沿着路径（从创建的“新树”合并开始）修复红红违规沿着路径.

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. 来自this paper 的结果，看起来这个实现非常快，并且“合并”方法可能是解决速度提高的关键。

任何指向此“合并”操作的解释的指针都会很棒。

请注意，这不是作业问题或其他任何问题。我正在独立研究 Okasaki 中给出的实现并填写“混乱”的删除。

谢谢。

Answer 1

鉴于关于这个话题有很多可以说的，我会尽量贴近你的问题，但如果我错过了重要的事情，请告诉我。

app 到底在做什么？

您是正确的，app 在下降的过程中打破了红色的不变量而不是黑色的不变量，并在返回的过程中修复了这个问题。

它app结束或合并两个服从顺序属性的子树，黑色不变量，红色不变量，并且具有相同的黑色深度成一棵也服从顺序属性，黑色不变量的新树，和红色不变量。一个值得注意的例外是根或app rb1 rb2 有时是红色的并且有两个红色子树。这种树被称为“红外线”。这在delete 中处理，只需将此行中的根设置为黑色。

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

Claim 1 (Order property) 如果输入 rb1 和 rb2 分别服从 order 属性（左子树 rb1 中的最大值为小于rb2 中的最小值，则app rb1 rb2 也服从 order 属性。

这个很容易证明。实际上，您甚至可以在查看代码时看到它 - 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 又具有与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 或@987654436 中的任何一个都多一个@，即与输入 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 具有相同的黑色-depth，这意味着T R (app a b) x c 和T R (app a b) x c 也具有相同的黑色深度

为什么这么快？

我的球拍有点生锈，所以我对此没有很好的答案。一般来说，app 允许您分两步完成所有操作，从而快速删除：您进入目标站点，然后继续向下合并子树，然后在进行过程中重新修复不变量，所有通往根的路。

在您引用的paper 中，一旦您到达目标站点，您就会调用min/delete（我认为这是关键区别——否则旋转看起来非常相似），它将递归调用自身来查找元素在子树中，您可以插入目标站点以及取出该元素后子树的状态。我相信最后一部分会损害该实施的性能。