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 中可能还可以吗？我在 Internet 上看到过类似的代码，但没有人提到那里的终止问题。
【问题讨论】：
标签： agda
我不能告诉你发生这种情况的确切原因，但我可以告诉你如何治愈这些症状。在我开始之前：这是带有终止检查器的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
最后，我们可以对Vectors 执行递归，然后转换回List：
open import @987654323@ 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 @987654324@
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
注意：在较新版本的 Agda 中，可以使用在定义两个函数之前声明它们的签名来代替 mutual。
更新：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)此函数调用合并，其中一个的大小 争论越来越多。为了使它通过终止检查器 现在在检查之前内联合并辅助的定义，因此 有效地终止检查原始源程序。
由于这种转换对变量 no 执行“with” 更长的保留终止。例如，这不 终止检查：
bad : Nat → Nat bad n with n ... | zero = zero ... | suc m = bad m
确实，您的原始函数现在通过了终止检查！
【讨论】：