<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"><<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 class=""><br>
<br>
On 01/07/2014 20:40, "Sergei Meshveliani" <<a href="mailto:mechvel@botik.ru">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 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'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>