agda - 使用 with-abstraction 的终止检查失败

Question

我很惊讶地看到以下函数未能通过终止检查。 y ∷ ys在结构上小于 x ∷ y ∷ ys ，不是吗？

open import Data.List using (List ; [] ; _∷_)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Nat.Properties using (<-cmp)

foo : List ℕ → ℕ
foo [] = 0
foo (x ∷ []) = 1
foo (x ∷ y ∷ ys) with <-cmp x y
... | _ = suc (foo (y ∷ ys))

做以下两件事中的一件(或两件)似乎能让终止检查器看到曙光:

• 删除 with -抽象。

• 更改最后一个子句以匹配 y ∷ ys而不是 x ∷ y ∷ ys并递归 ys而不是 y ∷ ys . (并且由于缺少 <-cmp x y 而将 <-cmp y y 更改为 x。)

现在我比平时更加​​困惑，我想知道:这是怎么回事，with 是怎么回事？ -抽象(及其辅助函数)影响了所有这些，我该怎么做？

我看过关于终止的其他问题和答案，但是 - 与那些更复杂的情况不同 - 手头的情况似乎是关于基本结构递归，不是吗？

更新

我刚刚找到了问题的答案，但如果有人想更清楚地了解到底发生了什么，例如，with 到底是怎么回事？ -抽象会干扰终止检查，那么我很乐意接受这个答案。

Answer 1

事实证明，这是自 2.6.1 以来终止检查器的已知限制。请参阅 2.6.1 更改日志中的终止检查部分:https://github.com/agda/agda/blob/v2.6.1/CHANGELOG.md

模式匹配和递归调用将无法与它们之间的 with 抽象一起使用。一种解决方法是也对递归调用进行抽象，以便将其拉起到with-抽象(从其在with之后的原始位置) -抽象)。

open import Data.List using (List ; [] ; _∷_)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Nat.Properties using (<-cmp)

foo : List ℕ → ℕ
foo [] = 0
foo (x ∷ []) = 1
foo (x ∷ y ∷ ys) with foo (y ∷ ys) | <-cmp x y
... | rec | _ = suc rec

在上面的代码中，模式匹配x ∷ y ∷ ys和递归调用foo (y ∷ ys)不要跨越和-不再抽象，终止检查成功。

以上解决了我的问题，但更改日志描述了更微妙的情况，需要多加注意。

此问题在 Agda 问题 #59 (!) 中进行了跟踪，其中包含更多详细信息和问题的历史记录:https://github.com/agda/agda/issues/59