[Agda] My coinductive function doesn't termination-check

[Ulf Norell]

On Tue, Oct 18, 2011 at 1:54 PM, Nick Smallbone <nicsma at chalmers.se> wrote:

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

What if f is

f (later x) = ♭ x
f (now x) = now x

?

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111018/f8f3d46e/attachment.html