binary-tree - 二叉树归纳示例

Question

我已经将这个归纳问题作为练习来解决，而且我已经有几个月没有进行过归纳了，所以我不知道如何解决这个问题。这是示例：

“通过归纳证明：在非空二叉树中，节点数等于节点之间的链接数加一”。

我对如何启动它有一个基本的想法，比如基本情况是 1 个节点和 0 个链接。但是，我不确定如何在我的解决方案中表示“链接”。任何帮助是极大的赞赏。

标签： binary-treeinduction

Answer 1

我将从归纳定义一个非空二叉树开始。

Inductive nonemptyTree :=
    | Endpoint 
    | Single (l : nonemptyTree)
    | Double (l : nonemptyTree) (r : nonemptyTree).

这看起来比普通的二叉树要复杂一些，但清楚地区分不同的结构并移除典型的“Nil”构造函数有助于证明。

从那里，您将要定义什么是“链接”和“节点”以及如何在给定树的情况下计算它们。nonemptyTree给定定义，这很容易。

Fixpoint links (t : nonemptyTree) : nat :=
    match t with
    | Endpoint => 0
    | Single l => 1 + links l
    | Double l r => 2 + links l + links r
    end.

Fixpoint nodes (t : nonemptyTree ) : nat :=
    match t with
    | Endpoint => 1
    | Single l => 1 + nodes l
    | Double l r => 1 + nodes l + nodes r
    end.

那时，我们只需要证明对于所有的树t，nodes t = links t + 1。只有三种情况需要考虑，并且您已经获得了第一种情况（基本情况）。