<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&#39;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 &quot;similar&quot; (probably &quot;similar&quot; 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">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
To my<br>
<br>
&gt; &gt; [..]<br>
<div class="">&gt; &gt; is it possible in Agda to prove termination of a function by programming<br>
&gt; &gt; a<br>
&gt; &gt;        negation of non-termination             -- call it  method  (M)<br>
&gt; &gt;<br>
&gt; &gt; (deriving an absurd from assuming an infinite work of the algorithm)<br>
&gt; &gt; ?<br>
&gt; &gt;<br>
&gt; &gt; A.A.Markov wrote that this provides a wider class of constructive<br>
&gt; &gt; objects, and that this is intuitive enough.<br>
&gt; &gt;<br>
&gt; &gt; My current termination proofs in Agda use only a simple approach by<br>
&gt; &gt; providing an upper bound for a certain counter. And I have an impression<br>
&gt; &gt; that (M) gives something wider.<br>
</div>&gt; &gt; [..]<br>
&gt; &gt; [..]<br>
<div class="">&gt; &gt; How to express this in Agda ?  Needs it to be expressed?<br>
<br>
<br>
</div>Frédéric Blanqui wrote on June 30<br>
&gt; [..]<br>
<div class="">&gt; I think that you need some axioms (dependent choice and excluded<br>
&gt; 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>
&gt; and related files (SN, InfSeq, NotSN).<br>
</div>&gt; [..]<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&#39;, it is only<br>
    for termination.<br>
But is this possible? Can this lead logically to a total excluded `or&#39; ?<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&#39; ?<br>
Can (3) be replaced in Agda with something that avoids<br>
NO_TERMINATION_CHECK and `postulate&#39; ?<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>
&gt; &gt;<br>
&gt; &gt; Thanks,<br>
&gt; &gt;<br>
&gt; &gt; ------<br>
&gt; &gt; Sergei<br>
&gt; &gt;<br>
&gt; &gt; _______________________________________________<br>
&gt; &gt; Agda mailing list<br>
&gt; &gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<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>