CLRS中二叉搜索树（BST）删除算法的正确性求证

BST的核心要求是中序遍历结果为严格递增序列，删除操作的正确性本质就是要维持这个规则不变。下面逐个拆解三种删除场景的正确性，再给出形式化证明的思路：

一、分场景正确性分析 #

1. z无子女（叶子节点） #

直接用NIL替换z即可。原中序遍历里，z夹在它的前驱（比z小的最大节点）和后继（比z大的最小节点）之间，移除z后，前驱直接衔接后继，序列的递增性完全不受影响。同时z的父节点的子树规则也没被破坏——原本z的子树为空，替换后还是空，父节点的左/右子树大小关系依然成立。

2. z仅有一个子女 #

把z的子女直接“提”到z的位置：

• 如果z只有左子女l：l的所有子节点原本就都小于z，z的后继原本就大于z，自然也大于l。替换后，中序序列只是把z的位置换成了l，l的子树序列位置不变，整体依然递增。
• 如果z只有右子女r：同理，r的所有子节点都大于z，z的前驱小于z自然也小于r，替换后序列的递增性依然保持。

3. z有两个子女（最复杂的场景） #

这里的关键是z的后继y的特性：y是z右子树里最小的节点（因为BST的后继是大于z的最小节点），所以y一定没有左子节点——如果y有左子节点，那这个左子节点比y小，才应该是z的后继，矛盾。

分两种子情况看：

子情况A：y是z的直接右子节点

把y放到z的位置，y的左子树替换成z的左子树（z的左子树所有节点都小于z，自然小于y），y的右子树保持原样（原本就都是大于y的节点）。原中序序列里，z的位置在左子树之后、y之前，替换后变成左子树→y→y的右子树，只是去掉了z，序列依然递增。

子情况B：y不是z的直接右子节点

第一步先把y从原位置移除：因为y没有左子节点，直接把y的右子树（如果有的话）交给y的父节点，这其实就是场景2的操作，不会破坏BST规则。
然后把y放到z的位置：y的左子树设为z的左子树（所有节点<z<y，满足y的左子树要求），y的右子树设为z的原右子树（此时z的右子树已经移除了y，剩下的节点都大于等于y）。原中序序列是「左子树→z→[z右子树中y之前的节点]→y→[y的右子树]」，替换后变成「左子树→y→[z右子树中y之前的节点]→[y的右子树]」，只是把z换成了y，而y原本就在z之后，中间的节点都大于z且小于y，所以序列依然严格递增。

二、形式化证明（结构归纳法） #

用结构归纳法可以严谨证明删除操作的正确性：

1. 基例：空树或只有单个节点的树，删除后要么是空树，要么符合BST规则，显然成立。
2. 归纳步骤：假设所有规模小于当前树的BST，删除操作都能维持中序递增的规则。对于当前树T和节点z：
   • 若z是叶子节点（场景1）：删除后的树T'是T去掉z，根据归纳假设，z的父节点的子树依然符合规则，整个树的中序序列是原序列去掉z，保持递增。
   • 若z只有一个子女（场景2）：设子女为c，删除后T'把z替换为c。c的子树原本符合规则，且c与z的父节点的大小关系（c<z则作为左子节点，c>z则作为右子节点）依然满足BST要求。中序序列只是把z换成c，c的子树序列位置不变，保持递增。
   • 若z有两个子女：取后继y，先删除y（场景1或2）得到树T1，根据归纳假设T1符合规则。再把y放到z的位置，y的左子树是z的左子树（所有节点<y），右子树是T1中z的原右子树（所有节点>=y），y的左右子树都符合规则。中序序列中y原本在z之后，替换后z的位置被y占据，中间节点的大小关系不变，序列依然递增。

综上，所有场景下删除操作都能维持BST的核心性质，中序遍历保持严格递增。

内容的提问来源于stack exchange，提问作者Vacation Due 20000