Hyperbolic arc-(co)secant

Average Accuracy: 100.0% → 100.0%

Time: 4.6s

Precision: binary64

Cost: 13376

Math

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

↓

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

FPCore

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

↓

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

Derivation

1. Initial program 100.0%

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

2. Applied egg-rr 99.9%

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

   [Start] 100.0	\[ \mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), x\right)\right)\right) \]
   expm1-log1p-u [=>] 99.9	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{expm1.f64}\left(\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), x\right)\right)\right)\right)}\right) \]
   expm1-udef [=>] 99.9	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), x\right)\right)\right)\right), 1\right)}\right) \]
   *-un-lft-identity [=>] 99.9	\[ \mathsf{log.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(1, \mathsf{/.f64}\left(1, x\right)\right)}, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), x\right)\right)\right)\right), 1\right)\right) \]
   div-inv [=>] 99.9	\[ \mathsf{log.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(1, \mathsf{/.f64}\left(1, x\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{/.f64}\left(1, x\right)\right)}\right)\right)\right), 1\right)\right) \]
   distribute-rgt-out [=>] 99.9	\[ \mathsf{log.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log1p.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{+.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)}\right)\right), 1\right)\right) \]

3. Simplified 100.0%

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

   [Start] 99.9	\[ \mathsf{log.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log1p.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{+.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right)\right), 1\right)\right) \]
   expm1-def [=>] 99.9	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{expm1.f64}\left(\mathsf{log1p.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{+.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right)\right)}\right) \]
   expm1-log1p [=>] 100.0	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{+.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)}\right) \]
   +-commutative [<=] 100.0	\[ \mathsf{log.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), 1\right)}\right)\right) \]
   associate-*l/ [=>] 100.0	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(1, \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), 1\right)\right), x\right)}\right) \]
   *-lft-identity [=>] 100.0	\[ \mathsf{log.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right), 1\right)}, x\right)\right) \]
   +-commutative [=>] 100.0	\[ \mathsf{log.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)}, x\right)\right) \]

4. Final simplification 100.0%

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

Alternatives

Alternative 1
Accuracy	99.5%
Cost	6976

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

Alternative 2
Accuracy	99.2%
Cost	6656

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

Alternative 3
Accuracy	99.1%
Cost	6592

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

Reproduce

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