[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Frédéric Blanqui]

Hi. Thanks for your explanations. However, the problem, at least for me, 
is that I am currently aware of no other tools for proving the 
termination of beta/iota-reduction on well typed terms in type systems 
with polymorphic types or/and inductive types.

Le 09/01/2014 16:42, Andrej Bauer a écrit :
>> 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.
>
> 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