问题描述:

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.

相关阅读:
Top