[Agda] mu-nu in Agda

[Thorsten Altenkirch]

Hi Nisse,
CC: Tarmo, Keiko, Agda

I have discussed mixed induction/coinduction with Tarmo and Keiko. We
tried to adopt their approach for representing νμ in Coq to represent
μν in Agda. Indeed it is possible (see attached file) but the use of
impredicativity destroys normalisation (try to normalize "f
bad"). While I assume "Type:Type" System F style impredicativity would
be sufficent (you only need a "weak large Σ-type to encode T, indeed
this is the type-theoretic representation of a left Kan extension).

I remember that Thierry once remarked that the structural order in a
impredicative system isn't always well-founded. I think this example
is an instance. Also, Coq seems to avoid this problem by checking that
structural recursion may only use "recursive arguments", hence the Coq
terminationchecker isn't untyped.

We were also wondering wether it would be already possible to encode
this example using a predicative hierarchy (which would be bad). Do
you see a way to do this? I don't.

Cheers,
Thorsten
-------------- next part --------------
A non-text attachment was scrubbed...
Name: TarmoTree.agda
Type: application/octet-stream
Size: 947 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100529/64e15f5b/TarmoTree.obj
-------------- next part --------------