我必须使用 Haskell 中的归纳法来证明给定一棵二叉树,叶子的数量等于节点的数量加一。 给定以下称为树的类型:
data Tree = Leaf Int | Node Tree Tree
我定义了两个函数,分别称为leaves和nodes,它们分别返回叶子和节点的数量:
通过归纳,我知道我需要证明基本情况,即节点数为 0 时,并且对于归纳步骤,我需要使用归纳假设。但让我困惑的是,有两个函数,我真的不知道如何继续。在基本情况下,我是否应该表明,如果节点数为 0,则叶子数为 1 或?
最佳答案
“通过归纳”来做到这一点的简单方法是不使用 induction on natural numbers而是使用 structural induction 。证明如下:
基本情况
基本情况适用于 Leaf x
,其中 x
是 Int
。所以你必须证明对于任何x
leaves (Leaf x) = 1 + nodes (Leaf x)
归纳步骤
在归纳步骤中,您假设两个归纳假设:
叶子 t = 1 + 节点 t
留下 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给出了一个与有根据的归纳更紧密联系的建设性版本。
关于haskell - Haskell 中叶子的数量比节点的数量大 1,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/48752973/