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

[Vladimir Voevodsky]

BTW what the general theory says about applying classical logic for termination checking? Can this be sensibly expressed in the eliminator language?

V.



On Jan 7, 2014, at 6:36 AM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:

> 
> 
> On 07/01/14 10:01, Frédéric Blanqui wrote:
>> Nowadays, one can automatically certify in proof assistants like Coq or
>> Isabelle/HOL quite complex termination proofs (see the website of the
>> termination competition http://termcomp.uibk.ac.at/termcomp/home.seam).
>> So, it would be a pity not to take advantage of this for making the life
>> of proof assistants users easier, and allow them to define functions (or
>> enrich the equivalence on types) in ways that can hardly (or cannot) be
>> translated into eliminators. This is for instance the case of function
>> definitions based on general rewriting theory. This of course may raise
>> problems for making sure that such definitions are consistent, but it is
>> another (interesting) problem.
> 
> The problem is that if you accept general recursive terminating
> definitions, you are in fact realizing new axioms that are not
> available in MLTT.
> 
> For example, once I and Paulo Oliva defined Bar Recursion in Agda (by
> disabling non-termination checking in a short module) to realize the
> Double Negation Shift (DNS), and used this to prove a form of the
> Infinite Pigeonhole Principle, so that canonicity for ground types is
> retained.
> 
> However, the DNS is certainly *not* provable in MLTT (in any of its
> flavours).
> 
> Similarly, you can realize other principles by having general
> recursion, such as the uniform continuity (UC) of all functions
> (N->Bool)->N.
> 
> And so on.
> 
> Even assuming that this wouldn't violate consistency, you have a
> problem: while UC may be consistent with Univalence (UA), it certainly
> negates excluded middle, and the HoTT people want HoTT to be
> compatible with excluded middle (EM), and with choice too (AC), which
> it is, but not if you add something like UC.
> 
> I am not saying that your termination checker will be able to check
> the termination of UC. But it may check the termination of a realizer
> of an axiom that contradicts EM or AC, or even UA.
> 
> Also, even if you forget about HoTT, it is not clear what new axioms
> you are adding when you allow general recursion, and the supply of new
> axioms you get will (necessarily) depend on the particularities of
> your termination checker (as there is no general termination checker),
> and so we won't be sure precisely what axioms we are adding to
> MLTT in this way.
> 
> That's why, as Thorsten says, it would be very good to have as a
> meta-theorem that any termination-checked Agda program can be
> in principle translated to eliminators (even if we decide not to do
> that in practice).
> 
> M.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda