gpt4 book ai didi

recursion - 结构感应的终止

转载 作者:行者123 更新时间:2023-12-04 14:49:30 25 4
gpt4 key购买 nike

我无法让 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 的示例,那会给我足够的提示吗?)

最佳答案

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

关于recursion - 结构感应的终止,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/9146928/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com