[TYPES] Statement of structural induction

Frédéric Blanqui frederic.blanqui at inria.fr
Wed Jan 10 05:31:28 EST 2018


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.


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

More information about the Types-list mailing list