Прекращение структурной индукции

Question

Я не могу заставить проверку завершения Агды принимать функции, определенные с использованием структурной индукции.

Я создал следующее как, я думаю, самый простой пример, демонстрирующий эту проблему. Следующее определение size отклоняется, даже если это всегда происходит на строго меньших компонентах.

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

Есть ли общее решение этой проблемы? Нужно ли создавать Recursor для моего типа данных? Если да, как мне это сделать? (Я думаю, если есть пример того, как можно определить Recursor за List Aчто даст мне достаточно намеков?)

Answer 1

Здесь можно сделать трюк: вы можете вручную встроить и объединить определения карты и суммировать во взаимном блоке. Это довольно антимодульно, но это самый простой метод, который я знаю. Некоторые другие общие языки (Coq) могут иногда делать это автоматически.

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

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