The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

On 01/09/2014 10:42 AM, Andrej Bauer wrote:
> > Sorry but I don't really understand Andrej and Mathieu's last mails. In
> > size-based termination, there is no ordinal in the type system itself.
> > Ordinals are just used in the meta-theory to justify that, indeed, every
> > well typed term terminates.
> I was just pointing out that well-founded relations are the correct
> notion to use.
>
> Ordinals require classical logic so you'll burn when you try to bring
> measures of termination from meta-theory down to theory. For instance,
> what happens if you want to formalize the meta-theory? You can only
> sensibly formalize ordinals if you have excluded middle, otherwise
> they get weird.
    They get weird, but they suffice for our purposes. As Bruno pointed 
out, ordinals can be formalized just fine in IZF, but they have the 
bizarre property of being neither linear, nor have the "successor/limit" 
property: in general it is not true that an ordinal is either a 
successor or a limit.

    Conveniently, neither of these properties is required to carry out 
the meta-theory of sized-types. Can we carry out the same formalization 
using measures and well-founded induction? It's likely, but it would be 
nice to have a single, unified rule for defining recursive functions.

    The real question is: what is required for a function definition, 
and what computation rules result? If we only have recursors, then we 
can define functions by well-founded recursion, and all is fine, except 
when we get around to actually having to prove things about recursive 
functions.

    Mathieu pointed out that with sufficiently heavy elaboration on top 
of this, we can "hide" the difficulties behind nice ad-hoc induction 
principles and adding enough "steam" to the acc type to be able to 
unfold open terms. Maybe this is the way to go, but certainly efficiency 
will be lost at the conversion stage, where huge terms with recursors 
and proofs of well-foundedness will be floating around.


    I guess I'm getting off track here, so I'll just finish with this 
remark: ordinals are simply a useful -approximation- to the shape of a 
term, which in turn can be manipulated to give a nice type-based 
criterion for size decrease in recursive calls. This is all size-based 
termination is. We all agree that the fact that ordinals are 
well-ordered (classically) is not fundamental, but nevertheless I don't 
see any well-studied alternative to measure decrease in recursive calls. 
Like I tried to say above, having a user define the well-founded order 
for each recursive function, or more likely having Coq fill in the 
blanks each time has some drawbacks.


Best,


Cody



> Ordinals are well-founded and *linear*, and there will be cases where
> the well-founded part is readily available, but the linearity
> requirement just gets in the way. Since linearity is not needed to
> show termination, why would we insist on it? For instance, if we want
> an automated tool for proving termination, why bother with linearity
> when all we need is well-foundedness? (Does Agda termination checker
> use ordinals?)
>
> So I really do not see an advantage to using ordinals, except perhaps
> easy notation. But I am not actually ruling out ordinals, I am just
> saying that we should use the more general well-founded relations, so
> the ordinal notations are still there for those cases where they are
> the best thing to use.
>
> With kind regards,
>
> Andrej