[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 01/06/2018 11:23 PM, Richard Eisenberg wrote: > My problem is that I had been blithely assuming that structural induction was > reducible to natural-number induction, where the natural number was the size > (number of nodes in the tree) of the structure. But this is clearly not true, > as both Coq and Agda accept this (written in Coq notation): > > Inductive ty := > | Ax : ty > | Suc : ty -> ty > | Mk : (nat -> ty) -> ty. The reduction to natural-number induction works if you consider the height of the tree representing the data structure a tree, instead of its size. As your example shows, the tree can contain infinitely-branching nodes, hence the size can be infinite, but all paths are finite, hence the depth is finite. Recursing from a node to one of its children decreases the height. Hope this helps, - Xavier Leroy
