[TYPES] Statement of structural induction

[Frédéric Blanqui]

Hello.

Well, it is if you define the height as a transfinite ordinal. In case 
of an infinitely branching constructor like Mk : (nat -> ty) -> ty, 
height(Mk f) = sup{height(f n) | n in nat} + 1.

Frédéric.


Le 09/01/2018 à 17:14, Xavier Leroy a écrit :
> [ 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