[Agda] Termination checking failure

[Nils Anders Danielsson]

On 2009-11-22 12:28, Ivan Tomac wrote:
> How would I go about rewriting the code in the attached file so that it
> passes termination checking?

The following code works:

  map : ∀ {A B} → (A → B) → Stream A → Stream B
  map f (cons x xs) = cons (f x) (♯ map f (♭ xs))

  sequence : ∀ {A} → Stream (Id A) → Id (Stream A)
  sequence = id ∘ map unId

> And why is the termination checker failing in first place?

Because the corecursive call is not guarded by constructors.

> I would appreciate any pointers to papers, articles or books.

You may want to have a look at "Mixing Induction and Coinduction":

  http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.