多路（玫瑰）树的结构归纳
Structural induction for multi-way (rose) trees
由于多路树可以定义为递归类型：
data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]}
对该类型进行结构归纳是否有相应的原理？
要声明 属性 P 对所有 (*) 玫瑰树成立，您必须证明
- 如果
l :: [RoseTree]是玫瑰树的列表，其元素满足P，而x :: a是任意的，则Note x l满足P
关于P持有l的元素的部分是归纳假设，你可以用它来证明P(Node x l)。
这里没有明确的基本情况：这是因为没有明确的基本情况构造函数。然而，Node x [] 充当树的隐式基本情况，
事实上，当 l 为空时，我们隐式地得到了归纳的基本情况。具体地，当l为空时，假设"all the elements of l satisfy P"虚无成立，所以我们根据上面的归纳原理得到P(Node x [])
(*) 更准确地说，该原理证明了每个有限深度玫瑰树的 P。如果你真的必须考虑无限深度的（例如圆形树），你需要coinduction。
由于多路树可以定义为递归类型：
data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]}
对该类型进行结构归纳是否有相应的原理？
要声明 属性 P 对所有 (*) 玫瑰树成立，您必须证明
- 如果
l :: [RoseTree]是玫瑰树的列表，其元素满足P，而x :: a是任意的，则Note x l满足P
关于P持有l的元素的部分是归纳假设，你可以用它来证明P(Node x l)。
这里没有明确的基本情况：这是因为没有明确的基本情况构造函数。然而，Node x [] 充当树的隐式基本情况，
事实上，当 l 为空时，我们隐式地得到了归纳的基本情况。具体地，当l为空时，假设"all the elements of l satisfy P"虚无成立，所以我们根据上面的归纳原理得到P(Node x [])
(*) 更准确地说，该原理证明了每个有限深度玫瑰树的 P。如果你真的必须考虑无限深度的（例如圆形树），你需要coinduction。