我試圖在這個 kata 上訓練一個串列的最長公共子序列，我稍微修改了一下，以便它可以與我的 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 是一個終止函式，老實說我不明白這一點：如果我做對了，遞回呼叫是在結構上更小的引數上進行的？如果有人能向我解釋這里的問題是什么，那將大有幫助。提前致謝 ！
uj5u.com熱心網友回復：
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
這是一個類似的問題：
使用 with-abstraction 的終止檢查失敗
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/536812.html
上一篇：Agda安裝PLFA配置