二叉树的结构归纳

Question

考虑以下函数定义:

data Tree a = Leaf a | Node a (Tree a) (Tree a)
sumLeaves :: Tree a -> Integer
sumLeaves (Leaf x) = 1 
sumLeaves (Node _ lt rt) = sumLeaves lt + sumLeaves rt 
sumNodes :: Tree a -> Integer
sumNodes (Leaf x) = 0 
sumNodes (Node _ lt rt) = 1 + sumNodes lt + sumNodes rt 

任务:用结构归纳法证明对于所有有限树t:: Tree a成立:

sumLeaves t = sumNodes t + 1

我现在有:

sumLeaves t = sumNodes t + 1
I.A. t = (Tree 0) = (Leaf 0)
sumLeaves (Leaf 0) = 1 sumNodes (Leaf 0) + 1
0 + 1 = 1
1 = 1
I.V.: We assume that the statement holds for an arbitrary t.

i。

现在归纳步骤是什么，我在解决最后一步时真的有问题。

Answer 1

类似于自然数上的归纳法，其中归纳法步骤是假设某些假设对所有小于n的数成立，然后证明对n的假设，结构归纳法步骤假设对给定结构的所有子结构的假设成立。

在你的例子中，正确的假设是该命题适用于任意t@(Node x lt rt)的子树lt和rt，然后证明该命题适用于t。