鉴于此主题可以说很多，我会尽可能地按照您的问题进行回答，但如果我漏掉了重要的内容，请告诉我。
这个`app`到底是干什么的？
您是正确的，
app会打破红色不变性而不是黑色不变性，并在返回时修复它。
它将符合顺序属性、黑色不变性、红色不变性且具有相同黑深度的两个子树附加或合并成一个新树，该新树也满足顺序属性、黑色不变性和红色不变性。唯一的例外是根节点或
app rb1 rb2有时是红色的且有两个红色子树。这些树被称为“红外线”。在
delete中，通过设置这行代码中的根节点为黑色来处理这种情况。
case del t of {T _ a y b -> T B a y b; _ -> E}
声明1（顺序属性）如果输入的rb1和rb2分别满足顺序属性（左子树 < 节点值 < 右子树），并且rb1中的最大值小于rb2中的最小值，则app rb1 rb2也满足顺序属性。
这个很容易证明。实际上，当查看代码时，您甚至可以看到它——a始终保持在b或b'的左侧，后者始终保持在c或c'的左侧，后者始终保持在d的左侧。而b'和c'也满足此属性，因为它们是使用满足该声明的子树b和c进行递归调用的结果。
声明2（红色不变性）如果输入的rb1和rb2符合红色不变性（如果一个节点是红色，则其两个子节点都是黑色），则app rb1 rb2中的所有节点也如此，除了可能的根节点。然而，只有当其参数之一具有红色根时，根才可能是“不红色的”。
证明 该证明通过对模式进行分支来完成。
- For cases
app E x = x and app x E = x the claim is trivial
- For
app (T R a x b) (T R c y d), the claim hypothesis tells us all of a, b, c, and d are black. It follows that app b c obeys the red invariant fully (it is not infrared).
- If
app b c matches T R b' z c' then its subtrees b' and c' must be black (and obey the red invariant), so T R (T R a x b') z (T R c' y d) obeys the red-invariant with an infrared root.
- Otherwise,
app b c produced a black node bc, so T R a x (T R bc y d) obeys the red invariant.
For app (T B a x b) (T B c y d) we only care that app b c will itself obey the red-invariant
- If
app b c is a red node, it can be infrared but its subtrees b' and c', on the other hand, must obey the red invariant completely. That means T R (T B a x b') z (T B c' y d) also obeys the red invariant.
Now, if bc turns out to be black, we call balleft a x (T B bc y d). The neat thing here is that we already know which two cases of balleft can be triggered: depending on whether a is red or black
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)
In the first case, what ends up happening is that we swap the color of the left subtree from red to black (and doing so never breaks the red-invariant) and put everything in a red subtree. Then balleft a x (T B bc y d) actually looks like T R (T B .. ..) (T B bc y d), and that obeys the red invariant.
Otherwise, the call to balleft turns into balance a x (T R bc y d) and the whole point of balance is that it fixes root level red violations.
For app a (T R b x c) we know that a and b must be black, so app a b is not infrared, so T R (app a b) x c obeys the red invariant. The same holds for app a (T R b x c) but with letters a, b, and c permuted.
第三条声明（黑不变量），如果输入的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
为什么它很快？
我的Racket有点生疏，所以我没有一个很好的答案。一般来说，app 通过允许您在两个步骤中完成所有操作，使删除变得更快：您首先进入目标站点，然后继续向下合并子树，然后回到顶部修复不变量。
在您提到的论文中，一旦您到达目标站点，就会调用 min/delete （我认为这是关键区别-旋转看起来非常相似），它将递归调用自身以查找可以放置在目标位置的子树中的元素，以及该元素被取出后子树的状态。我相信最后一部分是导致该实现性能不佳的原因。
