[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Richard,
My master's thesis contains a rigorous proof of wellfoundedness of the
structural ordering on inductive types, including your example. There
is also a journal publication of this result at JFP.
http://www.cse.chalmers.se/~abela/publications.html#jfp02
http://www.cse.chalmers.se/~abela/publications.html#diplomathesis
Cheers,
Andreas
On 06.01.2018 23: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>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.a...@gu.se
http://www.cse.chalmers.se/~abela/
