[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

Ok, I think I need some help with Sized types. I have a datatype representing a Heap:

data Heap : {i : Size} → Set where
  empty : {i : Size} → Heap {↑ i}
  node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑ i}

And I need to use sized types in merge function:

merge : {i : Size} → Heap → Heap → Heap
merge h1 h2 with h1 | h2
merge h1 h2 | empty | _ = h2
merge h1 h2 | _ | empty = h1
merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2 r2)  with p1 < p2
merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2 r2)  | true  = makeT p1 l1 (merge r1 h2)
merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2 r2)  | false = makeT p2 l2 (merge h1 r2)

Can I please have a hint how to do that? I tried adding annotation according to this presentation:

www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf‎

but with no success :-/ I keep getting errors like i != inf.

Janek


Dnia niedziela, 1 grudnia 2013, Andreas Abel napisał:
> 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/Loc
>allyNamelessValues.agda
>
> for induction and
>
>
> https://github.com/andreasabel/continuous-normalization/blob/master/src/Del
>ay.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