7

構造帰納法を使用して定義された関数を 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それで十分なヒントが得られると思いますか？）

4

1 に答える 1

8

ここでできるトリックがあります。相互ブロック内で 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-09T02:45:20.827 に答える