带有模糊终止条款

Question

我试图在agda中定义二进制数，但agda看不到⟦_⇑⟧正在终止。我真的不想打破无障碍关系。如何向agda显示n变小？

module Binary where
open import Data.Nat using (ℕ; _+_; +-suc)
open ℕ
2* : ℕ → ℕ
2* n = n + n
data Parity : ℕ → Set where
𝕖 : ∀ k → Parity (2* k)
𝕠 : ∀ k → Parity (1 + 2* k)
parity : ∀ n → Parity n
parity zero = 𝕖 0
parity (suc n) with parity n
parity (suc .(k + k)) | 𝕖 k = 𝕠 k
parity (suc .(suc (k + k))) | 𝕠 k rewrite sym (+-suc k k) = 𝕖 (suc k)
data 𝔹 : Set where
𝕫 : 𝔹
𝕖 : 𝔹 → 𝔹
𝕠 : 𝔹 → 𝔹
⟦_⇓⟧ : 𝔹 → ℕ
⟦ 𝕫 ⇓⟧ = 0
⟦ 𝕖 b ⇓⟧ = 2* ⟦ b ⇓⟧
⟦ 𝕠 b ⇓⟧ = 1 + 2* ⟦ b ⇓⟧
⟦_⇑⟧ : ℕ → 𝔹
⟦ zero ⇑⟧ = 𝕫
⟦ suc n ⇑⟧ with parity n
⟦ suc .(k + k) ⇑⟧ | 𝕖 k = 𝕠 ⟦ k ⇑⟧
⟦ suc .(suc (k + k)) ⇑⟧ | 𝕠 k = 𝕖 ⟦ k ⇑⟧

错误：

Termination checking failed for the following functions:
⟦_⇑⟧
Problematic calls:
⟦ k ⇑⟧

Answer 1

终止检查失败的原因很充分，因为以下函数在结构上不是递归的：

⟦_⇑⟧ : ℕ → 𝔹
⟦ zero ⇑⟧ = 𝕫
⟦ suc n ⇑⟧ with parity n
⟦ suc .(k + k) ⇑⟧ | 𝕖 k = 𝕠 ⟦ k ⇑⟧
⟦ suc .(suc (k + k)) ⇑⟧ | 𝕠 k = 𝕖 ⟦ k ⇑⟧

Agda甚至告诉您什么是有问题的调用：⟦ k ⇑⟧。(在这种情况下，有两个格式不正确的调用(。

虽然我同意函数是在结构较小的参数上调用的，但事实并非如此。要理解原因，您必须看到k被用作函数调用_+_的输入，并且只有该函数的结果在结构上小于n，而不是k本身。并且agda无法知道_+_的以下性质：

∀ {n} → n < suc (n + n)

如果你提供这样一个引理的证明，你可以使用_<_是有充分根据的事实来使你的函数在结构上递归于Acc，但你似乎不愿意这样做

理解为什么Agda不能知道它终止的一个简单方法是：假设用suc .(a ∸ b)替换suc .(k + k)，并通过a递归调用函数。从agda的角度来看，两者都是相同的情况，在这种情况下，除非b恰好是0，否则它通常不会终止。

---

这是根据终止校正的模块：

module Binary where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Induction.Nat
open import Induction.WellFounded
2* : ℕ → ℕ
2* n = n + n
data Parity : ℕ → Set where
𝕖 : ∀ k → Parity (2* k)
𝕠 : ∀ k → Parity (1 + 2* k)
parity : ∀ n → Parity n
parity zero = 𝕖 0
parity (suc n) with parity n
parity (suc .(k + k)) | 𝕖 k = 𝕠 k
parity (suc .(suc (k + k))) | 𝕠 k rewrite sym (+-suc k k) = 𝕖 (suc k)
data 𝔹 : Set where
𝕫 : 𝔹
𝕖 : 𝔹 → 𝔹
𝕠 : 𝔹 → 𝔹
⟦_⇓⟧ : 𝔹 → ℕ
⟦ 𝕫 ⇓⟧ = 0
⟦ 𝕖 b ⇓⟧ = 2* ⟦ b ⇓⟧
⟦ 𝕠 b ⇓⟧ = 1 + 2* ⟦ b ⇓⟧
decr : ∀ {n} → n < suc (n + n)
decr {n} = s≤s (m≤m+n n n) 
helper : (n : ℕ) → Acc _<_ n → 𝔹
helper zero a = 𝕫
helper (suc n) a with parity n
helper (suc .(k + k)) (acc rs) | 𝕖 k = 𝕠 (helper k (rs _ decr))
helper (suc .(suc (k + k))) (acc rs) | 𝕠 k = 𝕖 (helper k (rs _ (s≤s (<⇒≤ decr))))
⟦_⇑⟧ : ℕ → 𝔹
⟦ n ⇑⟧ = helper n (<-wellFounded n)

---

我也对你的定义的正确性持怀疑态度，事实证明我是对的，例如，考虑到以下定义：

test : ℕ
test = ⟦ ⟦ 124 ⇑⟧ ⇓⟧

Agda在评估CCD_ 16时返回CCD_。

考虑定义：

test₁ : ℕ
test₁ = ⟦ ⟦ 16 ⇑⟧ ⇓⟧

Agda在评估test₁时返回14

为了纠正您的定义，您可以从标准库中所做的工作中获得灵感，无论是在模块Data.Bin(已弃用(中还是在模块Data.Nat.Binary中，具体取决于您拥有的stdlib版本。