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

[Prof. Robert Harper]

that would be an application of markov's principle, i think, which would in effect add a new form of function of Pi-Sigma type.  andrej most probably knows the implications of this.  hugo herbelin has written about it recently, but i am not familiar with the result off the top of my head.

bob

Sent from tablet

> On Jan 7, 2014, at 9: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 to HomotopyTypeTheory+unsubscribe at googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.