当前位置: 动力学知识库 > 问答 > 编程问答 >

haskell - Structural induction for multi-way (rose) trees

问题描述:

Since multi-way trees can be defined as a recursive type:

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

is there a corresponding principle for performing structural induction on this type?

网友答案:

To state that property P holds for all (*) rose trees, you have to prove that

  • if l :: [RoseTree] is a list of rose trees whose elements satisfy P, and x :: a is arbitrary, then Note x l satisfies P

The part about P holding on the elements of l is the induction hypothesis, which you can use to prove P(Node x l).

There is no explicit base case here: this is because there's no explicit base case constructor. Yet, Node x [] acts as an implicit base case for the trees, and indeed when l is empty we get a base case for induction implicitly. Concretely, the hypothesis "all the elements of l satisfy P" becomes vacuously true when l is empty, so we get P(Node x []) from the induction principle above.

(*) More precisely, this principle proves P for every finite-depth rose tree. If you really have to consider infinite-depth ones (e.g. circular trees), you need coinduction.

分享给朋友:
您可能感兴趣的文章:
随机阅读: