終止結構感應

我無法讓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嗎？如果是的話，我該怎麼做？（我猜如果有一個例子說明如何爲List A定義一個Recursor，那會給我足夠的提示嗎？）

來源

2012-02-05 Cactus

有一個技巧你可以在這裏做：你可以手動內聯並融合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

來源

2012-02-09 02:45:20 wjedynak

是的，這是我在使用'map'時也是這樣做的。真的很不幸，終止檢查器無法進入'map'的定義，並看到一切都沒有問題。 – danr 2012-02-09 21:20:32

終止結構感應

回答

相關問題