[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

OK, I came up with a solution that is simple and relatively elegant:

fun : List A -> List A -> List A
fun xss yss with xss | yss
fun xss yss | [] | _ = yss
fun xss yss | x :: xs | [] = xss
fun xss yss | x :: xs | y :: ys with order x y
fun xss yss | x :: xs | y :: ys | le = x :: merge xs yss
fun xss yss | x :: xs | y :: ys | ge = y :: merge xss ys

Question about problems with sized types remains.

Janek


Dnia poniedziałek, 18 listopada 2013, Jan Stolarek napisał:
> Hi Andreas,
>
> I am now writing a merge function for trees and I've hit the same problem
> again.
>
> > 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.
>
> This time I am using a dependently typed order:
>
> data _≥_ : Nat → Nat → Set where
>   ge0 : {y : Nat} → y ≥ zero
>   geS : {x : Nat} {y : Nat} → x ≥ y → suc x ≥ suc y
>
> data Order : Nat → Nat → Set where
>   ge : {x : Nat} {y : Nat} → x ≥ y → Order x y
>   le : {x : Nat} {y : Nat} → y ≥ x → Order x y
>
> order : (a : Nat) → (b : Nat) → Order a b
> order ...
>
> So I can't use this solution.
>
> > 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
>
> Termination checker complains about that as well (i.e. it highlights calls
> to merge in the "with" pattern).
>
> > 3. Define your auxiliary function yourself and in a way that lets the
> > termination checker see that your call patterns are ok.
>
> Could you point me to an example of how to do that? I'm looking at my code
> but I can't come up with a solution that would work (other than giving an
> explicit parameter that would limit number of recursive calls, but that
> feels wrong).
>
> > 4. Use sized types (experimental) and --termination-depth=2.  This is
> > maybe not ripe for production-use.
>
> I'm having problems with that. I annotated my data type with {i : Size}
> index. Now I have merge function for trees (I'm eliding some details which
> I think are irrelevant - the code might be slightly inconsistent here):
>
> merge : {i : Size} {A : Set} {l r : Nat} → Tree A {i} l → Tree A {i} r →
> Tree A {↑ i} (l + r) merge .{↑ i} {A} {suc .(l1-rank + r1-rank)} {suc
> .(l2-rank + r2-rank)} (node {i} {l1-rank} {r1-rank} l1 r1)
>           (node .{i} {l2-rank} {r2-rank} l2 r2)
>           = node l1 (merge r1 (node {i} l2 r2)))
>
> and I get an error in the last line for the innermost node constructor:
>
>   Size !=< Set of type Set when checking that the expression i has type Set
>
> Why does it expect {i} to be Set? The definition of my data type is:
>
> data Tree (A : Set) : {i : Size} → Nat → Set where
>   empty : {i : Size} → Tree A {↑ i} zero
>   node  : {i : Size} → {l r : Nat} → Tree A {i} l → Tree A {i} r → Tree A
> {↑ i} (suc (l + r))
>
> Janek
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda