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

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