終止檢查合併

阿格達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版本中它可能還行嗎？我在互聯網上看到過類似的代碼，沒有人提到終止問題。

來源

2013-07-28 András Kovács

我不能告訴你爲什麼會發生這種情況，但我可以告訴你如何治癒症狀。在我開始之前：這是帶終止檢查器的known problem。如果你精通Haskell，你可以看看source。

一種可能的解決方案是將功能分割成兩個：第一個爲其中第一個參數將獲取第二個較小的和第二殼體：

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，我們切換到第二個功能，反之亦然。

其它的（也許令人驚訝的）的選項，這也是在問題報告中提到，是通過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

最後，我們可以執行遞歸在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回報List直接和完全避免引理：

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中。

更新：阿格達的開發版本有一個更新終止檢查，我就讓提交信息和發行說明一切：

調用圖完成的修訂可以處理任意終止深度。這個算法已經在MiniAgda中待了一段時間，正在等待它的美好一天。它現在在這裏！選項 - 終止深度現在可以退役。

而從發佈說明：由 '與' 定義的函數

終止檢查已被提高。以前需要--termination深度（現在已經過時！）

案件通過終止檢查（由於使用「與」的）不再
需要的標誌。例如
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) 
這未能終止檢查先前，由於在「與」擴展到一個輔助功能合併-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) 
此函數進行調用以合併在其尺寸其中一個的論點正在增加。爲了通過這個過程，終止檢查器現在在檢查之前嵌入merge-aux的定義，因此有效地終止檢查原始源程序。

由於此變換對'變量'做了變量，所以更長的時間保留終止。舉例來說，這並不終止檢查：
bad : Nat → Nat 
bad n with n 
... | zero = zero 
... | suc m = bad m 

事實上，原來的功能現在通過終止檢查！

來源

2013-07-28 20:27:18 Vitus

謝謝，這只是我尋找的答案。 –

終止檢查合併

回答

相關問題