[TYPES] Statement of structural induction

[Xavier Leroy]

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