The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi Dan,

Thanks for the additional reference and your explanation. I will have  
to take some time to study it, but I am now convinced that you are  
right: since the ordinals are well-founded, ordinal induction is just  
well-founded induction and therefore describes a terminating process.

It would be nice to see how ordinals can be used to do some (simple)  
proofs in Coq. While preparing a talk about ordinals for our research  
students (http://www.cs.tcd.ie/Edsko.de.Vries/talks/ordinals.pdf) I  
defined a small process language with an infinitely branching choice  
operator. I figured that I wouldn't be able to write an evaluator for  
this language in Coq because I thought that for a constructor (Sum :  
(nat -> Proc) -> Proc) of the language, given (Sum f), (f n) would not  
considered to be a subterm. Then I could do a termination proof using  
ordinals and then define the evaluator by transfinite recursion. But  
of course, it turns out that (f n) *is* considered a subterm and so  
the evaluator is easily definable :)

In fact, the whole reason I started looking at ordinals was a proof  
about modal logic and bisimulation, which Milner did by transfinite  
induction on the depth of the formula (which has an infinitely  
branching conjunction, and the depth must therefore be an ordinal).  
But since the depth of the trees is always finite (even if we cannot  
compute it without ordinals), 'ordinary' structural induction on these  
formulae should suffice (just like I could do structural induction on  
my process language). (Milner uses the depth to index the bisimulation  
too, so he has a separate need for it.)

Anyway, I feel a lot happier about transfinite induction now! Thanks  
again,

Edsko