Average Error: 63.0 → 56.4
Time: 18.0s
Precision: binary64
\[n > 6.8 \cdot 10^{+15}\]
\[\left(\left(n + 1\right) \cdot \log \left(n + 1\right) - n \cdot \log n\right) - 1\]
↓
\[\langle \left( \langle \left( \left({\left({\left(\sqrt{\sqrt[3]{n + 1}}\right)}^{\left(\sqrt[3]{4} \cdot \sqrt[3]{4}\right)}\right)}^{\left(\sqrt[3]{4}\right)} \cdot \left(\log \left(n + 1\right) \cdot \left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)\right) - n \cdot \log n\right) \right)_{binary64} \rangle_{posit16} \right)_{posit16} \rangle_{binary64} - 1\]
\left(\left(n + 1\right) \cdot \log \left(n + 1\right) - n \cdot \log n\right) - 1
↓
\langle \left( \langle \left( \left({\left({\left(\sqrt{\sqrt[3]{n + 1}}\right)}^{\left(\sqrt[3]{4} \cdot \sqrt[3]{4}\right)}\right)}^{\left(\sqrt[3]{4}\right)} \cdot \left(\log \left(n + 1\right) \cdot \left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)\right) - n \cdot \log n\right) \right)_{binary64} \rangle_{posit16} \right)_{posit16} \rangle_{binary64} - 1
(FPCore (n)
 :precision binary64
 (- (- (* (+ n 1.0) (log (+ n 1.0))) (* n (log n))) 1.0))
↓
(FPCore (n)
 :precision binary64
 (-
  (cast
   (!
    :precision
    posit16
    (cast
     (!
      :precision
      binary64
      (-
       (*
        (pow
         (pow (sqrt (cbrt (+ n 1.0))) (* (cbrt 4.0) (cbrt 4.0)))
         (cbrt 4.0))
        (*
         (log (+ n 1.0))
         (* (cbrt (sqrt (+ n 1.0))) (cbrt (sqrt (+ n 1.0))))))
       (* n (log n)))))))
  1.0))

Error

Bits error versus n

Target

Original63.0
Target0
Herbie56.4
\[\log \left(n + 1\right) - \left(\frac{1}{2 \cdot n} - \left(\frac{1}{3 \cdot \left(n \cdot n\right)} - \frac{4}{{n}^{3}}\right)\right)\]

Derivation

  1. Initial program 63.0

    \[\left(\left(n + 1\right) \cdot \log \left(n + 1\right) - n \cdot \log n\right) - 1\]
  2. Using strategy rm

  3. Applied add-cube-cbrt_binary6461.9

    \[\leadsto \left(\color{blue}{\left(\left(\sqrt[3]{n + 1} \cdot \sqrt[3]{n + 1}\right) \cdot \sqrt[3]{n + 1}\right)} \cdot \log \left(n + 1\right) - n \cdot \log n\right) - 1\]

  4. Applied associate-*l*_binary6461.8

    \[\leadsto \left(\color{blue}{\left(\sqrt[3]{n + 1} \cdot \sqrt[3]{n + 1}\right) \cdot \left(\sqrt[3]{n + 1} \cdot \log \left(n + 1\right)\right)} - n \cdot \log n\right) - 1\]

  5. Simplified61.8

    \[\leadsto \left(\left(\sqrt[3]{n + 1} \cdot \sqrt[3]{n + 1}\right) \cdot \color{blue}{\left(\log \left(n + 1\right) \cdot \sqrt[3]{n + 1}\right)} - n \cdot \log n\right) - 1\]
  6. Using strategy rm

  7. Applied add-sqr-sqrt_binary6461.8

    \[\leadsto \left(\left(\sqrt[3]{n + 1} \cdot \sqrt[3]{n + 1}\right) \cdot \left(\log \left(n + 1\right) \cdot \sqrt[3]{\color{blue}{\sqrt{n + 1} \cdot \sqrt{n + 1}}}\right) - n \cdot \log n\right) - 1\]

  8. Applied cbrt-prod_binary6461.7

    \[\leadsto \left(\left(\sqrt[3]{n + 1} \cdot \sqrt[3]{n + 1}\right) \cdot \left(\log \left(n + 1\right) \cdot \color{blue}{\left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)}\right) - n \cdot \log n\right) - 1\]
  9. Using strategy rm

  10. Applied insert-posit1659.4

    \[\leadsto \color{blue}{\langle \color{blue}{\left( \color{blue}{\langle \color{blue}{\left( \color{blue}{\left(\left(\sqrt[3]{n + 1} \cdot \sqrt[3]{n + 1}\right) \cdot \left(\log \left(n + 1\right) \cdot \left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)\right) - n \cdot \log n\right)} \right)_{binary64}} \rangle_{posit16}} \right)_{posit16}} \rangle_{binary64}} - 1\]

  11. Simplified59.4

    \[\leadsto \langle \left( \langle \left( \left(\color{blue}{{\left(\sqrt{\sqrt[3]{n + 1}}\right)}^{4} \cdot \left(\log \left(n + 1\right) \cdot \left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)\right)} - n \cdot \log n\right) \right)_{binary64} \rangle_{posit16} \right)_{posit16} \rangle_{binary64} - 1\]
  12. Using strategy rm

  13. Applied add-cube-cbrt_binary6456.4

    \[\leadsto \langle \left( \langle \left( \left({\left(\sqrt{\sqrt[3]{n + 1}}\right)}^{\left(\left(\sqrt[3]{4} \cdot \sqrt[3]{4}\right) \cdot \sqrt[3]{4}\right)} \cdot \left(\log \left(n + 1\right) \cdot \left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)\right) - n \cdot \log n\right) \right)_{binary64} \rangle_{posit16} \right)_{posit16} \rangle_{binary64} - 1\]

  14. Applied pow-unpow_binary6456.4

    \[\leadsto \langle \left( \langle \left( \left({\left({\color{blue}{\left(\sqrt{\sqrt[3]{n + 1}}\right)}}^{\left(\sqrt[3]{4} \cdot \sqrt[3]{4}\right)}\right)}^{\left(\sqrt[3]{4}\right)} \cdot \left(\log \left(n + 1\right) \cdot \left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)\right) - n \cdot \log n\right) \right)_{binary64} \rangle_{posit16} \right)_{posit16} \rangle_{binary64} - 1\]

  15. Final simplification56.4

    \[\leadsto \langle \left( \langle \left( \left({\left({\left(\sqrt{\sqrt[3]{n + 1}}\right)}^{\left(\sqrt[3]{4} \cdot \sqrt[3]{4}\right)}\right)}^{\left(\sqrt[3]{4}\right)} \cdot \left(\log \left(n + 1\right) \cdot \left(\sqrt[3]{\sqrt{n + 1}} \cdot \sqrt[3]{\sqrt{n + 1}}\right)\right) - n \cdot \log n\right) \right)_{binary64} \rangle_{posit16} \right)_{posit16} \rangle_{binary64} - 1\]

Reproduce

herbie shell --seed 2020285 
(FPCore (n)
  :name "logs (example 3.8)"
  :precision binary64
  :pre (> n 6.8e+15)

  :herbie-target
  (- (log (+ n 1.0)) (- (/ 1.0 (* 2.0 n)) (- (/ 1.0 (* 3.0 (* n n))) (/ 4.0 (pow n 3.0)))))

  (- (- (* (+ n 1.0) (log (+ n 1.0))) (* n (log n))) 1.0))