[Agda] Type and termination checking around with clauses

[Anton Setzer]

Ulf Norell wrote:
>
> On Wed, Apr 30, 2008 at 3:24 AM, Peter Berry <pwberry at gmail.com
> <mailto:pwberry at gmail.com>> wrote:
>
>
>     merge : List ℕ -> List ℕ -> List ℕ
>     merge xs        [] = xs
>     merge []        ys = ys
>     merge (x :: xs) (y :: ys) with x <= y -- should be l@(x :: xs) but
>     for the bug
>     ... | true  = x :: merge xs (y :: ys)
>     ... | false = y :: merge (x :: xs) ys
>
>     These last two lines trip the termination checker. Clearly the
>     arguments are (as a whole) strictly smaller, but a new list is made,
>     which presumably makes the termination checker think they're getting
>     bigger. With at-patterns in with clauses working properly (i.e. bug 56
>     fixed, see http://code.google.com/p/agda/issues/detail?id=56) and
>     using l instead of x :: xs, would it pass? Or are there plans to make
>     the checker spot this kind of 'reconstructing patterns'? Is that even
>     feasible?
>
>
> Yeah, this is a known issue. It wouldn't work even when the as-pattern
> bug is fixed. We have some vague ideas on how to solve the problem but
> nothing concrete yet.
>
Definition of this form can in general be dangerous
Consider

f : Nat -> Nat -> Bool -> Nat
f (S x) y        tt = f x              (S (S y)) ff
f x       (S y)  ff = f (S (S x))  y             tt
f _      _        _ = 0

Here you have in the first case a descent by x
in the second case a descent by y.
But f doesn't terminate as
f 1 0 tt
= f 0 2 ff
= f 2 1 tt
= f 1 3 ff
= ...

Simultaneous decrease of arguments works only
if when in one case  one argument reduces
and in another case the other argument reduces,
then in both cases both cases the arguments reduce
or stay the same.

Here is by the way a proper solution for merge sort:

> _<Bool_ : Nat  -> Nat  -> Bool
> _ <Bool Z     = ff
> Z <Bool S _   = tt
> S n <Bool S m = n <Bool m
>
>
> if_then_else_ : {A : Set} -> Bool -> A -> A -> A
> if tt then s else _ = s
> if ff then _ else t = t
>
>
> data List (A : Set) : Set where
>   []   : List A
>   _::_ : A -> List A -> List A
>
> mutual
>   merge : List Nat  -> List Nat -> List Nat
>   merge []        ys = ys
>   merge (x :: xs) ys = mergeauxl x xs ys
>
>
>   mergeauxl : Nat -> List Nat -> List Nat -> List Nat
>   mergeauxl x xs []        = x :: xs
>   mergeauxl x xs (y :: ys) = mergeauxlr x xs y ys
>
>   mergeauxr : List Nat -> Nat -> List Nat -> List Nat
>   mergeauxr []        y ys = y :: ys
>   mergeauxr (x :: xs) y ys = mergeauxlr x xs y ys
>
>   mergeauxlr : Nat -> List Nat -> Nat -> List Nat -> List Nat
>   mergeauxlr  x xs y ys = if x <Bool y
>                             then  x :: mergeauxr xs y ys
>                             else (y :: mergeauxl x xs ys)

So mergeauxl x xs ys   is essentially merge (x :: xs) ys
      mergeauxr xs y ys  is essentially merge  xs         (y :: ys)
      mergeauxlr x xs y ys is essentially merge (x :: xs) (y :: ys)

The advantage of this solution is that it never packs elements
back into merge and then unpacks them again.


Anton





> 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.
>
>     Possibly related: suppose I have a 'with' clause, say
>
>     contrived (dprod l p) with l
>     ... | [] = ?0
>     ... | x :: xs = ?1
>
>     where p : P l for some function P : List ℕ -> Set, say a property
>     which p is a proof of, and somewhere in ?1 I need something of type P
>     (x :: xs) (like a proof of the same property). Clearly x :: xs = l so
>     p will do, but somehow the type checker misses this - it won't unify P
>     l = P (x :: xs). (If you want a concrete example I can provide one.)
>
>
> If p : P l then in ?1 you should have p : P (x :: xs). If you don't
> there's a bug. A concrete example might be helpful.
>
> / Ulf
> ------------------------------------------------------------------------
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>   


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
 
                    
  

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