Terminación de la inducción estructural

Question

No consigo que el verificador de terminación Agda acepte funciones definidas mediante inducción estructural.

Creé lo siguiente como, creo, el ejemplo más simple que presenta este problema. Se rechaza la siguiente definición de size, aunque siempre recurre a componentes estrictamente más pequeños.

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

¿Existe una solución genérica para este problema? ¿Debo crear un Recursor para mi tipo de datos? Si es así, ¿cómo hago eso? (Supongo que si hay un ejemplo de cómo se podría definir un Recursor para List A, que me daría suficientes pistas?)

Answer 1

Hay un truco que puede hacer aquí: Puede manualmente en línea y se fusionan las definiciones de mapa y suma dentro de un bloque mutuo. Es bastante anti-modular, pero es el método más simple que conozco. Algunos otros idiomas totales (Coq) a veces pueden hacer esto automáticamente.

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

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