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


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

Я создал следующее, как я считаю, самый простой пример, демонстрирующий эту проблему. Следующее определение 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, что даст мне достаточно намеков?)


6


источник


Ответы:


Здесь вы можете сделать трюк: вы можете вручную встроить и спланировать определения карты и суммы внутри взаимного блока. Это довольно антимодульное, но это самый простой способ, о котором я знаю. Некоторые другие общие языки (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

7