[TYPES] Statement of structural induction

[Andreas Abel]

Richard,

My master's thesis contains a rigorous proof of wellfoundedness of the 
structural ordering on inductive types, including your example.  There 
is also a journal publication of this result at JFP.

   http://www.cse.chalmers.se/~abela/publications.html#jfp02
   http://www.cse.chalmers.se/~abela/publications.html#diplomathesis

Cheers,
Andreas

On 06.01.2018 23: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>
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/