[TYPES] Statement of structural induction

Albert R Meyer ameyer at mit.edu
Sun Jan 7 15:02:57 EST 2018

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

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

More information about the Types-list mailing list