<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jul 2, 2014 at 5:36 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</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></div><div class="">
> The problem is that findNatByContra never looks at the proof, so there<br>
> is no guarantee that it's a closed proof (which Thorsten mentioned<br>
> above).<br>
<br>
</div>Please, what is a closed proof?<br></blockquote><div><br></div><div>A closed proof is a proof that does not contain any free variables.</div><div> </div><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="">> For instance,<br>
><br>
> False : ℕ → Set<br>
> False _ = ⊥<br>
><br>
> decFalse : Decidable False<br>
> decFalse _ = no (λ x → x)<br>
><br>
> loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False<br>
> loopy H = findNatByContra False decFalse H<br>
><br>
><br>
> Here, loopy will happily evaluate forever with the hypothetical<br>
> (classical) proof that there is a number satisfying False. There is no<br>
> need to evaluate under the case since decFalse comes back 'no' for any<br>
> number.<br><br>
</div>Can you, please, explain further?<br>
<br>
To apply (loopy H), one needs to provide<br>
H : (∀ n → ¬ False n) → ⊥.<br>
<br>
And this is not possible, because its type normalizes to<br>
<br>
((n : ℕ) → (False n → ⊥)) → ⊥, and to ((n : ℕ) → (⊥ → ⊥)) → ⊥,<br>
<br>
and the type (n : ℕ) → (⊥ → ⊥) has a value (\n → id) in it.<br>
<br>
<br>
As one cannot provide any argument value to `loopy', how can it<br>
evaluate forever?<br></blockquote><div><br></div><div>The problem is that in Agda programs need to terminate not only at run-time</div><div>when you apply them to actual arguments, but also at type checking-time when</div>
<div>the type checker runs programs to check for equality. For instance, suppose</div><div>you define loopy as above and then try to prove that loopy always returns 42</div><div><br></div><div>thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42</div>
<div>thm _ = refl</div><div><br></div><div>In this case the type checker needs to evaluate loopy in the context of the</div><div>free variable H to check if it normalises to 42. This evaluation will not terminate</div><div>
with your definition of findNatByContra.</div><div><br></div><div>/ Ulf</div></div></div></div>