Re: [TYPES] Statement of structural induction

Xavier Leroy <[email protected]>
Newsgroups gmane.comp.science.types
Message-ID <[email protected]> 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.