[TYPES] Statement of structural induction

[Richard Eisenberg]

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>