私は問題があります。
maxT二分木からノードの最大値を返す Haskellの関数を実装する必要があります。
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))
これは正しいですか？
質問する
3761 次
1 に答える
4
これが正しいことを証明するのがどれほど難しいか見てみましょう。なんで？プログラムのエラーを分析する優れた方法だからです。特に再帰的なもの。技術的には誘導を使用しますが、それほど複雑ではありません。重要なのは、maxT t常にツリー内の最大値でなければならないことを認識することですt。この宣言、「maxT t常にツリー内の最大値でなければならないt」は不変条件と呼ばれ、それを証明しようとします。
tまず、が であると仮定しましょうLeaf。この場合、定義済みであり、このツリーにmaxT (Leaf a) = aは文字通り他の値がないため、最大でa なければなりません。したがって、maxTa が渡されたときに不変条件が維持されますLeaf。これが「ベースケース」です。
ここで、 、、およびを lett = Node (Leaf a) b (Leaf c)にするとどうなるかを考えてみましょう。これは高さ 1 のツリーであり、誘導の「事例」と呼ばれるものを形成します。不変式が成り立つか試してみましょう。IntegerabcmaxT
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最大の値を返すと仮定して喜んでいます。ここで詳細を選択することもできますが、高さ 1 のツリー全体の最大値を計算するための関連情報がすべて与えられていることは明らかです。これは、高さ 0 の木と高さ 1 の木 ( s とs のみを含むs ) の両方で機能する成功した証明と言えます。abmax b (max a c)NodemaxTLeafNodeLeaf
次のステップは、この例のケースを一般化することです。
では、同じパターンを木の高さに一般化して適用してみましょう。ある数値 を修正するとどうなるかを尋ね、高さ以下のすべての不変条件を維持するnと仮定します。これは少し奇妙です。なぜこれが機能するのかは、少し後で明らかになります。maxT ttnn = 0n = 1
では、その仮定は私たちに何をもたらすのでしょうか? Treeでは、高さn以下の任意の 2 つ (それらlを and と呼びますr)、任意の整数を取りx、それらを組み合わせて新しい tree を形成しましょう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支持しています。次に、maxes のチェーンは、現在、高さのツリーに対して不変条件を維持し続けtます(n+1)。Treeさらに (これは非常に重要です)、新しいsを組み立てるプロセスは一般的です。この方法では、任意の高さツリーを作成できます。(n+1)これはmaxT、任意の高さ(n+1)ツリーで機能することを意味します。
誘導タイム！を選択し、n(何らかの理由で) それmaxTが任意の高さnツリーで機能すると信じる場合、それはすぐに任意の高さ(n+1)ツリーで機能するはずです。を選びましょうn = 0。s でmaxT機能する「基本ケース」でわかっているので、高さツリーで機能することが突然わかります。これが私たちの「事例」でした。さて、その知識があれば、すぐに高さの木の働きを見ることができます。そして高さの木。そして高さ- . などなど。LeafmaxT1maxT234
maxTこれで正しい証明*が完成しました。
※注意事項をいくつか残しておきます。max意味はありますが、チェーンが機能することを示すために、実際には面倒な詳細は行いませんでした. また、誘導ステップが機能することを実際に証明したわけでもありません。高さ以下のツリーで使用する(n+1)以外に、高さツリーを作成する方法が他にもあるとしたらどうでしょうか? より強力な方法は、高さツリーを「ばらばらにする」ことですが、それは少しわかりにくいと思います。最後に、そのような病理学的値を送信した場合に何が起こるかについて、真剣に考えたいと思います。Haskell は純粋な数学ではなく (チューリング完全な) コンピューター言語であるため、これらは Haskell で発生します。正直なところ、これらの小さな部分は、状況によって大きく変わるわけではありません.NodennmaxT (Leaf undefined)
于 2013-05-19T19:05:22.733 に答える