Zakończenie indukcji strukturalnej

Question

Nie mogę uzyskać funkcji sprawdzania zakończenia Agdy, aby zaakceptować funkcje zdefiniowane za pomocą indukcji strukturalnej.

Stworzyłem następujące, jak sądzę, najprostszy przykład wykazujący ten problem. Następująca definicja size została odrzucona, mimo że zawsze powtarza się na ściśle mniejszych składnikach.

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

Czy istnieje ogólne rozwiązanie tego problemu? Czy muszę utworzyć Recursor dla mojego typu danych? Jeśli tak, w jaki sposób mogę to zrobić? (Przypuszczam, że istnieje przykład tego, jak zdefiniować Recursor dla List A, co dałoby mi wystarczającą liczbę wskazówek?)

Answer 1

Istnieje sztuczka, którą możesz zrobić tutaj: możesz ręcznie wstawić i połączyć definicje mapy i sumy wewnątrz wspólnego bloku. Jest dość anty-modułowy, ale jest to najprostsza metoda, jaką znam. Niektóre inne języki łącznie (Coq) czasami mogą to zrobić automatycznie.

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

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