haskell - Haskell 中叶子的数量比节点的数量大 1

Question

我必须使用 Haskell 中的归纳法来证明给定一棵二叉树，叶子的数量等于节点的数量加一。给定以下称为树的类型:

data Tree = Leaf Int | Node Tree Tree 

我定义了两个函数，分别称为leaves和nodes，它们分别返回叶子和节点的数量:

通过归纳，我知道我需要证明基本情况，即节点数为 0 时，并且对于归纳步​​骤，我需要使用归纳假设。但让我困惑的是，有两个函数，我真的不知道如何继续。在基本情况下，我是否应该表明，如果节点数为 0，则叶子数为 1 或？

Answer 1

“通过归纳”来做到这一点的简单方法是不使用 induction on natural numbers而是使用 structural induction 。证明如下:

基本情况

基本情况适用于 Leaf x，其中 x 是 Int。所以你必须证明对于任何x

leaves (Leaf x) = 1 + nodes (Leaf x)

归纳步骤

在归纳步骤中，您假设两个归纳假设:

1. 叶子 t = 1 + 节点 t
2. 留下 u = 1 + 节点 u

证明

leaves (Node t u) = 1 + nodes (Node t u)

我会让你填写实际的证明。

<小时/>

旁注:

结构归纳法是自然数归纳法的推广。特别是，您可以将自然数定义为

data Nat = Z | S Nat

您现在可以使用 p Z 的基本情况进行归纳，以及假设 p n 并证明 p (S n) 的归纳步骤>.

结构归纳法本身可以进一步推广到 well-founded induction ，这是我所知道的最普遍的归纳数学概念。请注意，维基百科页面基于有理有据的经典概念； nLab给出了一个与有根据的归纳更紧密联系的建设性版本。