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

[Matthieu Sozeau]

If you believe in Coq with Prop and in particular Acc then you can use classical
logic to prove a relation is well founded and then use that with the eliminator 
for Acc even to build things in Set. The culprit is that the proof is an open 
term (uses an axiom) and reduction will get stuck (but you can add tons of "fuel” 
to avoid that in practice).  Same situation happens without Prop actually, 
but using classical logic in Set then potentially destroys also nat’s 
computational content for example. Does that answer your question?

— Matthieu

On 7 janv. 2014, at 15:39, Vladimir Voevodsky <vladimir at ias.edu> wrote:

> 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
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email toHomotopyTypeTheory+unsubscribe at googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.