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