haskell - 多路（玫瑰）树的结构归纳

Question

由于多路树可以定义为递归类型：

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

对这种类型进行结构归纳有相应的原则吗？

Answer 1

要声明该属性P适用于所有 (*) 玫瑰树，您必须证明

• ifl :: [RoseTree]是一个玫瑰树列表，其元素满足P，并且x :: a是任意的，则Note x l满足P

关于P保持元素的部分l是归纳假设，您可以使用它来证明P(Node x l)。

这里没有明确的基本情况：这是因为没有明确的基本情况构造函数。然而，Node x []作为树的隐式基本情况，实际上当l为空时，我们隐式地得到归纳的基本情况。l具体而言，假设“满足的所有元素P”在为空时变为空虚l，因此我们P(Node x [])从上面的归纳原理得到。

(*) 更准确地说，这个原理P适用于每棵有限深度的玫瑰树。如果你真的必须考虑无限深度的（例如圆形树），你需要共归纳。