Terminazione dell'induzione strutturale

Question

Non riesco a ottenere che il controllo di terminazione di Agda accetti le funzioni definite mediante induzione strutturale.

Ho creato il seguente esempio, a mio avviso, più semplice che mostra questo problema. La seguente definizione di size viene rifiutata, anche se ricorre sempre su componenti strettamente più piccoli.

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

Esiste una soluzione generica a questo problema? Devo creare un Recursor per il mio tipo di dati? Se sì, come faccio? (Immagino che se ci fosse un esempio di come definire uno Recursor per List A, mi darebbe abbastanza suggerimenti?)

Answer 1

C'è un trucco che puoi fare qui: puoi allineare e fondere manualmente le definizioni di mappa e somma all'interno di un blocco reciproco. È piuttosto anti-modulare, ma è il metodo più semplice di cui io sia a conoscenza. Alcune altre lingue totali (Coq) a volte possono farlo automaticamente.

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

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