Termination check on list merge

Question

Agda 2.3.2.1 can't see that the following function terminates:

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _     = y ∷ merge (x ∷ xs) ys 
merge xs ys = xs ++ ys

Agda wiki says that it's OK for the termination checker if the arguments on recursive calls decrease lexicographically. Based on that it seems that this function should also pass. So what am I missing here? Also, is it maybe OK in previous versions of Agda? I've seen similar code on the Internet and no one mentioned termination issues there.

Answer 1

I cannot give you the reason why exactly this happens, but I can show you how to cure the symptoms. Before I start: This is a known problem with the termination checker. If you are well-versed in Haskell, you could take a look at the source.

---

One possible solution is to split the function into two: first one for the case where the first argument gets smaller and second for the second one:

mutual
  merge : List ℕ → List ℕ → List ℕ
  merge (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ merge xs (y ∷ ys)
  ... | no  _ = y ∷ merge′ x xs ys
  merge xs ys = xs ++ ys

  merge′ : ℕ → List ℕ → List ℕ → List ℕ
  merge′ x xs (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ merge xs (y ∷ ys)
  ... | no  _ = y ∷ merge′ x xs ys
  merge′ x xs [] = x ∷ xs

So, the first function chops down xs and once we have to chop down ys, we switch to the second function and vice versa.

---

Another (perhaps surprising) option, which is also mentioned in the issue report, is to introduce the result of recursion via with:

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y | merge xs (y ∷ ys) | merge (x ∷ xs) ys
... | yes _ | r | _ = x ∷ r
... | no  _ | _ | r = y ∷ r
merge xs ys = xs ++ ys

---

And lastly, we can perform the recursion on Vectors and then convert back to List:

open import Data.Vec as V
  using (Vec; []; _∷_)

merge : List ℕ → List ℕ → List ℕ
merge xs ys = V.toList (go (V.fromList xs) (V.fromList ys))
  where
  go : ∀ {n m} → Vec ℕ n → Vec ℕ m → Vec ℕ (n + m)
  go {suc n} {suc m} (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _                 = x ∷ go xs (y ∷ ys)
  ... | no  _ rewrite lem n m = y ∷ go (x ∷ xs) ys
  go xs ys = xs V.++ ys

However, here we need a simple lemma:

open import Relation.Binary.PropositionalEquality

lem : ∀ n m → n + suc m ≡ suc (n + m)
lem zero    m                 = refl
lem (suc n) m rewrite lem n m = refl

We could also have go return List directly and avoid the lemma altogether:

merge : List ℕ → List ℕ → List ℕ
merge xs ys = go (V.fromList xs) (V.fromList ys)
  where
  go : ∀ {n m} → Vec ℕ n → Vec ℕ m → List ℕ
  go (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ go xs (y ∷ ys)
  ... | no  _ = y ∷ go (x ∷ xs) ys
  go xs ys = V.toList xs ++ V.toList ys

---

The first trick (i.e. split the function into few mutually recursive ones) is actually quite good to remember. Since the termination checker doesn't look inside the definitions of other functions you use, it rejects a great deal of perfectly fine programs, consider:

data Rose {a} (A : Set a) : Set a where
  []   :                     Rose A
  node : A → List (Rose A) → Rose A

And now, we'd like to implement mapRose:

mapRose : ∀ {a b} {A : Set a} {B : Set b} →
          (A → B) → Rose A → Rose B
mapRose f []          = []
mapRose f (node t ts) = node (f t) (map (mapRose f) ts)

The termination checker, however, doesn't look inside the map to see if it doesn't do anything funky with the elements and just rejects this definition. We must inline the definition of map and write a pair of mutually recursive functions:

mutual
  mapRose : ∀ {a b} {A : Set a} {B : Set b} →
            (A → B) → Rose A → Rose B
  mapRose f []          = []
  mapRose f (node t ts) = node (f t) (mapRose′ f ts)

  mapRose′ : ∀ {a b} {A : Set a} {B : Set b} →
             (A → B) → List (Rose A) → List (Rose B)
  mapRose′ f []       = []
  mapRose′ f (t ∷ ts) = mapRose f t ∷ mapRose′ f ts

Usually, you can hide most of the mess in a where declaration:

mapRose : ∀ {a b} {A : Set a} {B : Set b} →
          (A → B) → Rose A → Rose B
mapRose {A = A} {B = B} f = go
  where
  go      :       Rose A  →       Rose B
  go-list : List (Rose A) → List (Rose B)

  go []          = []
  go (node t ts) = node (f t) (go-list ts)

  go-list []       = []
  go-list (t ∷ ts) = go t ∷ go-list ts

Note: Declaring signatures of both functions before they are defined can be used instead of mutual in newer versions of Agda.

---

Update: The development version of Agda got an update to the termination checker, I'll let the commit message and release notes speak for themselves:

• A revision of call graph completion that can deal with arbitrary termination depth. This algorithm has been sitting around in MiniAgda for some time, waiting for its great day. It is now here! Option --termination-depth can now be retired.

And from the release notes:

• Termination checking of functions defined by 'with' has been improved.

  Cases which previously required --termination-depth (now obsolete!) to pass the termination checker (due to use of 'with') no longer
  need the flag. For example

  merge : List A → List A → List A
  merge [] ys = ys
  merge xs [] = xs
  merge (x ∷ xs) (y ∷ ys) with x ≤ y
  merge (x ∷ xs) (y ∷ ys)    | false = y ∷ merge (x ∷ xs) ys
  merge (x ∷ xs) (y ∷ ys)    | true  = x ∷ merge xs (y ∷ ys)
  

  This failed to termination check previously, since the 'with' expands to an auxiliary function merge-aux:

  merge-aux x y xs ys false = y ∷ merge (x ∷ xs) ys
  merge-aux x y xs ys true  = x ∷ merge xs (y ∷ ys)
  

  This function makes a call to merge in which the size of one of the arguments is increasing. To make this pass the termination checker now inlines the definition of merge-aux before checking, thus effectively termination checking the original source program.

  As a result of this transformation doing 'with' on a variable no longer preserves termination. For instance, this does not termination check:

  bad : Nat → Nat
  bad n with n
  ... | zero  = zero
  ... | suc m = bad m
  

And indeed, your original function now passes the termination check!