<div dir="ltr"><div>Nice :)<br><br>I think making "findNatByContra" primitive may help. Or not?<br>Anyway, "loopy" is weakness of this particular implementation of MP, but not of MP itself.<br>(if I am not confused completely)<br>
<br></div>Dmytro<br><br></div><div class="gmail_extra"><br><br><div class="gmail_quote">2014-07-02 12:43 GMT+03:00 Altenkirch Thorsten <span dir="ltr"><<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><div>Thank you for the correction, Ulf.</div>
<div><br></div><span><div style="font-family:Calibri;font-size:11pt;text-align:left;color:black;BORDER-BOTTOM:medium none;BORDER-LEFT:medium none;PADDING-BOTTOM:0in;PADDING-LEFT:0in;PADDING-RIGHT:0in;BORDER-TOP:#b5c4df 1pt solid;BORDER-RIGHT:medium none;PADDING-TOP:3pt">
<span style="font-weight:bold">From: </span> Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>><br><span style="font-weight:bold">Date: </span> Wed, 2 Jul 2014 10:12:36 +0100<br>
<span style="font-weight:bold">To: </span> txa <<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>><br><span style="font-weight:bold">Cc: </span> Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>>, "<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><div class="">
<br><span style="font-weight:bold">Subject: </span> Re: [Agda] termination by contradiction<br></div></div><div><br></div><div dir="ltr"><br><div class="gmail_extra"><br><div><div class="h5"><br><div class="gmail_quote">On Tue, Jul 1, 2014 at 10:04 PM, Altenkirch Thorsten <span dir="ltr"><<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div><br><br>
On 01/07/2014 20:40, "Sergei Meshveliani" <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br><br>
><br>
>Consider the example:<br>
><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></div><div><br></div>In Agda we need to execute programs with variables. This is usually called<br>
symbolic evaluation. It is important that symbolic evaluation terminates<br>
otherwise the type checker will hang.<br><br>
In Agda every recursive program can be computed until it gets stuck.<br>
However, it is not clear what this means for findFrom. If we recursively<br>
unfold findFrom evaluation will not terminate.<br><br>
I guess you have an operational semantics in mind which does not unfold<br>under the case. While this seems reasonable (and solves the problem) it is<br>
not without problems.<br></blockquote><div><br></div><div>The problem isn't evaluation under the case. The case is just shorthand for a helper function that does the pattern matching, so you get the appropriate semantics. The problem is that findNatByContra never looks at the proof, so there is no guarantee that it's a closed proof (which Thorsten mentioned above). For instance,</div>
<div><br></div><div>False : ℕ → Set</div><div>False _ = ⊥</div><div><br></div><div>decFalse : Decidable False</div><div>decFalse _ = no (λ x → x)</div><div><br></div><div>loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False</div><div>
loopy H = findNatByContra False decFalse H</div><div><br></div><div>Here, loopy will happily evaluate forever with the hypothetical (classical) proof that there is a number satisfying False. There is no need to evaluate under the case since decFalse comes back 'no' for any number.</div>
<div><br></div><div>/ Ulf</div></div></div></div></div></div></span></div>
<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></blockquote></div><br></div>