[Agda] Termination problems with "with" and recursion

[Andreas Abel]

On 04.12.2013 09:48, Jan Stolarek wrote:
> One more question: when would I use inf as a size?

Whenever the size is unbounded or the system is too weak to express the 
precise size.  Examples:

1. minus : Nat i -> Nat \inf -> Nat i

    Here, the size of the subtracted number does not matter for 
termination and does not affect the output size in a way we can express 
with sized types.

2. times : Nat i -> Nat j -> Nat \inf
    times : Nat i -> Nat \inf -> Nat \inf

    Here, the output is not bounded by any input, so we can only assign 
\inf.  Then, it does not make sense to put a precise bound j on the 
second argument, so we default to \inf.  Finally, the bound i on the 
first argument is only used by the termination checker for times, it 
does not make the type more precise.  If the termination checker does 
not need it, we can default this to \inf as well

    times : Nat \inf -> Nat \inf -> Nat \inf

This actually happens if you do not specify the size to Agda but just write

    times : Nat _ -> Nat _ -> Nat _

Does this answer your question?  If not, please ask further.

Cheers,
Andreas

>> 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
>
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/