如何解决将二进制值类型加1
我想将二进制值加1，但是我对agda中的递归如何工作还不是很熟悉。
为什么我在这里没有得到正确的输出？
容器类型定义
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
我的增量功能
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = ⟨⟩ I
inc (x I) = (inc x) I
解决方法
算法快速修正
您的增量功能不正确。考虑到您对二进制数的定义：
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
您的增量函数应编写如下：
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
当正确的数字为零时，您只需将其替换为一，但您一定不要忘记保留数字的左侧部分。
当正确的数字为1时，您必须继续增加其左侧部分，但还需要将此1转换为0。
新算法的快速验证
但是，请不要相信我，让我们尝试（部分）验证我们的功能。毕竟，我们在举证助理中，对吗？
验证此类功能的一种好方法是评估其应提供的属性。增量函数的结果必须等于1加上其输入值。 Agda提供自然数，因此让我们将您的二进制数转换为自然数以检查此类属性。首先，一些进口：
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
然后是一个将二进制数转换为自然数的函数：
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
最后，我们的验证属性：
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
此验证当然是不完整的（从本质上来说），但至少可以使您对算法充满信心。在编写算法时，应该始终尝试证明这种假设，这是Agda的重点（不是全部，而是至少一部分）。
有关验证的更多信息
为了进一步说明我的观点，我决定尝试通过实现从自然数到二进制数的倒数转换来继续验证您对二进制数的表示形式：
_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)
我们可以直接证明这两个转换是互为倒数的：
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
然后我尝试做另一种方法：
↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
这一面需要prop₂，其签名如下：
prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O
此属性应为真（在某种意义上，我们认为的二进制数应满足它的含义），但不能用形式主义证明，因为您可以用无数种方式表示零，所有这些方式介词不相等（例如，prop₂等于n时0的第一种情况需要证明⟨⟩ ≡ (⟨⟩ O)，无法证明）。
总而言之，验证不仅使我们能够找到错误的算法（或证明算法正确），而且还可以揭示我们理论基础本身的不一致或错误（即使在这种情况下，可以快速浏览一下）足以看到0可以表示无数种不同的方式。
作为旁注，我并不是说应该总是有一种方法来表示抽象数据类型的特定元素，但是它肯定会有所帮助，尤其是在经常需要命题相等性时。 / p>
另一方面，对不起，我感到有些遗憾，但是我发现这类主题对于使用证明助手和形式验证非常有启发性。
请随时要求进一步的解释。
完整（且不完整）的代码
module BinaryNumber where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O
prop₂ {zero} = {!!}
prop₂ {suc n} = {!!}
↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
标准库
最后，二进制数存在于文件Data.Nat.Binary.Base中的标准库中，文件{{1}中具有相关的属性（特别是在您的表示中无法证明的对等属性） }}，如果您想看看它们是如何实现的。
当我们将 inc 定义为 Bin → Bin 时，我们是说它接受 Bin 类型的值并返回相同类型的值，即 Bin。
由于我们有 3 个构造函数可用于创建 Bin，Bin 类型的所有值都将具有以下 3 种形式之一：
- ⟨⟩
- b I 其中 b 是 Bin 类型的某个值
- b O 其中 b 是 Bin 类型的某个值
对于情况 1，因为⟨⟩ 代表零。
inc ⟨⟩ = ⟨⟩ I
对于情况 2，我们知道对以零结尾的数字加 1 只会将最后一位数字更改为 1，所以
inc (x O) = x I
对于情况 3，当一个数字以 1 结尾时，在增加它时，我们会在最后得到零，并且会生成需要向前传递的结转。可以使用我们相同的 inc 函数传递结转。假设 (inc x) 给出一个二进制数，我们取该输出并在末尾附加零。
inc (x I) = (inc x) O
此外，只是在 MrO 给出的出色答案的范围内，他正确地指出，由于有无限多种方式来表示零（和所有数字）
(b ↓) ↑ = b
不能证明 b 在第一个有效数字前有前导零。但是如果我们将↓↑的域限制为只有规范的二进制数，即没有任何前导零的二进制数，则可以推导出证明。
(b ↓) ↑ = b 对于规范 b 的证明
扩展 MrO 的代码，
module BinaryNumber where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
_↓ : ℕ → Bin
zero ↓ = ⟨⟩ O
suc n ↓ = inc (n ↓)
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
-- One b -> b start with ⟨⟩ I
data One : Bin → Set where
first : One (⟨⟩ I)
nextO : ∀ { b : Bin }
→ One b
------------
→ One (b O)
nextI : ∀ { b : Bin }
→ One b
------------
→ One (b I)
-- Can i.e Canonical representing binary numbers without extras leading zeros after ⟨⟩. For e.g ⟨⟩ O O I I and ⟨⟩ I I both represents binary form of number 3 but only ⟨⟩ I I is the canonical
data Can : Bin → Set where
startWithZero : Can (⟨⟩ O)
startWithOne : ∀ {b : Bin }
→ One b
------------
→ Can b
-- If m ≤ n then m ≤ (n + 1)
≤-sucʳ : ∀ {m n : ℕ }
→ m ≤ n
-----------
→ m ≤ suc n
≤-sucʳ z≤n = z≤n
≤-sucʳ (s≤s m≤n) = s≤s (≤-sucʳ m≤n)
-- If m ≤ n then m ≤ (n + p)
≤-addʳ : ∀ (m n p : ℕ)
→ m ≤ n
--------
→ m ≤ n + p
≤-addʳ m n zero m≤n rewrite +-comm n zero = m≤n
≤-addʳ m n (suc p) m≤n rewrite +-comm n (suc p) | +-comm p n = ≤-sucʳ (≤-addʳ m n p m≤n)
-- If a natural number n has eqivalent binary form (⟨⟩ I b) then 1 ≤ n
1-≤-oneb : ∀ { b : Bin }
→ One b
---------
→ suc zero ≤ b ↑
1-≤-oneb first = s≤s z≤n
1-≤-oneb {b O} (nextO oneb) = ≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb)
1-≤-oneb {b I} (nextI oneb) = ≤-sucʳ (≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb))
-- If 0 ≤ (n + 1) then 1 ≤ n
0-≤-suc : ∀ (n : ℕ)
→ 0 ≤ suc n
-----------
→ 1 ≤ suc n
0-≤-suc n z≤n = s≤s z≤n
-- If 1 ≤ n and binary form of n is b then binary form of (n + n) using ↓ is b O
↓-over-+ : ∀ (n : ℕ)
→ 1 ≤ n
-----------------------
→ (n + n) ↓ ≡ (n ↓) O
↓-over-+ (suc zero) s≤n = refl
↓-over-+ (suc (suc n)) (s≤s s≤n) = begin
(suc (suc n) + (suc (suc n))) ↓
≡⟨⟩
inc (( suc n + (suc (suc n))) ↓)
≡⟨ cong (inc) (cong (_↓) (+-comm (suc n) (suc (suc n)))) ⟩
inc (inc ((suc n + suc n) ↓))
≡⟨ cong (inc) (cong inc (↓-over-+ (suc n) (0-≤-suc n s≤n))) ⟩
refl
-- For all binary numbers that are canonical,↑↓ is identity (returns same b)
↑↓-canb : ∀ ( b : Bin )
→ Can b
--------------
→ (b ↑) ↓ ≡ b
↑↓-canb _ startWithZero = refl
↑↓-canb _ (startWithOne first) = refl
↑↓-canb (b O) (startWithOne (nextO x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl
↑↓-canb (b I) (startWithOne (nextI x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。