查找樹中節點的最大值

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中，因爲它是一種（圖靈完備的）計算機語言，而不是純數學。老實說，儘管如此，這些小小的東西並沒有改變你的情況。