如何解决Dhall的整数分区
我想计算两个Natural
的商。我需要满足的要求是,我有一些配置项必须动态定义为另一项的共享(即,一个容器具有X
内存,该容器中该过程的两个配置键被定义为{{1 }}和X / Y
。
X / Z
尤其是,Dhall抱怨我尝试调用let quotient =
\(n: Natural) ->
\(m: Natural) ->
if lessthan n m then 0
else 1 + quotient (Natural/subtract m n) m
时尚未定义。考虑到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
中寻找现成的整数除法函数,但找不到。
解决方法
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
中的位置或多长时间subs
必须如此。
我的理论家很伤心,因为我只是将除法简化为对数(粗略近似),但是实践者说:“您一直对u64感到满意,闭嘴。”
[编辑]经过一番思考,我仍然无法有效地计算所有输入的对数(我认为不可能)。但是我可以从对数直至固定上限(2 ^ 2 ^ 23或42×10 ^ 2525221,但请参见下文)找到对数的下一个2的幂。可以通过以下方式修改上述功能(将其称为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上,我可以计算在11秒内达到2 ^(2 ^ 18)/ 7,但是对于更大的数字,内存不足。
无论如何,如果您有那么大的牛肉,那么您使用的是错误的语言。
,当前,除了您已经编写的内容以外,没有一种更简单的方法来实现Natural
除法,但是可能有一种更有效的方法。会带来对数时间复杂性但实现起来更加复杂的另一种方法是“猜测”,您可以在所需数字周围进行二进制搜索以找到最大数字x
,从而使x * m = n
尽管我真的不建议这样做,但我认为可能更好的方法是查看是否有明智的内建方法添加到可以有效地为整数除法提供支持的语言中。理想情况下,这样的内建函数对于所有输入都应定义良好,因此直接添加整数除法可能不起作用(因为x / 0
定义不明确)。但是,(我在这里开玩笑),也许像Natural/safeDivide x y == x / (y + 1)
这样的内置函数可以工作,然后,如果用户希望允许被0
划分,则用户可以围绕它们定义自己的包装器。可能最好的地方是内置Discourse论坛,以获取有关内置外观的想法:
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。