[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 >
