[Agda] Termination problems with "with" and recursion

[Andreas Abel]

Your explanation of you mergeO fails to termination-check is accurate.

I guess Idris does like Coq and only regards the recursive arguments of 
constructors such as ocons.  This means that x, y, blex, bley, xlex, 
ylex are ignored in ocons and only xs and ys matter.

We could implement this as well, but it would be incompatible with

   --guardedness-preserving-type-constructors

which, I'd guess, no one uses in practice...

My suggestion is to use --sized-types, then you can say yourself which 
are the recursive arguments of ocons and do not have to rely on 
termination checker magic.  I am using sized types when the termination 
checker is not good enough, e.g. see examples at

 
https://github.com/andreasabel/continuous-normalization/blob/master/src/LocallyNamelessValues.agda

for induction and

 
https://github.com/andreasabel/continuous-normalization/blob/master/src/Delay.agda

for coinduction.

Cheers,
Andreas

On 01.12.2013 10:02, Jan Stolarek wrote:
>> Ulf recently changed Agda to reduce the need for workarounds:
>>
>>     Issue 59: Improving termination checking of functions defined using
>>               with
>>     http://code.google.com/p/agda/issues/detail?id=59
>>
>> You may want to try the latest development version.
> I just installed the latest version from repository and indeed there are improvements. Agda no
> longer complains about:
>
> merge : List Nat → List Nat → List Nat
> merge nil       ys             = ys
> merge xs        nil            = xs
> merge (x :: xs) (y :: ys) with order x y
> merge (x :: xs) (y :: ys) | le = x :: merge xs (y :: ys)
> merge (x :: xs) (y :: ys) | ge = y :: merge (x :: xs) ys
>
> but it still complains about this:
>
> mergeO : {b : Nat} → OList b → OList b → OList b
> mergeO onil ys = ys
> mergeO (ocons x blex xs) onil = ocons x blex xs
> mergeO (ocons x blex xs) (ocons y bley ys) with orderD x y
> mergeO (ocons x blex xs) (ocons y bley ys) | le xley =
>    ocons x blex (mergeO xs (ocons y xley ys))
> mergeO (ocons x blex xs) (ocons y bley ys) | ge ylex =
>    ocons y bley (mergeO (ocons x ylex xs) ys)
>
> I presume the reason is that parameter to recursive call is not an exact reconstruction of the
> input parameter (notice how bley is replaced by xley or blex by ylex). Idris is smarter here and
> correctly detects that mergeO is total.
>
> Janek
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>