按1递增二进制值类型

你的增量函数不正确。考虑到你对二进制数的定义:

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

当右边的数字是0时,你只要用1来代替它,但是你不能忘记保留数字的左边部分。

新算法的快速验证

验证这样一个函数的一个好方法是评估它应该提供哪些属性。增量函数的结果必须等于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

这个属性应该是真的(在这个意义上,我们认为二进制数应该满足它),但是它不能在你的形式主义中被证明,因为你可以用无数种方式来表示零,而且所有这些方式都不是介词相等的(例如 道具 n 等于 0 需要证明 ⟨⟩ ≡ (⟨⟩ O) 无法证明)。

作为旁注,我并不是说应该总是有一种方法来表示抽象数据类型的特定元素,但它确实有帮助,特别是在处理命题等式时,这是经常需要的。

另一方面,我很抱歉,如果我有点失控,但我发现这些话题非常启发有关使用证明助理和正式验证。

请随时要求进一步解释。

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 Data.Nat.Binary.Properties 如果你想看看他们是如何实现的。