3

我有个问题。

我必须在 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))

这是正确的吗？

4

1 回答 1

4

让我们看看证明它是正确的有多难。为什么？因为这是分析程序错误的好方法。尤其是递归的。我们将在技术上使用归纳法，但它并不那么复杂。关键是要意识到maxT t必须始终是树中的最大值——这个t声明，“maxT t必须始终是树中的最大值t”被称为不变量，我们将尝试证明它。

首先，我们假设t是一个Leaf. 在这种情况下，您已经定义并且由于在这棵树maxT (Leaf a) = a中实际上没有其他值，因此a 必须是最大的。因此，maxT当通过 a 时维护我们的不变量Leaf。这是“基本情况”。

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

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

在这一点上，我们将使用我们的基本情况步骤并说由于maxT这个表达式中的唯一应用程序是在Leafs 上，所以每个人都必须维护我们的不变量。这有点愚蠢，但那是因为它只是一个示例案例。稍后我们将看到更一般的模式。

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

===
max b (max a c)

现在，我不想深入研究 的定义max，但根据它的名称，我很高兴假设返回的值在和max a b之间是最大的。我们可以通过这里的细节来选择我们的方式，但很明显，已经给出了关于我们的所有相关信息，用于计算整个 height-1 树的最大值。我认为这是一个成功的证明，适用于 height-0 和 height-1 树（s 和s 仅包含s）。abmax b (max a c)NodemaxTLeafNodeLeaf

下一步是概括这个例子。

因此，让我们应用相同的模式概括树的高度。我们会问，如果我们固定某个数字 会发生什么n，并假设它在所有高度或更少的情况maxT t下都支持我们的不变量。这有点奇怪——我们只展示了这适用于和。稍后会清楚为什么这会起作用。tnn = 0n = 1

那么这个假设对我们有什么作用呢？好吧，让我们取任意两个Tree高度n或更少的 s（称它们为l和r）、任意整数x，并将它们组合成一棵新树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坚持我们的不变量。然后 es 链max现在继续支持我们的不变量，对于一个t高度为 - 的树(n+1)。此外（这非常重要）我们组装新Trees 的过程是通用的——我们可以用这种方法制作任何高度(n+1)树。这意味着它maxT适用于任何高度(n+1)树。

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

maxT这完成了一个正确的证明* 。

*我必须留下一些警告。我们并没有真正做繁琐的细节来证明max链条可以正常工作，尽管这是有道理的。我也没有真正证明归纳步骤有效——如果有更多的方法来制作高度(n+1)树，而不仅仅是Node在高度n或较小的树上使用呢？更强大的方法是“分解”一棵高度n树，但我认为这有点难以看到。最后，我们想要认真思考如果我们发送maxT (Leaf undefined)或其他类似的病态值会发生什么。这些出现在 Haskell 中是因为它是一种（图灵完备的）计算机语言，而不是纯数学。老实说，尽管如此，这些小细节并不会改变你的情况。

于 2013-05-19T19:05:22.733 回答