<br><br><div class="gmail_quote">On Tue, Oct 18, 2011 at 1:54 PM, Nick Smallbone <span dir="ltr">&lt;<a href="mailto:nicsma@chalmers.se">nicsma@chalmers.se</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

Hi Agdaers,<br>
<br>
I&#39;m trying to use coinduction to model possibly-nonterminating<br>
functions:<br>
<br>
  module Delay where<br>
<br>
  open import Coinduction<br>
<br>
  data Delay (A : Set) : Set where<br>
    now : A → Delay A<br>
    later : ∞ (Delay A) → Delay A<br>
<br>
  fix : ∀ {A} → (Delay A → Delay A) → Delay A<br>
  fix f = later (♯ f (fix f))<br>
<br>
The idea is that Delay A represents a computation that may eventually<br>
produce a value of type A---or might not. As I understand it, fix is<br>
productive, but it doesn&#39;t seem to termination-check. Why&#39;s that?<br></blockquote><div><br></div><div>What if f is</div><div><br></div><div>f (later x) = ♭ x</div><div>f (now x) = now x</div><div><br></div><div>?</div>

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