Termination of structural induction

agda, induction, recursion, termination

Solution

There is a trick you can do here: you can manually inline and fuse the definitions of map and sum inside a mutual block. It's pretty anti-modular, but it's the simplest method I'm aware of. Some other total languages (Coq) can sometimes do this automatically.

mutual
  size : Tree → ℕ
  size leaf = 1
  size (branch ts) = suc (sizeBranch ts)

  sizeBranch : List Tree → ℕ
  sizeBranch [] = 0
  sizeBranch (x :: xs) = size x + sizeBranch xs

Problem

I can't get Agda's termination checker to accept functions defined using structural induction. I created the following as the, I think, simplest example exhibiting this problem. The following definition of `size` is rejected, even though it always recurses on strictly smaller components. ``` module Tree where open import Data.Nat open import Data.List data Tree : Set where leaf : Tree branch : (ts : List Tree) → Tree size : Tree → ℕ size leaf = 1 size (branch ts) = suc (sum (map size ts)) ``` Is there a generic solution to this problem? Do I need to create a `Recursor` for my data type? If yes, how do I do that? (I guess if there's an example of how one would define a `Recursor` for `List A`, that would give me enough hints?)

Original source