[Agda] agda halting problem

[Nils Anders Danielsson]

On 2012-07-05 20:57, Andreas Abel wrote:
> Termination checking happens only after type-checking. This is a
> design flaw, and a long standing issue to be fixed.
>
>    http://code.google.com/p/agda/issues/detail?id=42
>
> It is in the back of my mind and should be implemented during the next
> major overhaul of the termination checker.

How do you plan to handle mutually recursive definitions? Let's say that
we have the following code:

   f : A
   g : B
   h : C

   f = a
   g = b
   h = c

We could use the following naive approach:

   1) Type-check A, B and C.
   2) Type-check a.
   3) Termination-check a.
   4) Type-check b.
   5) Termination-check a and b.
   6) Type-check c.
   7) Termination-check a, b and c.

However, the quadratic overhead of this approach seems scary.

-- 
/NAD