<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; 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 id="OLK_SRC_BODY_SECTION"><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">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">psztxa@exmail.nottingham.ac.uk</a>><br><span style="font-weight:bold">Cc: </span> Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>>, "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br><span style="font-weight:bold">Subject: </span> Re: [Agda] termination by contradiction<br></div><div><br></div><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></span></body></html>