[Agda] Normalisation before termination checking

[Nils Anders Danielsson]

On Wed, Jul 23, 2008 at 10:47 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
> 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.

"Just" adding sized types does make the language quite a bit more
complicated, so it is worth exploring the options. However, a more
semantic termination/productivity criterion would be nice, especially
for coinductive definitions, and I look forward to experimenting with
sized types in Agda, if they get implemented.

By the way, when you described sized types at the last AIM you
intended them to be used in conjunction with the current termination
checker (basically as a prior pass providing extra information to the
checker). What was the rationale for not scrapping size-change
termination entirely, and relying just on sized types?

> This is the systematic solution, normalization is just a clutch which
> then works in some cases.

But also with sized types there is scope for more or less ad-hoc
extensions, making the system easier to use on a day-by-day basis,
right? I suspect that the answer to my previous question goes along
those lines.

> We do not want to repeat Coq's mistakes, do we?

What mistake are you referring to here?

-- 
/NAD