我无法让 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
for List A
,这会给我足够的提示吗?)
您可以在这里使用一个技巧:您可以手动内联并融合共同块内的 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
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)