[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

> The problem with the definition of merge is that the termination checker
> looks for one argument to the function that becomes structurally smaller in
> all recursive calls. 
OK, that makes sense. Well, maybe termination checker could be smarter, but now at least I can 
reasonably predict when it is going to complain.

Thanks!

Janek

> There is no such argument for this definition, because 
> the first recursive call only reduces the size of the first argument, while
> the second one only reduces the size of the second one. I think the
> 'proper' way to solve this is to define your own termination order and use
> Induction.WellFounded from the standard library, but I find this quite hard
> to explain. Another way that works for this example is to define an
> auxiliary merge function that takes a maximum number of recursion steps as
> an extra argument. The real merge function can then call this one with a
> sufficiently large number of steps (e.g. the total length of the two
> lists). In agda:
>
> open import Data.Nat using (ℕ; zero; suc; _+_)
> open import Data.List using (List; []; _∷_; length)
>
> data Order : Set where
>   le ge : Order
>
> order : ℕ → ℕ → Order
> order zero y = le
> order (suc x) zero = ge
> order (suc x) (suc y) = order x y
>
> merge-aux : ℕ → List ℕ → List ℕ → List ℕ
> merge-aux _       []       ys = ys
> merge-aux _       xs       [] = xs
> merge-aux zero    _        _  = []
> merge-aux (suc n) (x ∷ xs) (y ∷ ys) with order x y
> merge-aux (suc n) (x ∷ xs) (y ∷ ys) | le = merge-aux n xs (y ∷ ys)
> merge-aux (suc n) (x ∷ xs) (y ∷ ys) | ge = merge-aux n (x ∷ xs) ys
>
> merge : List ℕ → List ℕ → List ℕ
> merge xs ys = merge-aux (length xs + length ys) xs ys
>
> I don't know why the termination checker doesn't complain for the version
> that uses if_then_else_ instead of with. Maybe there is some additional
> smartness in the termination checker that doesn't work well for 'with'?
>
> To the developers: In my opinion, the termination checker is one biggest
> hurdles for people coming to Agda from other languages. How hard would it
> be for the termination checker to detect termination of Janek's merge
> function?
>
> Jesper
>
> On Wed, Oct 30, 2013 at 12:29 PM, Jan Stolarek <jan.stolarek at p.lodz.pl>wrote:
> > Thanks for reply Jesper. Perhaps I ommitied something important when
> > trying to simplify my
> > example. Full code is below:
> >
> > ========== START CODE ==========
> >
> > module MergeSort where
> >
> > record Sg (S : Set)(T : S → Set) : Set where
> >   constructor _,_
> >   field
> >     fst : S
> >     snd : T fst
> > open Sg public
> > _×_ : Set → Set → Set
> > S × T = Sg S λ _ → T
> > infixr 4 _,_ _×_
> >
> > data Nat : Set where
> >   zero : Nat
> >   suc  : Nat → Nat
> >
> > data Order : Set where
> >   le ge : Order
> >
> > data List (X : Set) : Set where
> >   nil  : List X
> >   _::_ : X → List X → List X
> >
> > order : Nat → Nat → Order
> > order zero    y       = le
> > order (suc x) zero    = ge
> > order (suc x) (suc y) = order x y
> >
> > 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
> >
> > deal : {X : Set} → List X → List X × List X
> > deal nil        = nil , nil
> > deal (x :: nil) = x :: nil , nil
> > deal (y :: (z :: xs)) with deal xs
> > deal (y :: (z :: xs)) | ys , zs = y :: ys , z :: zs
> >
> > sort : List Nat → List Nat
> > sort xs with deal xs
> > sort xs | ys , nil = ys
> > sort xs | ys , zs  = merge (sort ys) (sort zs)
> >
> > ========== END CODE ==========
> >
> > I have problems with merge and sort.
> >
> > Janek