带有模糊终止的条款
With clauses obscuring termination
我正在尝试在 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 ⇑⟧
终止检查有充分的理由失败，因为以下函数在其输入上不是结构递归的：
⟦_⇑⟧ : ℕ →
⟦ 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 returns 2 求值时 test.
考虑定义：
test₁ : ℕ
test₁ = ⟦ ⟦ 16 ⇑⟧ ⇓⟧
Agda returns 14 计算时 test₁
为了更正您的定义，您可以从标准库中的工作中获取灵感，可以是模块 Data.Bin（已弃用）或模块 Data.Nat.Binary，具体取决于哪个版本你拥有的标准库。
我正在尝试在 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 ⇑⟧
终止检查有充分的理由失败，因为以下函数在其输入上不是结构递归的：
⟦_⇑⟧ : ℕ → ⟦ 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 returns 2 求值时 test.
考虑定义：
test₁ : ℕ
test₁ = ⟦ ⟦ 16 ⇑⟧ ⇓⟧
Agda returns 14 计算时 test₁
为了更正您的定义，您可以从标准库中的工作中获取灵感，可以是模块 Data.Bin（已弃用）或模块 Data.Nat.Binary，具体取决于哪个版本你拥有的标准库。