[ 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 >> > >
