如何在Agda中将数字转换为字符串？

Question

如何在Agda中将数字转换为字符串？

5

我需要写一个将数字转换为字符串的Agda代码。之前有人询问如何将字符串转换为Agda代码。我考虑反过来使用它。请参考以下链接：Agda: parse a string with numbers。

row-to-stringh : (m : ℕ) → string
row-to-stringh 0 = "0"
row-to-stringh 1 = "1"
row-to-stringh 2 = "2"
row-to-stringh 3 = "3"
row-to-stringh 4 = "4"
row-to-stringh 5 = "5"
row-to-stringh 6 = "6"
row-to-stringh 7 = "7"
row-to-stringh 8 = "8"
row-to-stringh 9 = "9"
row-to-stringh _ = ""

但这还不够好。当数字大于9时，它只会将其转换为“”，而不是“(那个数字)”。有人能帮我吗？

- Bobai

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Vitus · Accepted Answer

如果您不想自己实现此函数，则标准库中有一个show函数。

如果您想要自己编写：将数字转换为字符串的常规方法是通过重复除以余数来提取数字。例如（余数用括号表示）：

7214 / 10 = 721 (4)
721  / 10 = 72  (1)
72   / 10 = 7   (2)
7    / 10 = 0   (7)

你只需将余数收集到列表中，然后反转并将数字转换为字符。尝试在Agda中实现这个过程是有诱惑力的，但你会遇到终止检查的问题。

首先，你必须让它相信`divMod`(即带余除法-模运算)是终止的。你可以在函数中硬编码除数，使得说服终止检查器变得容易。

困难之处在于要证明通过重复将数字除以10最终会终止。这可能需要一些相当复杂的技巧(如良基递归)。

如果你想知道如何用这种方式来做，可以查看上面链接的实现。无论如何，还有一种不太高效但更简单的方法来完成这个过程。

我们将数字表示为自然数列表。

Digits = List ℕ

我们想编写一个名为addOne的函数，它会将由数字列表表示的数字加一，即：

addOne : Digits → Digits

为此，我们将使用原始的纸笔方法：将1加到最低有效数字上；如果结果小于10，则完成；如果不是，则写0并将1进位到下一位数字。因此，这就是我们的进位：

data Carry : Set where
  +0 : Carry
  +1 : Carry

这是执行加法的函数 - 第二个Carry参数可以被视为前两位数字相加的进位。

ripple-carry : Digits → Carry → Digits
ripple-carry ns       +0 = ?
ripple-carry []       +1 = ?
ripple-carry (n ∷ ns) +1 with suc n ≤? 9
... | yes _ = ?
... | no  _ = ?

实际实现是一项练习 - 使用上面给出的描述。只需注意，我们以相反的顺序存储数字（这样可以更有效地实现和更容易）。例如，123由3 ∷ 2 ∷ 1 ∷ []表示，0由[]表示。我们可以恢复addOne函数：

addOne : Digits → Digits
addOne n = ripple-carry n +1

其余都只是管道工程。

toDigits : ℕ → Digits
toDigits zero    = []
toDigits (suc n) = addOne (toDigits n)

show : ℕ → String
show 0 = "0"
show n = (fromList ∘ map convert ∘ reverse ∘ toDigits) n
  where
  convert : ℕ → Char
  convert 0 = '0'
  convert 1 = '1'
  convert 2 = '2'
  convert 3 = '3'
  convert 4 = '4'
  convert 5 = '5'
  convert 6 = '6'
  convert 7 = '7'
  convert 8 = '8'
  convert 9 = '9'
  convert _ = ' ' -- Never happens.

使用的模块：

open import Data.Char
open import Data.List
open import Data.Nat
open import Data.String
open import Function
open import Relation.Nullary

我进行了一些测试，结果表明这种方法实际上相当有效（特别是与标准库中的函数相比）。

以上算法需要访问 O(n) 个数字（addOne 在 90% 的情况下只需要访问一个数字，在 9% 的情况下需要访问两个数字，在 0.9% 的情况下需要访问三个数字等等），对于给定的数字 n。除非我们有一些更快的原始操作（例如使用 Haskell 的 Integer 在后台执行的 _+_），否则这就是我们能够获得的最快速度 - 毕竟我们正在使用一元数字。

标准库使用上面提到的重复除法，这也是（除非我的数学有误）O(n)。然而，这并不包括处理证明所需的巨大开销，这会使其速度变慢。让我们来做一个比较：

open import Data.Nat
open import Data.Nat.Show
open import Function
open import IO

main = (run ∘ putStrLn ∘ show) n

这是编译代码所需的时间（在Emacs中使用C-c C-x C-c）。来自标准库的show命令：

n       time
———————————————
1000     410 ms
2000    2690 ms
3000    8640 ms

如果我们按照上述定义使用show函数，我们会得到如下结果：

n         time
———————————————
100000    26 ms
200000    41 ms
300000    65 ms