[TYPES] Statement of structural induction

[Albert R Meyer]

We teach our students that it is a bad idea to replace structural induction
on recursive data types by integer induction, even when this is possible.
A reason for this is illustrated by the attached excerpt on win-lose games
from our text "Mathematics for Computer Science," where reduction to
integer induction is actually not possible.  The full text is available for
download at
   https://learning-modules.mit.edu/materials/index.html?uuid=
/course/6/fa17/6.042#materials


Yours truly,

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


On Sun, Jan 7, 2018 at 11:41 AM, Xavier Leroy <Xavier.Leroy at inria.fr> wrote:

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