多方向（バラ）木の構造誘導 - ハスケ、樹木、プルーフ、誘導

多方向ツリーは再帰型として定義できるので

data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]}

このタイプで構造誘導を実行するための対応する原則はありますか？

回答：

その性質を述べるために P すべての（*）バラの木に当てはまります、あなたはそれを証明しなければなりません

• if l :: [RoseTree] 要素が満たすバラの木のリストです P、および x :: a 任意です Note x l 満たしている P

その部分について P の要素を保持 l 帰納仮説であり、証明に使用できます。 P(Node x l).

ここには明示的なベースケースはありません。これは、明示的なベースケースコンストラクタがないためです。 Node x [] 木のための暗黙のベースケースとして振る舞う、 そして確かにいつ l 空の場合は、帰納法の基本ケースが暗黙的に得られます。具体的には、仮説「のすべての要素 l 満たす P「真実になると l 空ですので、 P(Node x []) 上記の誘導原理から。

（*）もっと正確に言えば、この原則は証明する P すべての有限深さのバラの木に対して。無限の深さのもの（円形の木など）を本当に考慮する必要がある場合は、coinductionが必要です。