[TYPES] Statement of structural induction

[Ben Sherman]

Hi Richard,

You may be interested in the following papers:

http://www.cse.chalmers.se/~peterd/papers/Wellorderings.pdf <http://www.cse.chalmers.se/~peterd/papers/Wellorderings.pdf>
Peter Dyber
Representing inductively defined sets by wellorderings in Martin-Löf's type theory
1996

http://www.cse.chalmers.se/~peterd/papers/ESSLLI94.pdf <http://www.cse.chalmers.se/~peterd/papers/ESSLLI94.pdf>
Thierry Coquand and Peter Dyber
Inductive definitions and type theory - an introduction
1997

In general, the sizes of structures can be represented as ordinals, and termination arguments can be described as demonstrating that recursive calls always occur on strictly smaller ordinals. The finite ordinals correspond to the natural number sizes that you refer to.

Your type [ty] is exactly what is known as “Brouwer ordinals,” which serve to represent countable ordinals (though I’m not sure of their exact relation to countable ordinals). There is a close relationship between Brouwer ordinals and W-types, which with a single set of judgments/axioms can encode likely all of the inductive datatypes that you’re thinking of (though schemes like induction-recursion require more complicated types than W-types, and I believe also more complicated ordinals than Brouwer ordinals).

Ben

> On Jan 6, 2018, at 2:23 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))
>  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>