基于归纳法证明Haskell二叉树叶节点数=节点数+1的困惑

嘿，别纠结啦！这个归纳证明其实完全可以跟着二叉树的递归结构和你那两个函数的定义一步步走，咱们把它拆解得明明白白的～

首先，先对齐一下前提：我先假设你的Tree类型和leaves、nodes函数是符合常规递归定义的（如果你的实现略有不同，思路也是通用的）：

-- 二叉树类型：Leaf是叶节点，Node是带左右子树的内部节点
data Tree a = Leaf a | Node (Tree a) (Tree a)

-- 计算叶节点数量
leaves :: Tree a -> Int
leaves (Leaf _) = 1
leaves (Node l r) = leaves l + leaves r

-- 计算内部节点数量（划重点：这里的nodes是指非叶节点的数量，不然等式不成立）
nodes :: Tree a -> Int
nodes (Leaf _) = 0
nodes (Node l r) = 1 + nodes l + nodes r

我们要证明的命题是：对于任意二叉树t，leaves t = nodes t + 1恒成立

结构归纳法刚好适配二叉树的递归结构，咱们分两步来：

1. 基础情况：树是单个叶节点（t = Leaf x） #

直接代入函数计算两边：

• 左边：leaves (Leaf x) = 1
• 右边：nodes (Leaf x) + 1 = 0 + 1 = 1
  两边完全相等，基础情况成立。

2. 归纳步骤：假设子树满足命题，推导当前树 #

首先给出归纳假设：
对于任意两棵二叉树l和r，都有：

• leaves l = nodes l + 1
• leaves r = nodes r + 1

现在我们要证明，当树是t = Node l r时，leaves t = nodes t + 1也成立。

先算左边（叶节点数）：
根据leaves的递归定义，leaves (Node l r) = leaves l + leaves r
把归纳假设代入进去：
leaves l + leaves r = (nodes l + 1) + (nodes r + 1) = nodes l + nodes r + 2

再算右边（内部节点数+1）：
根据nodes的递归定义，nodes (Node l r) = 1 + nodes l + nodes r
所以右边是(1 + nodes l + nodes r) + 1 = nodes l + nodes r + 2

左边和右边的结果完全一致，说明归纳步骤成立。

为啥涉及两个函数也不用慌？ #

其实核心逻辑很简单：你的leaves和nodes都是递归定义的，刚好和归纳法的“拆解子问题”思路完全匹配。归纳假设同时覆盖了子树的叶节点数和内部节点数的关系，而我们只需要把函数的递归规则套进去，就能把当前树的结果和子树的已知结论关联起来，完全不需要额外的复杂操作～

内容的提问来源于stack exchange，提问作者Pape Sow Traore