<div dir="ltr"><div>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:<br>
<br><div style="margin-left:40px">open import Data.Nat using (ℕ; zero; suc; _+_)<br>open import Data.List using (List; []; _∷_; length)<br><br>data Order : Set where<br> le ge : Order<br><br>order : ℕ → ℕ → Order<br>order zero y = le<br>
order (suc x) zero = ge<br>order (suc x) (suc y) = order x y<br><br>merge-aux : ℕ → List ℕ → List ℕ → List ℕ<br>merge-aux _ [] ys = ys<br>merge-aux _ xs [] = xs<br>merge-aux zero _ _ = []<br>
merge-aux (suc n) (x ∷ xs) (y ∷ ys) with order x y<br>merge-aux (suc n) (x ∷ xs) (y ∷ ys) | le = merge-aux n xs (y ∷ ys)<br>merge-aux (suc n) (x ∷ xs) (y ∷ ys) | ge = merge-aux n (x ∷ xs) ys<br><br>merge : List ℕ → List ℕ → List ℕ<br>
merge xs ys = merge-aux (length xs + length ys) xs ys<br><br></div>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'? <br>
</div><div><div style="margin-left:40px"><br></div>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? <br>
<br></div>Jesper<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Oct 30, 2013 at 12:29 PM, Jan Stolarek <span dir="ltr"><<a href="mailto:jan.stolarek@p.lodz.pl" target="_blank">jan.stolarek@p.lodz.pl</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thanks for reply Jesper. Perhaps I ommitied something important when trying to simplify my<br>
example. Full code is below:<br>
<br>
========== START CODE ==========<br>
<br>
module MergeSort where<br>
<br>
record Sg (S : Set)(T : S → Set) : Set where<br>
constructor _,_<br>
field<br>
fst : S<br>
snd : T fst<br>
open Sg public<br>
_×_ : Set → Set → Set<br>
S × T = Sg S λ _ → T<br>
infixr 4 _,_ _×_<br>
<br>
data Nat : Set where<br>
zero : Nat<br>
suc : Nat → Nat<br>
<br>
data Order : Set where<br>
le ge : Order<br>
<br>
data List (X : Set) : Set where<br>
nil : List X<br>
_::_ : X → List X → List X<br>
<br>
order : Nat → Nat → Order<br>
order zero y = le<br>
order (suc x) zero = ge<br>
order (suc x) (suc y) = order x y<br>
<br>
merge : List Nat → List Nat → List Nat<br>
merge nil ys = ys<br>
merge xs nil = xs<br>
merge (x :: xs) (y :: ys) with order x y<br>
merge (x :: xs) (y :: ys) | le = x :: merge xs (y :: ys)<br>
merge (x :: xs) (y :: ys) | ge = y :: merge (x :: xs) ys<br>
<br>
deal : {X : Set} → List X → List X × List X<br>
deal nil = nil , nil<br>
deal (x :: nil) = x :: nil , nil<br>
deal (y :: (z :: xs)) with deal xs<br>
deal (y :: (z :: xs)) | ys , zs = y :: ys , z :: zs<br>
<br>
sort : List Nat → List Nat<br>
sort xs with deal xs<br>
sort xs | ys , nil = ys<br>
sort xs | ys , zs = merge (sort ys) (sort zs)<br>
<br>
========== END CODE ==========<br>
<br>
I have problems with merge and sort.<br>
<br>
Janek<br>
</blockquote></div><br></div>