Termination of structural induction

Question

I cannot get the Agda terminator check to accept functions defined by structural induction.

I created the following, in my opinion, the simplest example demonstrating this problem. The following definition of size rejected, although it is always recursive 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 general solution to this problem? Do I need to create a Recursor for my data type? If so, how do I do this? (I think if there was an example of how to define Recursor for List A , would this give me enough hints?)

Answer 1

Here you can do the trick: you can manually embed and plan the definition of the card and amount inside the reciprocal block. This is pretty anti-modular, but it's the easiest way I know of. Some other complete 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