[Agda] Termination problems with "with" and recursion

[Jesper Cockx]

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. 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131030/b58c9888/attachment.html