recursion - 结构感应的终止

Question

我无法让 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为我的数据类型创建一个吗？如果是，我该怎么做？（我想如果有一个如何定义Recursorfor的例子List A，那会给我足够的提示吗？）

Answer 1

你可以在这里做一个技巧：你可以手动内联和融合 map 和 sum 的定义在一个相互块中。它非常反模块化，但它是我所知道的最简单的方法。其他一些总语言（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