私はどのようにinorder + preorderが一意のバイナリツリーを構築するのかを見ていましたか? Idris で正式な証明を書くのは楽しいだろうと考えました。残念ながら、ツリー内の要素を検索する方法が、順序通りに検索する方法に対応していることを証明しようとして、かなり早い段階で行き詰まってしまいました (もちろん、事前順序検索でもそれを行う必要があります)。 . どんなアイデアでも大歓迎です。私は完全な解決策には特に関心がありません。それ以上のことは、正しい方向への出発点に役立つだけです。
与えられた
data Tree a = Tip
| Node (Tree a) a (Tree a)
少なくとも 2 つの方法でリストに変換できます。
inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r
また
foldrTree : (a -> b -> b) -> b -> Tree a -> b
foldrTree c n Tip = n
foldrTree c n (Node l v r) = foldr c (v `c` foldrTree c n r) l
inorder = foldrTree (::) []
2 番目のアプローチはほとんどすべてを困難にするように思われるため、私の努力のほとんどは最初のアプローチに集中しています。ツリー内の場所を次のように説明します。
data InTree : a -> Tree a -> Type where
AtRoot : x `InTree` Node l x r
OnLeft : x `InTree` l -> x `InTree` Node l v r
OnRight : x `InTree` r -> x `InTree` Node l v r
inorder（ の最初の定義を使用して）書くのはとても簡単です
inTreeThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t
結果はかなり単純な構造になり、証明にはかなり適しているようです。
のバージョンを書くこともそれほど難しくありません。
inorderThenInTree : x `Elem` inorder t -> x `InTree` t
inorderThenInTree残念ながら、これまでのところ、の逆であることを証明できた のバージョンを書く方法を思いつきませんでしinTreeThenInorderた。私が思いついた唯一の用途
listSplit : x `Elem` xs ++ ys -> Either (x `Elem` xs) (x `Elem` ys)
私はそこを通り抜けようとしてトラブルに遭遇します。
私が試したいくつかの一般的なアイデア：
Vect代わりにを使用Listすると、左側にあるものと右側にあるものを理解しやすくなります。その「緑のスライム」にはまってしまいました。木の根元での回転が十分に根拠のある関係につながることを証明するまで、木の回転をいじってみました。（これらの回転について何かを使用する方法を理解できなかったため、以下の回転をいじりませんでした）。
ツリー ノードに到達する方法に関する情報でツリー ノードを装飾しようとしています。そのアプローチで何か面白いものを表現する方法が思いつかなかったので、私はこれにあまり時間をかけませんでした。
そうする関数を構築しながら、開始した場所に戻るという証拠を構築しようとしています。これはかなり厄介になり、どこかで行き詰まりました。