查找树中节点的最大值

Question

我遇到问题。

我必须在Haskell中实现函数maxT，它返回二叉树中节点的最大值。

data Tree a = Leaf a | Node (Tree a) a (Tree a) 

这是给出的。接下来我应该做什么？

maxT :: (Tree Integer) -> Integer 
maxT (Leaf a) = a 
maxT (Node l a r) = max a (max (maxT l) (maxT r)) 

这是正确的吗？

Answer 1

我们来看看证明有多难。为什么？因为这是分析程序错误的好方法。特别是递归的。我们将在技术上使用归纳，但并不复杂。关键是要认识到maxT t必须始终是树t中的最大值 - 此声明“maxT t必须始终是树中最大值t”称为不变量，我们将尝试证明它。我们假设t是Leaf。在这种情况下，您已经定义了maxT (Leaf a) = a，并且由于字面意思是此树中没有其他值，所以a必须是是最大的。因此，当Leaf通过时，maxT支持我们的不变量。这是“基本案例”。现在

---

我们会考虑会发生什么，当我们让t = Node (Leaf a) b (Leaf c)一些Integer小号a，b和c。这是一个高度为1的树，并形成你可能称之为归纳的“示例案例”。让我们试试maxT，看看不变量是否成立。

maxT t 
=== 
maxT (Node (Leaf a) b (Leaf c)) 
=== 
max b (max (maxT (Leaf a)) (maxT (Leaf c))) 

在这一点上，我们将使用我们的基本步骤，并且说，自maxT在此表达的只是应用在Leaf当时的每一个都必须坚持我们不变的。这有点愚蠢，但那是因为这仅仅是一个例子。稍后我们会看到更一般的模式。

现在，让我们评估我们的maxT (Leaf _)比特，知道结果是每个特定左子树或右子树的最大值。

=== 
max b (max a c) 

现在，我不太想潜入max定义，但基于它的名字，我很高兴地假设max a b返回值是a和b之间最大。我们可以通过这里的细节选择我们的方式，但很明显，max b (max a c)已被提供有关我们的Node的所有相关信息，用于计算整个height-1树的最大值。我称这是maxT适用于高度为0和高度为1的树木（Leaf s和Node s仅包含Leaf s）的成功证明。

下一步是概括这个例子案例。

---

所以让我们应用相同的模式概括树的高度。我们会问，如果我们修复了一些数字n，并且假设maxT t支持我们的高度为n或更低的所有t的不变量，会发生什么情况。这有点奇怪 - 我们只显示这适用于n = 0和n = 1。这将清楚为什么这个稍后工作。

那么这个假设对我们有什么作用呢？那么，让我们采取高度为n或更低（称为它们l和r），任意整数x的任意两个Tree s，并将它们组合以形成新树t = Node x l r。当我们做maxT t会发生什么？

maxT t 
=== 
maxT (Node x l r) 
=== 
max x (max (maxT l) (maxT r)) 

，我们知道，根据我们的假设，即maxT l和maxT r坚持我们不变的。然后max es的链继续支持我们现在的树t这是高度-不变。此外（这真的很重要）我们的组装新Tree的过程是通用的 - 我们可以在此方法中使用任何高度-树。这意味着maxT适用于任何高度 - (n+1)树。

---

感应时间！我们现在知道，如果我们选择n并相信（出于某种原因）maxT适用于任何高度的树，那么它立即必须适用于任何高度 - (n+1)树。我们来挑选n = 0。我们通过“基本案例”知道maxT适用于Leaf s，所以突然我们知道maxT适用于height- 1树。这是我们的“示例案例”。现在，鉴于这些知识，我们可以立即看到maxT作品为高度 - 2树木。然后高度 - 3树。然后height- 4。等等等等。

这就完成了一个证明* maxT是正确的。我不得不留下一些警告。我们并没有真正做到这样的细节，以显示max连锁店解决问题，尽管它很有意义。我也没有真正证明诱导步骤的工作原理 - 如果有更多的方法可以创建高度 - (n+1)树，而不是仅使用高度为n或较小树的Node？更强大的方法是“分开”高度，但我认为这有点难以看清。最后，如果我们发送maxT (Leaf undefined)或其他类似的病理值，会发生什么情况。这些出现在Haskell中，因为它是一种（图灵完备的）计算机语言，而不是纯数学。老实说，尽管如此，这些小小的东西并没有改变你的情况。