Agda 中函数的终止检查失败

Question

我目前正在为这个项目编写以下不完整的函数：

  extend : ∀ o asc (s : CSet (suc k) o) → SC asc → SC (add s asc)
  extend 0 asc s rewrite l≡0 s Eq.refl =
    restrict (add (empty _) asc) asc (add-∈ asc (empty∈asc asc))
  extend 1 asc s = restrict (add s asc) asc (add-∈ asc (asc .hasAllPoints s))
  extend {k} (suc (suc o)) asc s with has asc (_ , s) in eq
  ... | true = restrict (add s asc) asc (add-∈ asc (pser T eq tt))
  ... | false = result
    module Extend where      
      extendAll : ∀ bsc (ss : Fin m → CSet (suc k) (suc o)) → SC bsc → SC (addAll ss bsc)
      extendAll {zero} _ _ sc = sc
      extendAll {suc _} bsc ss sc =
        let head-ss = ss zero
            tail-ss i = ss (suc i)
        in extendAll (add head-ss bsc) tail-ss (extend (suc o) bsc head-ss sc)

      faces : SC asc → SC (addAll (except s) asc)
      faces = extendAll asc (except s)

      cycl : SC asc → Cycle P o
      cycl sc .face i = faces sc .for (∈-addAll (except s) asc i)
      cycl sc .compatible i j =
        P.proj (punchIn i) (cycl sc .face j) ≈˘⟨ P.map-cong (embed-except (except s j) Eq.refl _) _ ⟩
        P.proj (embed (except⊂s (except s j) i)) (cycl sc .face j) ≡⟨⟩
        P.proj (embed (except⊂s (except s j) i)) (faces sc .for (∈-addAll (except s) asc j)) ≈˘⟨ faces sc .compat (∈-addAll (except s) asc _) _ ⟩
        faces sc .for (Has-⊆ (addAll (except s) asc) (except⊂s (except s j) i) (∈-addAll (except s) asc j)) ≡˘⟨ for-resp (faces sc) _ _ ⟩
        faces sc .for (resp (_∈ addAll (except s) asc) (except-except s Eq.refl j i) (Has-⊆ (addAll (except s) asc) (except⊂s (except s j) i) (∈-addAll (except s) asc j))) ≡⟨ faces sc .for =$= T-irrel ⟩
        faces sc .for (Has-⊆ (addAll (except s) asc) (except⊂s (except s (punchIn j i)) (pinch i j)) (∈-addAll (except s) asc (punchIn j i))) ≈⟨ faces sc .compat _ _ ⟩
        P.proj (embed (except⊂s (except s (punchIn j i)) (pinch i j))) (faces sc  .for (∈-addAll (except s) asc (punchIn j i))) ≡⟨⟩
        P.proj (embed (except⊂s (except s (punchIn j i)) (pinch i j))) (cycl sc .face (punchIn j i)) ≈⟨ P.map-cong (embed-except (except s (punchIn j i)) Eq.refl _) _ ⟩
        P.proj (punchIn (pinch i j)) (cycl sc .face (punchIn j i)) ∎
        where open Relation.Reasoning (P._≃_)
              open Equiv (refl (P.Space _)) (trig (P.Space _))

      result : SC asc → SC (add s asc)
      result sc .for {s = t} t∈added with add-⊂ {s = t} {s} {asc} t∈added
      ... | inj₂ t∈asc = sc .for t∈asc
      ... | inj₁ t⊂s with ⊂-except t⊂s Eq.refl
      ... | inj₂ (i , t⊂except) = faces sc .for (Has-⊆ (addAll (except s) asc) t⊂except (∈-addAll (except s) asc i))
      ... | inj₁ (Eq.refl , Eq.refl) = ?
      result sc .compat = ?

正如我们所看到的，

extend

对其自身的唯一递归调用是在最后一个分支中，其中第一个显式参数

o

（这是一个自然数）与

suc (suc o)

进行模式匹配，并且递归调用本身传递

suc o

作为第一个显式参数，因此它严格小于匹配的一个模式。

然而，Agda 2.6.4.1 拒绝这个定义并抱怨终止检查失败。我在这里遗漏了一些东西还是这可能是一个错误？

顺便说一句，很抱歉没有包含此函数中使用的所有定义，因为实在太多了。如果您想自己尝试一下，可以在前述项目中的here下找到此函数的稍微修改版本，其中递减参数（此处命名为

l

而不是

o

）是隐式的而不是显式的（如最初预期），并且

extendAll

被移到

extend

之外。

Answer 1

我不知道这是否有帮助，无论如何，你的代码片段对我来说太复杂了，无法考虑深入细节......但是如果你改变模式

suc (suc o)

，随后使用

，会发生什么下面的suc o

，而不是

suc o@(suc _)

，所有后续出现的

suc o

现在都只是

o

本身？

据我所知，在任何调用中都没有使用

o

的附加子项

suc (suc o)

，因此使用

@

模式会更精确，并简化后续代码。人们可能希望...