agda - 列表合并的终止检查

Question

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 中是否可以？我在互联网上看到过类似的代码，但没有人提到那里的终止问题。

Answer 1

我无法告诉您发生这种情况的确切原因，但我可以向您展示如何治愈这些症状。在我开始之前:这是一个 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 上执行递归tors 然后转换回 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 中。

更新:Agda 的开发版本对终止检查器进行了更新，我将让提交消息和发行说明不言自明:

• A revision of call graph completion that can deal with arbitrary termination depth. This algorithm has been sitting around in MiniAgda for some time, waiting for its great day. It is now here! Option --termination-depth can now be retired.

并从发行说明:

• Termination checking of functions defined by 'with' has been improved.

  Cases which previously required --termination-depth (now obsolete!) to pass the termination checker (due to use of 'with') no longer
  need the flag. For example

  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)
  

  This failed to termination check previously, since the 'with' expands to an auxiliary function 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)
  

  This function makes a call to merge in which the size of one of the arguments is increasing. To make this pass the termination checker now inlines the definition of merge-aux before checking, thus effectively termination checking the original source program.

  As a result of this transformation doing 'with' on a variable no longer preserves termination. For instance, this does not termination check:

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

事实上，您的原始函数现在通过了终止检查!