[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello, are you looking for Noetherian (well-founded) induction? There is an article here, which should provide a good starting point: https://en.m.wikipedia.org/wiki/Well-founded_relation - Burak On Jan 6, 2018 11:39 PM, "Richard Eisenberg" <[email protected]> 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> >
