[TYPES] Statement of structural induction
burak.emir at gmail.com
Sat Jan 6 18:33:30 EST 2018
Hello, are you looking for Noetherian (well-founded) induction?
There is an article here, which should provide a good starting point:
On Jan 6, 2018 11:39 PM, "Richard Eisenberg" <rae at cs.brynmawr.edu> 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))
> 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
> 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.
> 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>
More information about the Types-list