[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

Andreas,

thank you for detailed explanation.

Janek

Dnia środa, 30 października 2013, Andreas Abel napisał:
> 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.
>
>    http://gc.codehum.com/p/agda/issues/detail?can=2&q=709
>
> >>> >>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.
>
> Cheers,
> Andreas