时间戳

首页 > 解决方案 > 带有抽象的终止检查失败

agda - 带有抽象的终止检查失败

问题描述

我很惊讶地看到以下函数未能通过终止检查。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（及其辅助函数）如何影响所有这些，我该怎么办？

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

更新

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

标签： agda

解决方案

Turns out that this is a known limitation of the termination checker since 2.6.1. See the Termination checking section in the change log for 2.6.1: https://github.com/agda/agda/blob/v2.6.1/CHANGELOG.md

The pattern match and the recursive call won't work with a with-abstraction between them. A workaround is to also abstract over the recursive call in order to pull it up into the with-abstraction (from its original location after the 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

In the above code, the pattern match x ∷ y ∷ ys and the recursive call foo (y ∷ ys) don't straddle the with-abstraction any longer and the termination check succeeds.

The above fixes my issue, but the change log describes more delicate cases that require a little more care.

This issue is tracked in Agda issue #59 (!), which contains more details and a history of the problem: https://github.com/agda/agda/issues/59

推荐阅读