Dhall中的整数除法
Posted
技术标签:
【中文标题】Dhall中的整数除法【英文标题】：Integer division in Dhall 【发布时间】：2020-09-29 08:53:16 【问题描述】：我想计算两个Naturals 的商。我需要满足的要求是我有一些配置项必须动态定义为另一个容器的共享（即一个容器具有X 内存，该容器中进程的两个配置键定义为X / Y 和@ 987654324@).
我的第一个想法是使用递归，但这种方法行不通：
let quotient =
\(n: Natural) ->
\(m: Natural) ->
if lessThan n m then 0
else 1 + quotient (Natural/subtract m n) m
特别是，当我尝试调用 quotient 时，Dhall 抱怨它尚未定义。鉴于 Dhall 的全部功能范式（以及我对它的不熟悉），这似乎是合理的。我认为可能有某种方法可以做到这一点，但不幸的是我无法做到。
我使用Natural/fold 进行了另一次尝试，但我不确定这是否有意义。
let quotient =
λ(n : Natural) →
λ(m : Natural) →
let div =
λ(n : Natural) →
λ(m : Natural) →
let Div = q : Natural, r : Natural
in Natural/fold
n
Div
( λ(d : Div) →
if Natural/isZero m
then d
else if lessThan d.r m
then d
else q = d.q + 1, r = Natural/subtract m d.r
)
q = 0, r = n
in (div n m).q
这会通过以下所有断言。
let example1 = assert : quotient 1 1 ≡ 1
let example2 = assert : quotient 2 2 ≡ 1
let example3 = assert : quotient 3 1 ≡ 3
let example4 = assert : quotient 3 2 ≡ 1
let example5 = assert : quotient 9 4 ≡ 2
let example6 = assert : quotient 4 5 ≡ 0
let example7 = assert : quotient 0 1 ≡ 0
let example8 = assert : quotient 0 2 ≡ 0
let example9 = assert : quotient 1 0 ≡ 0
let example9 = assert : quotient 0 0 ≡ 0
let example9 = assert : quotient 2 0 ≡ 0
在我的情况下，除以 0 时返回 0 很好。
有没有更惯用的方法来实现这一点？我在Prelude中找了一个现成的整数除法函数但是没找到。
【问题讨论】：
【参考方案1】：TL;WR 编辑：
let Natural/div = λ(n : Natural) → λ(m : Natural) →
let div = https://github.com/jcaesar/dhall-div/releases/download/1/quotient.dhall sha256:d6a994f4b431081e877a0beac02f5dcc98f3ea5b027986114487578056cb3db9
in (div n m).q
Gabriel Gonzalez 用他的answer 提到二分搜索让我非常讨厌。有一段时间，我在圈子里跑，尝试通过将数字转换为List Bool是否无法实现搜索所需的除以二（嗯，可以，与以下相同的问题），然后我注意到你可以实现长除法：
let Natural/le = λ(a : Natural) → λ(b : Natural) → Natural/isZero (Natural/subtract b a)
let Natural/equals = λ(a : Natural) → λ(b : Natural) → Natural/le a b && Natural/le b a
let bits =
λ(bits : Natural) →
Natural/fold
bits
(List Natural)
( λ(l : List Natural) →
l
# [ merge
Some = λ(i : Natural) → i * 2, None = 1
(List/last Natural l)
]
)
([] : List Natural)
in λ(w : Natural) →
let bits = bits w
in λ(n : Natural) →
λ(m : Natural) →
let T = r : Natural, q : Natural : Type
let div =
List/fold
Natural
bits
T
( λ(bit : Natural) →
λ(t : T) →
let m = m * bit
in if Natural/le m t.r
then r = Natural/subtract m t.r, q = t.q + bit
else t
)
r = n, q = 0
in if Natural/equals m 0 then 0 else div.q
唯一的问题是，由于没有对数，您不能在表格中进行左对齐以进行长除法，即您不知道 MSB 在n 中的位置或@987654326 中的位置有多长@ 必须是。
我的理论家很伤心，因为我只是将除法简化为（粗略的近似）对数，但实践者说“你一直对 u64 很满意，闭嘴。”
[编辑] 经过一番思考，我仍然无法有效地计算所有输入的对数（我认为这是不可能的）。但我可以从数字的对数中找到下一个 2 的幂，直到一个固定的大限制（2^2^23 或 42 × 10^2525221，但见下文）。可以通过以下方式修改上述函数（我们称之为quotient）：
let Natural/less =
λ(a : Natural) →
λ(b : Natural) →
if Natural/isZero (Natural/subtract a b) then False else True
let max = 23
let powpowT = l : Natural, n : Natural
let powpow =
Natural/fold
max
(List powpowT)
( λ(ts : List powpowT) →
merge
Some =
λ(t : powpowT) → [ l = t.l + t.l, n = t.n * t.n ] # ts
, None = [ l = 1, n = 2 ]
(List/head powpowT ts)
)
([] : List powpowT)
let powpow = List/reverse powpowT powpow
let bitapprox =
λ(n : Natural) →
List/fold
powpowT
powpow
Natural
( λ(e : powpowT) →
λ(l : Natural) →
if Natural/less n e.n then e.l else l
)
0
in λ(n : Natural) → λ(m : Natural) → quotient (bitapprox n) n m
这给出了一个可接受的商的有效实现，一个长除法表最大是必要的两倍。在我的桌面 (62GB) m 上，我可以计算例如2^(2^18) / 7 在 11 秒内，但是对于更大的数字会耗尽内存。
无论如何，如果您对这么大的数字感到不满，那么您使用的是错误的语言。
【讨论】：
【参考方案2】：目前除了您已经编写的内容之外，没有更简单的方法来实现Natural 除法，但可能有更有效的方法。另一种会给出对数时间复杂度但实现要复杂得多的方法是“猜测和检查”，您可以在所需数字周围进行二进制搜索，以找到最大的数字 x，例如 x * m = n。
不过，我真的不建议这样做，而且我认为可能更好的方法是查看是否有一个明智的内置函数可以添加到可以有效地支持整数除法的语言中。理想情况下，这样的内置函数将对所有输入进行明确定义，因此直接添加整数除法可能不起作用（因为 x / 0 没有明确定义）。但是（我在这里吐槽），也许像Natural/safeDivide x y == x / (y + 1) 这样的内置函数可以工作，然后用户可以定义自己的包装器，如果他们想允许被0 分割。就内置的外观征求意见的最佳地点可能是 Discourse 论坛：
https://discourse.dhall-lang.org/
【讨论】：
嗯，如果Natural/subtract 3 1 === 0，那为什么不应该Natural/divide x 0 === 0？
我只是尝试用上述实现将 2^30 除以 6，显然内存不足。所以我很好奇：你将如何实现二进制搜索？你不需要除以 2 和一个对数吗（我想我可以用 Natural/show + 字符串长度来近似对数，以上是关于Dhall中的整数除法的主要内容，如果未能解决你的问题，请参考以下文章