7

Agda 2.3.2.1 は、次の関数が終了することを確認できません。

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _     = y ∷ merge (x ∷ xs) ys 
merge xs ys = xs ++ ys

Agda wiki によると、再帰呼び出しの引数が辞書順で減少しても、終了チェッカーは問題ないとのことです。それに基づいて、この関数も通過する必要があるようです。それで、私はここで何が欠けていますか？また、以前のバージョンの Agda でも問題ないのでしょうか? インターネットで同様のコードを見たことがありますが、終了の問題について誰も言及していません。

4

1 に答える 1

7

正確な理由を説明することはできませんが、症状を治す方法を示すことはできます。始める前に: これは終了チェッカーの既知の問題です。Haskell に精通している場合は、ソースを見ることができます。

考えられる解決策の 1 つは、関数を 2 つに分割することです。1 つ目は最初の引数が小さくなる場合に使用し、2 つ目は 2 番目の引数に使用します。

mutual
  merge : List ℕ → List ℕ → List ℕ
  merge (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ merge xs (y ∷ ys)
  ... | no  _ = y ∷ merge′ x xs ys
  merge xs ys = xs ++ ys

  merge′ : ℕ → List ℕ → List ℕ → List ℕ
  merge′ x xs (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ merge xs (y ∷ ys)
  ... | no  _ = y ∷ merge′ x xs ys
  merge′ x xs [] = x ∷ xs

したがって、最初の関数はxs切り捨てられ、切り捨てなければならないys場合は、2 番目の関数に切り替えます。その逆も同様です。

イシュー レポートにも記載されている別の (おそらく驚くべき) オプションは、次の方法で再帰の結果を導入することですwith。

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y | merge xs (y ∷ ys) | merge (x ∷ xs) ys
... | yes _ | r | _ = x ∷ r
... | no  _ | _ | r = y ∷ r
merge xs ys = xs ++ ys

そして最後に、 tors で再帰を実行してVecから、 に戻すことができますList:

open import Data.Vec as V
  using (Vec; []; _∷_)

merge : List ℕ → List ℕ → List ℕ
merge xs ys = V.toList (go (V.fromList xs) (V.fromList ys))
  where
  go : ∀ {n m} → Vec ℕ n → Vec ℕ m → Vec ℕ (n + m)
  go {suc n} {suc m} (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _                 = x ∷ go xs (y ∷ ys)
  ... | no  _ rewrite lem n m = y ∷ go (x ∷ xs) ys
  go xs ys = xs V.++ ys

ただし、ここでは簡単な補題が必要です。

open import Relation.Binary.PropositionalEquality

lem : ∀ n m → n + suc m ≡ suc (n + m)
lem zero    m                 = refl
lem (suc n) m rewrite lem n m = refl

goまた、直接returnListして補題を完全に回避することもできます。

merge : List ℕ → List ℕ → List ℕ
merge xs ys = go (V.fromList xs) (V.fromList ys)
  where
  go : ∀ {n m} → Vec ℕ n → Vec ℕ m → List ℕ
  go (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ go xs (y ∷ ys)
  ... | no  _ = y ∷ go (x ∷ xs) ys
  go xs ys = V.toList xs ++ V.toList ys

最初のトリック (つまり、関数をいくつかの相互に再帰的なものに分割する) は、覚えておくと非常に役立ちます。終了チェッカーは、使用する他の関数の定義の中を調べないため、完全に問題のないプログラムを大量に拒否します。次のことを考慮してください。

data Rose {a} (A : Set a) : Set a where
  []   :                     Rose A
  node : A → List (Rose A) → Rose A

そして今、実装したいと思いますmapRose:

mapRose : ∀ {a b} {A : Set a} {B : Set b} →
          (A → B) → Rose A → Rose B
mapRose f []          = []
mapRose f (node t ts) = node (f t) (map (mapRose f) ts)

ただし、終了チェッカーは の内部mapを調べて、要素に対して何かおかしなことをしていないかどうかを確認せず、この定義を拒否するだけです。定義をインライン化し、map相互に再帰的な関数のペアを作成する必要があります。

mutual
  mapRose : ∀ {a b} {A : Set a} {B : Set b} →
            (A → B) → Rose A → Rose B
  mapRose f []          = []
  mapRose f (node t ts) = node (f t) (mapRose′ f ts)

  mapRose′ : ∀ {a b} {A : Set a} {B : Set b} →
             (A → B) → List (Rose A) → List (Rose B)
  mapRose′ f []       = []
  mapRose′ f (t ∷ ts) = mapRose f t ∷ mapRose′ f ts

通常、混乱のほとんどはwhere宣言で隠すことができます。

mapRose : ∀ {a b} {A : Set a} {B : Set b} →
          (A → B) → Rose A → Rose B
mapRose {A = A} {B = B} f = go
  where
  go      :       Rose A  →       Rose B
  go-list : List (Rose A) → List (Rose B)

  go []          = []
  go (node t ts) = node (f t) (go-list ts)

  go-list []       = []
  go-list (t ∷ ts) = go t ∷ go-list ts

mutual注:新しいバージョンの Agda の代わりに、定義する前に両方の関数のシグネチャを宣言することを使用できます。

更新: Agda の開発バージョンは、終了チェッカーが更新されました。コミット メッセージとリリース ノートで説明します。

  • 任意のターミネーション深度に対応できるコールグラフ補完のリビジョン。このアルゴリズムは、素晴らしい日を待って、しばらくの間 MiniAgda に留まっています。今ここにある！オプション --termination-depth を廃止できるようになりました。

そしてリリースノートから：

  • with で定義された関数の終了チェックが改善されました。

    以前は --termination-depth (現在は廃止されています) が終了チェッカーを通過する必要があったケース ('with' の使用により) では
    、フラグは不要になりました。例えば

    merge : List A → List A → List A
merge [] ys = ys
merge xs [] = xs
merge (x ∷ xs) (y ∷ ys) with x ≤ y
merge (x ∷ xs) (y ∷ ys)    | false = y ∷ merge (x ∷ xs) ys
merge (x ∷ xs) (y ∷ ys)    | true  = x ∷ merge xs (y ∷ ys)

    「with」が補助関数merge-auxに展開されるため、これは以前の終了チェックに失敗しました。

    merge-aux x y xs ys false = y ∷ merge (x ∷ xs) ys
merge-aux x y xs ys true  = x ∷ merge xs (y ∷ ys)

    この関数は、引数の 1 つのサイズが増加するマージを呼び出します。これをパスするために、終了チェッカーはチェックの前に merge-aux の定義をインライン化するようになりました。これにより、元のソース プログラムの終了チェックが効果的に行われます。

    この変換の結果、変数に対して「with」を実行しても終了が保持されなくなりました。たとえば、これは終了チェックを行いません:

    bad : Nat → Nat
bad n with n
... | zero  = zero
... | suc m = bad m

実際、元の関数は終了チェックに合格しました!

于 2013-07-28T20:27:18.270 に答える