<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jul 1, 2014 at 10:04 PM, Altenkirch Thorsten <span dir="ltr">&lt;<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>&gt;</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 class=""><br>
<br>
On 01/07/2014 20:40, &quot;Sergei Meshveliani&quot; &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt; wrote:<br><br>
&gt;<br>
&gt;Consider the example:<br>
&gt;<br>
&gt;  findNatByContra :<br>
&gt;           (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
&gt;<br>
&gt;  findNatByContra P P? _ =  findFrom 0<br>
&gt;    where<br>
&gt;    findFrom : ℕ → Σ ℕ P<br>
&gt;    findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
&gt;                                ; (no _)   → findFrom (suc n) }<br>
&gt;<br></div><div class="">
<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&#39;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&#39;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 &#39;no&#39; for any number.</div>

<div><br></div><div>/ Ulf</div></div></div></div>