[Agda] Termination problems with "with" and recursion

Andreas Abel abela at chalmers.se
Wed Oct 30 23:51:34 CET 2013

Hi Jan, Jesper, and Dominique,

Unfortunately, the termination checker and 'with' do not harmonize.  The 
problem, as already been outlined by Dominique, is that the termination 
checker works on the desugared code, where 'with' has been replaced by 
an auxiliary function.  So, even if in the source code the recursive 
call arguments are looking smaller, the termination checker might not 
see it due to the generated auxiliary function.

On 30.10.2013 15:04, Dominique Devriese wrote:
> I believe that a with-pattern-match is internally translated to a call
> of a local helper function with the scrutinee as an extra argument and
> an appropriate type to use the information learned from the pattern
> match. Strangely, if I perform this translation manually here:
>    merge′ : List Nat → List Nat → List Nat
>    merge′ nil       ys             = ys
>    merge′ xs        nil            = xs
>    merge′ (x :: xs) (y :: ys)       = go x xs y ys (order x y)
>      where go : Nat → List Nat → Nat → List Nat → Order → List Nat
>            go x xs y ys le = x :: merge xs (y :: ys)
>            go x xs y ys gt = y :: merge (x :: xs) ys
> Then the termination checker does succeed.  It seems weird (at least
> to me) that it doesn't work on the same code without the
> with-desugaring.

Yes that is weird.  It does not succeed when I try your code.  Note that 
the apparent success might be to the fact that you actually have no 
recursive calls, since your function merge' only calls merge (which is, 
to your bad luck, in scope here).

So, let me emphasize that the termination checker refutes this call pattern.

   merge (x :: xs) (y :: ys)
     --> go x xs y ys ...
     --> merge xs (y :: ys)

The termination checker sees that in merge-->go, the arguments all 
become smaller, but in go--->merge, one argument becomes bigger.  Since 
it has simplistic, it cannot remember where y and ys came from and that 
taken together, they are actually the same as we started out.  Thus, it 
fails to see that, in the composed call

   merge (x :: xs) (y :: ys) -->---> merge xs (y :: ys),

one argument actually got smaller where the other did not become bigger. 
  If it did not fail to see this, it would accept merge.

There are several ways out of this dilemma:

1. (preferred) Avoid 'with' when possible.  In your case, there is no 
dependency in the types on (order x y), thus, use an if-then-else-like 
function instead.

2. Use the trick to put the recursive calls into the 'with' as well.

   merge (x :: xs) (y :: ys) with order x y | merge xs (y :: ys) | merge 
(x :: xs) ys
   ... | le | call1 | call2 = call1
   ... | ge | call1 | call2 = call2

   This basically corresponds to the use of an if-like function, only 
that it is "defined on the fly" here.

3. Define your auxiliary function yourself and in a way that lets the 
termination checker see that your call patterns are ok.

4. Use sized types (experimental) and --termination-depth=2.  This is 
maybe not ripe for production-use.


>>> >>The problem with the definition of merge is that the termination checker
>>> >>looks for one argument to the function that becomes structurally smaller in
>>> >>all recursive calls.

This is not correct.  Lexicographic orders are also accepted, for instance.


More information about the Agda mailing list