终止结构感应 [英] Termination of structural induction

问题描述

我无法让Agda的终止检查器接受使用结构归纳定义的功能.

I can't get Agda's termination checker to accept functions defined using structural induction.

我创建了以下示例，它是展示此问题的最简单示例. 尽管size总是在严格较小的组件上重复出现，但以下定义却被拒绝.

I created the following as the, I think, simplest example exhibiting this problem. The following definition of size is rejected, even though it always recurses on strictly smaller components.

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吗?如果是，我该怎么做? (我想如果有一个示例可以说明如何为List A定义Recursor，那会给我足够的提示吗?)

Is there a generic solution to this problem? Do I need to create a Recursor for my data type? If yes, how do I do that? (I guess if there's an example of how one would define a Recursor for List A, that would give me enough hints?)

推荐答案

您可以在此处完成一个技巧:您可以手动将内联映射和求和的定义内联并融合在一起.这是非常反模块化的，但这是我所知道的最简单的方法.其他一些总语言(Coq)有时可以自动执行此操作.

There is a trick you can do here: you can manually inline and fuse the definitions of map and sum inside a mutual block. It's pretty anti-modular, but it's the simplest method I'm aware of. Some other total languages (Coq) can sometimes do this automatically.

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

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

这篇关于终止结构感应的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！