[Agda] hot computer churns codata

[Nils Anders Danielsson]

On 2009-05-20 09:24, Conor McBride wrote:

> This command line thing: is it a recent return to the old ways?

No.

> Maybe I should upgrade, but I always worry about what else I'll have
> to upgrade...)

Nowadays it should be very easy to upgrade, assuming that you have
installed the Haskell Platform (http://hackage.haskell.org/platform/),
and instructed cabal-install to install things onto your PATH. Just run

  cabal install Agda-executable.

If you have not upgraded for a while I suggest that you also remove the
Agda-related settings from your .emacs and then run

  agda-mode setup.

This is documented in more detail in the README.

> It's hard to see where the termination check is even being
> engaged.

My guess is that that the final type-checked term, including all
inferred implicit arguments, is huge, and that it takes a long time for
the termination checker simply to (force and) traverse it.

> If we're really lucky, we might be able to code those nice
> proofs Ralf H has been doing, proving corecursions equal
> by showing they satisfy the same unfolding equation.

I have done some of his proofs in Agda:

  http://www.cs.nott.ac.uk/~nad/listings/codata/README.html.

If all relevant functions are represented as constructors his proofs
turn out to be instances of guarded coinduction.

-- 
/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.