带有抽象的终止检查失败答案

【问题标题】：Failing termination check with a with-abstraction带有抽象的终止检查失败
【发布时间】：2020-07-03 20:33:18
【问题描述】：

我很惊讶以下函数未能通过终止检查。 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-abstraction。
更改最后一个子句以匹配 y ∷ ys 而不是 x ∷ y ∷ ys 并使用 ys 而不是 y ∷ ys 进行递归。（并且由于缺少xs，还将<-cmp x y 更改为<-cmp y y。）

现在我比平时更困惑，我想知道：发生了什么事，with-abstraction（及其辅助函数）如何影响所有这些，我该怎么做?

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

更新

我刚刚找到了这个问题的答案，但是如果有人想更清楚地了解到底发生了什么，例如，with-abstraction 究竟是如何干扰终止检查的，那么我会超过很高兴接受这个答案。

【问题讨论】：

这确实很奇怪......尤其是当注意到终止时的wiki页面（agda.readthedocs.io/en/v2.6.1/language/…）有一个名为“with-functions”的部分恰好是空的。我将进行更多测试，看看是否可以理解这种行为。
它看起来确实像一个错误。您可以在定义之前使用{-# TERMINATING #-} pragma 以避免出现此警告，即使它只是隐藏了问题。如果没有其他人在这里找到原因，您可以提交错误报告。
非常感谢您对此进行调查！我还做了一些研究，偶然发现了 2.6.1 CHANGELOG.md 文件中的一个注释，它指出这是终止检查器的一个已知限制，并提供了一种解决方法。我会写一个答案。
我很想知道是什么导致了这种限制。
我也是！也许其他人会参与进来。再次感谢您考虑到这一点。

标签： agda

【解决方案1】：

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

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

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) 不再跨越with 抽象，终止检查成功。

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

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

【讨论】：