Re: [TYPES] Statement of structural induction

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Yes, structural induction is, in a precise sense, equivalent to ordinal
induction -- which is why it is, again in a precise sense, more powerful
than integer induction.  Pedagogically, however, structural induction is
easy for beginning students to manage while they generally are at a loss to
cope with ordinals.

regards, a

Albert R. Meyer
Professor of Computer Science
Department of Electrical Engineering and Computer Science
MIT, Cambridge MA 02139


On Wed, Jan 10, 2018 at 5:31 AM, Frédéric Blanqui <[email protected]
> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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/ma
>> ilman/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
>>
>
>