Hyperbolic arc-(co)tangent

Average Accuracy: 8.4% → 100.0%

Time: 10.6s

Precision: binary64

Cost: 13440

Math

\[\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(1, x\right)\right)\right)\right) \]

↓

\[\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{log1p.f64}\left(x\right)\right), \mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right) \]

FPCore

(FPCore (x)
 :precision binary64
 (*.f64 (/.f64 1 2) (log.f64 (/.f64 (+.f64 1 x) (-.f64 1 x)))))

↓

(FPCore (x)
 :precision binary64
 (*.f64 1/2 (-.f64 (*.f64 2 (log1p.f64 x)) (log1p.f64 (neg.f64 (*.f64 x x))))))

Derivation

1. Initial program 8.4%

   \[\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(1, x\right)\right)\right)\right) \]

2. Simplified 8.4%

   \[\leadsto \color{blue}{\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(1, x\right)\right)\right)\right)} \]
   Proof

   [Start] 8.4	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(1, x\right)\right)\right)\right) \]
   metadata-eval [=>] 8.4	\[ \mathsf{*.f64}\left(\color{blue}{\frac{1}{2}}, \mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(1, x\right)\right)\right)\right) \]

3. Applied egg-rr 8.4%

   \[\leadsto \mathsf{*.f64}\left(\frac{1}{2}, \color{blue}{\mathsf{neg.f64}\left(\mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right), 1\right)\right)\right)}\right) \]
   Proof

   [Start] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(1, x\right)\right)\right)\right) \]
   clear-num [=>] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{log.f64}\left(\color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right)\right)}\right)\right) \]
   clear-num [=>] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{log.f64}\left(\color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right), 1\right)\right)}\right)\right) \]
   log-rec [=>] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \color{blue}{\mathsf{neg.f64}\left(\mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right), 1\right)\right)\right)}\right) \]

4. Applied egg-rr 100.0%

   \[\leadsto \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{log1p.f64}\left(x\right)\right)\right)}\right)\right) \]
   Proof

   [Start] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{log.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right), 1\right)\right)\right)\right) \]
   /-rgt-identity [=>] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{log.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right)}\right)\right)\right) \]
   flip-- [=>] 8.3	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{log.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(1, 1\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{+.f64}\left(1, x\right)\right)}, \mathsf{+.f64}\left(1, x\right)\right)\right)\right)\right) \]
   associate-/l/ [=>] 8.3	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{log.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(1, 1\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right)\right)}\right)\right)\right) \]
   log-div [=>] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{log.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(1, 1\right), \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{log.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right)\right)\right)}\right)\right) \]
   metadata-eval [=>] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{log.f64}\left(\mathsf{\_.f64}\left(\color{blue}{1}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{log.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right)\right)\right)\right)\right) \]
   sub-neg [=>] 8.4	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{log.f64}\left(\color{blue}{\mathsf{+.f64}\left(1, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right)}\right), \mathsf{log.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right)\right)\right)\right)\right) \]
   log1p-def [=>] 8.7	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right)}, \mathsf{log.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(1, x\right)\right)\right)\right)\right)\right) \]
   pow2 [=>] 8.7	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{log.f64}\left(\color{blue}{\mathsf{pow.f64}\left(\mathsf{+.f64}\left(1, x\right), 2\right)}\right)\right)\right)\right) \]
   metadata-eval [<=] 8.7	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{log.f64}\left(\mathsf{pow.f64}\left(\mathsf{+.f64}\left(1, x\right), \color{blue}{\mathsf{+.f64}\left(1, 1\right)}\right)\right)\right)\right)\right) \]
   log-pow [=>] 8.7	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, 1\right), \mathsf{log.f64}\left(\mathsf{+.f64}\left(1, x\right)\right)\right)}\right)\right)\right) \]
   metadata-eval [=>] 8.7	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\color{blue}{2}, \mathsf{log.f64}\left(\mathsf{+.f64}\left(1, x\right)\right)\right)\right)\right)\right) \]
   log1p-udef [<=] 100.0	\[ \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(2, \color{blue}{\mathsf{log1p.f64}\left(x\right)}\right)\right)\right)\right) \]

5. Final simplification 100.0%

   \[\leadsto \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{log1p.f64}\left(x\right)\right), \mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right) \]

Alternatives

Alternative 1
Accuracy	100.0%
Cost	13184

\[\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{\_.f64}\left(\mathsf{log1p.f64}\left(x\right), \mathsf{log1p.f64}\left(\mathsf{neg.f64}\left(x\right)\right)\right)\right) \]

Alternative 2
Accuracy	99.5%
Cost	7040

\[\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, 2\right), \mathsf{*.f64}\left(\frac{2}{3}, \mathsf{pow.f64}\left(x, 3\right)\right)\right)\right) \]

Alternative 3
Accuracy	99.1%
Cost	320

\[\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, 2\right)\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (x)
  :name "Hyperbolic arc-(co)tangent"
  :precision binary64
  (* (/ 1.0 2.0) (log (/ (+ 1.0 x) (- 1.0 x)))))