[TYPES] Statement of structural induction

[James Wood]

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>