[TYPES] Statement of structural induction
xavier.leroy at inria.fr
Tue Jan 9 11:14:59 EST 2018
On 07/01/2018 17:41, Xavier Leroy wrote:
> As your example shows, the tree can contain infinitely-branching nodes, hence the size can be infinite, but all paths are finite, hence the height is finite.
I was confused. All paths in this tree are finite indeed, and that's why it induces a well-founded ordering. But in the presence of infinitely-branching nodes, the height can still be infinite and is not an appropriate justification for structural induction.
Sorry for the noise,
- Xavier Leroy
More information about the Types-list