问题描述:

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.