Termination of structural induction

Question

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?)

Lacrimator

Answer 1

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

Newby

Yes this is how I also do it when using map. It's really unfortunate really that the termination checker cannot go into the definition of map and see that everything is alright. – Prestonprestress