终止检查失败

Question

我试图在 this kata about longest common subsequences of a list 上进行训练，我稍微修改了一下，以便它可以与我的 agda 版本和标准库（Agda 2.6.2，stdlib 1.7）一起使用，这导致了这个代码

{-# OPTIONS --safe #-}
module pg where

open import Data.List
open import Data.Nat
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary

data Subseq {n} { A : Set n } : List A → List A → Set where
subseq-nil : Subseq [] []
subseq-take : ∀ a xs ys → Subseq xs ys → Subseq (a ∷ xs) (a ∷ ys)
subseq-drop : ∀ a xs ys → Subseq xs ys → Subseq xs (a ∷ ys)

is-lcs : ∀ {n} {A : Set n} → List A → List A → List A → Set n
is-lcs zs xs ys =
(Subseq zs xs × Subseq zs ys) ×
(∀ ts → Subseq ts xs → Subseq ts ys → length ts ≤ length zs)

longest : ∀ {n} {A : Set n} → List A → List A → List A
longest s1 s2 with length s1 ≤? length s2
... | yes _ = s2
... | no _ = s1

lcs : ∀ {n} {A : Set n} → Decidable {A = A} _≡_ → List A → List A → List A
lcs _ [] _ = []
lcs _ _ [] = []
lcs dec (x ∷ xs) (y ∷ ys) with dec x y
... | yes _ = x ∷ lcs dec xs ys
... | no _ = longest (lcs dec (x ∷ xs) ys) (lcs dec xs (y ∷ ys))

不幸的是，Agda 无法识别 lcs 是一个终止函数，老实说我不明白这一点：如果我做对了，递归调用是在结构上更小的参数上进行的？如果有人能向我解释这里的问题是什么，那将大有帮助。提前致谢！

Answer 1

在处理终止时尽量避免使用with。当您的代码重构如下时，终止检查器成功（请注意，我删除了您的前两个定义，因为它们与您的问题无关，也许您应该相应地对其进行编辑）：

{-# OPTIONS --safe #-}

open import Data.List
open import Data.Nat
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Data.Bool using (if_then_else_)

module Term where

longest : ∀ {a} {A : Set a} → List A → List A → List A
longest s1 s2 with length s1 ≤? length s2
... | yes _ = s2
... | no _ = s1

lcs : ∀ {a} {A : Set a} → Decidable {A = A} _≡_ → List A → List A → List A
lcs _ [] _ = []
lcs _ _ [] = []
lcs dec (x ∷ xs) (y ∷ ys) = if does (dec x y) then
  x ∷ lcs dec xs ys else
  longest (lcs dec (x ∷ xs) ys) (lcs dec xs (y ∷ ys))

显然，这是 with 抽象结合终止检查器的已知限制，如 wiki 中所述：

https://agda.readthedocs.io/en/v2.6.2.1/language/with-abstraction.html#termination-checking

这是一个类似的问题：

终止检查失败

Termination checking failed

agda

agda-stdlib