[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The old Agda wiki has an article ( http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker ) which defines the structurally-smaller relation <. Note that it's defined on untyped syntax. James On 06/01/18 22:23, Richard Eisenberg wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Does anyone know a place I could see a statement of how structural induction > works, spelled out in full detail? I don't need a "canonical" (i.e. citable) > reference, per se, but a place I can enhance my own understanding of > structural induction. > > 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. > > Fixpoint f (t : ty) : nat := > match t with > | Ax => 1 > | Suc t' => 1 + f t' > | Mk x => 1 + (f (x 2)) > end. > > Note that there's no good way (that I see) of denoting the size of such a > structure. And yet, Coq feels confident that my f will terminate. Indeed, I > certainly don't have a counterexample to this, and I don't believe there is > one. > > So, I'm looking for a description of structural induction that explains how > the function above is terminating in a rigorous way. Bonus points if it also > shows how non-strictly-positive recursive occurrences of a type in its own > definition cause structural induction to fail. > > Thanks! > Richard > > -=-=-=-=-=-=-=-=-=-=- > Richard A. Eisenberg, PhD > Asst. Prof. of Computer Science > Bryn Mawr College > Bryn Mawr, PA, USA > cs.brynmawr.edu/~rae <http://cs.brynmawr.edu/~rae>
