[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

Thank you very much Andreas.

> You are saying both argument have a common upper bound that is decreased in each
> recursive call.
Oh, silly me.

One more question: when would I use inf as a size?

> This should work.  However, it does not, which seems to be a bug, and I
> filed an issue.
I think I'm gonna pretend that it works :-) and hope that it gets fixed sometime soon.

Janek

Dnia wtorek, 3 grudnia 2013, Andreas Abel napisał:
> [CC to Ulf]
>
> There are two issues here.
>
> First, your size assignment for merge does not work.  You are saying
> both argument have a common upper bound that is decreased in each
> recursive call.  This is not the case, since only one of the two heaps
> gets smaller each time.  So you need to have two sizes:
>
> module ShouldSucceed where
>
>    merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap {∞} p
>    merge empty h2 = h2
>    merge h1 empty = h1
>    merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2
> r-rank p2≥p l2 r2) with order p1 p2
>    merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2
> r-rank p2≥p l2 r2) | le p1≤p2 = makeT p1 p1≥p l1 (merge {i} {↑ j} r1
> (node p2 r-rank p1≤p2 l2 r2))
>    merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2
> r-rank p2≥p l2 r2) | ge p1≥p2 = makeT p2 p2≥p l2 (merge {↑ i} {j} (node
> p1 l-rank p1≥p2 l1 r1) r2)
>
> This should work.  However, it does not, which seems to be a bug, and I
> filed an issue.  (See agda issues 59).
>
> If you expand the "with" out manually (the new command C-c C-h comes in
> very handy here), you get something that is accepted by the termination
> checker:
>
> module Succeeds where
>   mutual
>    merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap {∞} p
>    merge empty h2 = h2
>    merge h1 empty = h1
>    merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2
> r-rank p2≥p l2 r2) =
>      merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (order p1 p2)
>
>    merge' : ∀ {i} {j} {p} →
>             ∀ p1 → Nat → p1 ≥ p → Heap {i} p1 → Heap {i} p1 →
>             ∀ p2 → Nat → p2 ≥ p → Heap {j} p2 → Heap {j} p2 → Order p1
> p2 → Heap {∞} p
>    merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (le p1≤p2) =
> makeT p1 p1≥p l1 (merge {i} {↑ j} r1 (node p2 r-rank p1≤p2 l2 r2))
>    merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (ge p1≥p2) =
> makeT p2 p2≥p l2 (merge {↑ i} {j} (node p1 l-rank p1≥p2 l1 r1) r2)
>
> Cheers,
> Andreas
>
> On 02.12.2013 14:09, Jan Stolarek wrote:
> > Ok, I think I need some more assistance :-)
> >
> > Now let's say I have this definition:
> >
> > data Heap : {i : Size} → Priority → Set where
> >    empty : {i : Size} {n : Priority} → Heap {↑ i} n
> >    node  : {i : Size} {n : Priority} → (p : Priority) → Rank → p ≥ n →
> >            Heap {i} p → Heap {i} p → Heap {↑ i} n
> >
> > ≥ is evidence that p >= n. If I now extend merge with evidence like this:
> >
> > merge : {i : Size} {p : Nat} → Heap {i} p → Heap {i} p → Heap p
> > merge empty h2 = h2
> > merge h1 empty = h1
> > merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2
> > r2) with order p1 p2 merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node
> > {i} p2 r-rank p2≥p l2 r2) | le p1≤p2 = makeT p1 p1≥p l1 (merge r1 (node
> > p2 r-rank p1≤p2 l2 r2))
> > merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2
> > r2) | ge p1≥p2 = makeT p2 p2≥p l2 (merge r2 (node p1 l-rank p1≥p2 l1 r1))
> >
> > The termination checker complains on the second call to merge, but does
> > not complain on the first one. I am puzzled. Andreas, can you explain why
> > the first case works and the second doesn't? They seem to be symmetric.
> > I'm attaching source file with definitions that I'm using.
> >
> > Janek
> >
> > Dnia poniedziałek, 2 grudnia 2013, Andreas Abel napisał:
> >> Here you go:
> >> Note that unconstraint sizes default to \inf, so you need to give sizes
> >> in type signatures where sizes are important, e.g. in merge.
> >>
> >> {-# OPTIONS --sized-types #-}
> >>
> >> open import Size
> >> open import Data.Bool
> >>
> >> module _ (Rank Priority : Set) (_<_ : Priority → Priority → Bool) where
> >>
> >> data Heap : {i : Size} → Set where
> >>     empty : {i : Size} → Heap {↑ i}
> >>     node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑
> >> i}
> >>
> >> module _ (makeT : Priority → Heap → Heap → Heap) where
> >>
> >>     merge : {i : Size} → Heap {i} → Heap {i} → Heap
> >>     merge empty h2 = h2
> >>     merge h1 empty = h1
> >>     merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  with p1 < p2
> >>     merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  | true  =
> >>       makeT p1 l1 (merge r1 (node p2 w2 l2 r2))
> >>     merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  | false =
> >>       makeT p2 l2 (merge (node p1 w1 l1 r1) r2)
> >>
> >> Depending on what makeT is, you might be able to give a more precise
> >> type to merge.
> >>
> >> On 02.12.2013 12:38, Jan Stolarek wrote:
> >>> 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