Re: [TYPES] Statement of structural induction

[ 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>
>