<div dir="ltr"><div><div><div><div>Hello,<br><br></div>You are definitelly able to add new axioms to constructive logic if you are sure (you have an evidence in theory or in meta-theory) it will not lead to inconsistency.<br>
</div>And from that point of view Markov axiom is Ok.<br></div>The only problem is that people didn't find nice (non-adhoc) way to put this axiom in theory (if I am not mistaking).<br></div><div><br></div><div>NB You can add this axiom only for types like Nat or "similar" (probably "similar" here means сardinality).<br>
For example adding such axiom for Float will lead to infinite loop.<br><br></div><div>Best regards,<br></div><div>Dmytro<br></div><div><div><div><div><div><br></div></div></div></div></div></div><div class="gmail_extra"><br>
<br><div class="gmail_quote">2014-07-01 12:47 GMT+03:00 Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
To my<br>
<br>
> > [..]<br>
<div class="">> > is it possible in Agda to prove termination of a function by programming<br>
> > a<br>
> > negation of non-termination -- call it method (M)<br>
> ><br>
> > (deriving an absurd from assuming an infinite work of the algorithm)<br>
> > ?<br>
> ><br>
> > A.A.Markov wrote that this provides a wider class of constructive<br>
> > objects, and that this is intuitive enough.<br>
> ><br>
> > My current termination proofs in Agda use only a simple approach by<br>
> > providing an upper bound for a certain counter. And I have an impression<br>
> > that (M) gives something wider.<br>
</div>> > [..]<br>
> > [..]<br>
<div class="">> > How to express this in Agda ? Needs it to be expressed?<br>
<br>
<br>
</div>Frédéric Blanqui wrote on June 30<br>
> [..]<br>
<div class="">> I think that you need some axioms (dependent choice and excluded<br>
> middle). See<br>
<a href="http://color.inria.fr/doc/CoLoR.Util.Relation.NotSN_IS.html" target="_blank">http://color.inria.fr/doc/CoLoR.Util.Relation.NotSN_IS.html</a><br>
> and related files (SN, InfSeq, NotSN).<br>
</div>> [..]<br>
<br>
<br>
I would like to add some comments and to ask some questions.<br>
<br>
(1) (M) does not intend to introduce a total excluded `or', it is only<br>
for termination.<br>
But is this possible? Can this lead logically to a total excluded `or' ?<br>
<br>
(2) Can anybody give a simple example of and algorithm for which there<br>
is a simple termination proof by (M) and it is difficult to provide a<br>
termination proof without using (M) ?<br>
(I recall that there are many statements in classical mathematics for<br>
which it is difficult to provide a proof other than by assuming some<br>
particular infinite sequence and deriving a contradiction from this).<br>
<br>
(3) What can be a axiom for (M) in an Agda program:<br>
<br>
{-# NO_TERMINATION_CHECK #-}<br>
findNatByContra :<br>
(P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
<br>
findNatByContra P P? _ = findFrom 0<br>
where<br>
findFrom : ℕ → Σ ℕ P<br>
findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
; (no _) → findFrom (suc n) }<br>
<br>
I think that this occurrence of NO_TERMINATION_CHECK expresses (M) for<br>
all predicates on ℕ,<br>
and findNatByContra together with this occurrence of<br>
NO_TERMINATION_CHECK present the needed axiom with respect to ℕ.<br>
<br>
Right?<br>
May this lead to a total excluded `or' ?<br>
Can (3) be replaced in Agda with something that avoids<br>
NO_TERMINATION_CHECK and `postulate' ?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
> ><br>
> > Thanks,<br>
> ><br>
> > ------<br>
> > Sergei<br>
> ><br>
> > _______________________________________________<br>
> > Agda mailing list<br>
> > <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>