将二进制值类型加一

Question

我想将二进制值加一，但我仍然不太熟悉 agda 中递归的工作原理。

为什么我在这里没有得到正确的输出？

Bin 类型定义

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 

Answer 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

当正确的数字为零时，您只需将其替换为一，但您一定不要忘记保留数字的左侧部分。

当正确的数字为 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?whenn等于的第一种情况0需要证明?? ? (?? O)哪个不能被证明）。

总而言之，验证不仅可以让我们找到错误的算法（或证明算法正确），而且还可以揭示我们理论基础本身的不一致或错误（即使在这种情况下，快速浏览一下就足够了看到 0 可以表示无数种不同的方式）。

作为旁注，我并不是说应该总是有一种方法来表示抽象数据类型的特定元素，但它肯定会有所帮助，尤其是在处理命题相等时，这通常是必需的。

另一方面，如果我有点得意忘形，我很抱歉，但我发现这些主题对于证明助手和正式验证的使用非常有启发性。

请随时要求任何进一步的解释。

完整的（在某种程度上是不完整的）代码

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。