[TYPES] Statement of structural induction

[Richard Eisenberg]

Many, many thanks to all who provided responses, several of which were off-list. I thought I'd summarize the bulk of responses.

What I did not explain in my original email -- but bears importance in how this all fits together -- is my mental model of induction. For a natural number induction of a proposition P : Nat -> Prop, we can imagine that, for any n, we can eventually build up a proof of P(n). We do this by starting by proving P(0), using that to prove P(1), using that (perhaps both of those) to prove P(2), and so on. After n+1 steps, we'll prove P(n). Thus, we can prove P(n) in finite time, for any finite n. Accordingly, we can conclude (forall n, P(n)).

However, this approach -- prove a proposition by building up a finite number of sub-proofs -- fails for my `ty`, below. (This `ty` is, by sheer coincidence, a representation of the ordinals, as used in, e.g., Abel and Altenkirch's http://www.cse.chalmers.se/~abela/foetuswf.pdf <http://www.cse.chalmers.se/~abela/foetuswf.pdf>) It would take an unbounded number of sub-proofs in order to prove a proposition over a `ty` made with `Mk`.

The insight I gained from the answers is that it's OK to require this unbounded number of sub-proofs. Equivalently, it might take an infinite amount of time to prove a proposition, but that doesn't cause trouble. The well-foundedness of this approach, called transfinite induction, is proved in Abel and Altenkirch's paper, above. I have not tried to digest it, but I trust the result. Indeed, some responses have pointed out that because structural induction is equivalent in power to transfinite induction, it might be easier to teach the latter by reference to the former.

Dybjer (http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf <http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf>) also gives a thorough treatment of inductive types. Having been satisfied by the Abel and Altenkirch paper, I have not dived into the details here, but it seems to address my concern, as well.

Another intriguing answer is that some aspect of mathematics is, and always will be, an article of faith. We can use the edifice of mathematics built up from, say, set theory to prove the well-foundedness of transfinite induction. Or, if we use type theory as the basis for mathematics, structural induction is taken as a given. Either way, we're basing our result on unprovable axioms.

Once again, thanks to all. I've learned a new nugget of knowledge through this interaction!
Richard

> On Jan 6, 2018, at 5: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>