[Agda] Normalisation before termination checking

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Nils Anders Danielsson wrote:
> On Tue, Jul 22, 2008 at 8:06 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>> Can you explain what the exact problem is? There might be a theoretical
>> problem behind this, and making a quick adhoc fix might not be the
>> right solution.
> 
> Let us say that you have two guarded definitions,
> 
>   a ~ c₁ e₁ (c₂ (e₂ i) a)
>   b ~ c₁ e₁ (c₂ (e₂ j) b),
> 
> where c₁ and c₂ are codata constructors, and e₁ and e₂ are arbitrarily
> large expressions not involving a and b. In this case you cannot
> abstract out the common part of the definitions, because the resulting
> code is not guarded:
> 
>   f x y = c₁ e₁ (c₂ (e₂ x) y)
>   a ~ f i a
>   b ~ f j b.

What you really want so say here is that f is *guarding*, since it adds
two constructors onto y.  So, just allow the type system to express this
=> use sized types.  Then you can abstract out f to anywhere, even to
another module, or even make it a postulate.

This is the systematic solution, normalization is just a clutch which
then works in some cases.  We do not want to repeat Coq's mistakes, do we?

Cheers,
Andreas


- --
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFIhv46PMHaDxpUpLMRAki0AJ9KqsrJsBEJajckLZ19ubm8XwrdBACgl0yN
nadQ8RM3pjoJ40vSh4fncQk=
=BaLT
-----END PGP SIGNATURE-----