[Agda] Type and termination checking around with clauses

[Ulf Norell]

On Wed, Apr 30, 2008 at 8:11 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk>
wrote:

>  Peter Berry wrote:
>
> 2008/4/30 Ulf Norell <ulfn at cs.chalmers.se> <ulfn at cs.chalmers.se>:
>
>
>  A possible work around might be to include the recursive calls in the with
> clause (untested):
>
>  merge (x :: xs) (y :: ys) with x <= y | merge xs (y :: ys) | merge (x ::
> xs) ys
>  ... | true   | rec | _ = x :: rec
>  ... | false | _ | rec = y :: rec
>
> This isn't very nice, but at least it should make the termination checker
> happy. Of course, in this particular case an if_then_else_ would also work.
>
>
>  Aha, I didn't know you could do that. And yes, doh, if_then_else_
> makes perfect sense.
>
>
>
>
> It sounds to me odd that this solution is accepted, but the direct
> solution
> is not accepted.
> It shouldn't make any difference whether I make a recursive call
> to merge using a with clause or whether I use it directly.
>

Bear in mind that with clauses are translated to calls to an auxiliary
function. It's not that odd that it makes a difference to the termination
checker how you arrange your mutually recursive functions. The difference
for the termination checker is the following:

-- The original example (which doesn't pass the termination checker)
mutual
  aux x xs y ys = ... f xs (y :: ys) .. f (x :: xs) ys ..
  f (x :: xs) (y :: ys) = aux x xs y ys

-- The work around (does pass the termination checker)
aux rec1 rec2 = .. rec1 .. rec2 ..
f (x :: xs) (y :: ys) = aux (f xs (y :: ys)) (f (x :: xs) ys)

In the first example the arguments in the call to f from aux are actually
getting bigger, the fact that they're only getting a little bigger isn't
recognized by the termination checker. In the second example, there is only
one recursive function (f) and it's quite clear that both arguments either
stay the same or get smaller in the recursive calls.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080430/9950db06/attachment.html