我很惊讶地看到以下函数未能通过终止检查。 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
到底是怎么回事? -抽象会干扰终止检查,那么我很乐意接受这个答案。
最佳答案
事实证明,这是自 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
关于agda - 使用 with-abstraction 的终止检查失败,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/62722346/