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的总体功能范式（以及我对其的不熟悉），这似乎是合理的。我认为可能有某种方法可以做到，但不幸的是我无法做到这一点。

我尝试了使用quotient的另一种方法，但效果不明显。

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论坛，以获取有关内置外观的想法：

https://discourse.dhall-lang.org/