?

Average Accuracy: 35.4% → 99.9%
Time: 2.7s
Precision: binary64
Cost: 12992

?

\[\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{*.f64}\left(2, x\right)\right), 1\right), \mathsf{\_.f64}\left(\mathsf{exp.f64}\left(x\right), 1\right)\right)\right) \]
↓
\[\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(x\right)\right)\right) \]
(FPCore (x)
 :precision binary64
 (sqrt.f64 (/.f64 (-.f64 (exp.f64 (*.f64 2 x)) 1) (-.f64 (exp.f64 x) 1))))
↓
(FPCore (x) :precision binary64 (sqrt.f64 (+.f64 1 (exp.f64 x))))
\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{*.f64}\left(2, x\right)\right), 1\right), \mathsf{\_.f64}\left(\mathsf{exp.f64}\left(x\right), 1\right)\right)\right)
↓
\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(x\right)\right)\right)

Error?

Derivation?

  1. Initial program 35.4%

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

  2. Simplified99.9%

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

    [Start]35.4

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

    *-commutative [=>]35.4

    \[ \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(x, 2\right)}\right), 1\right), \mathsf{\_.f64}\left(\mathsf{exp.f64}\left(x\right), 1\right)\right)\right) \]

    exp-lft-sqr [=>]35.9

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

    difference-of-sqr-1 [=>]36.4

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

    associate-/l* [=>]36.4

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

    *-inverses [=>]99.9

    \[ \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(x\right), 1\right), \color{blue}{1}\right)\right) \]

    /-rgt-identity [=>]99.9

    \[ \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{exp.f64}\left(x\right), 1\right)}\right) \]

    +-commutative [=>]99.9

    \[ \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(x\right)\right)}\right) \]

  3. Final simplification99.9%

    \[\leadsto \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(x\right)\right)\right) \]

Reproduce?

herbie shell --seed 2023144 
(FPCore (x)
  :name "sqrtexp (problem 3.4.4)"
  :precision binary64
  (sqrt (/ (- (exp (* 2.0 x)) 1.0) (- (exp x) 1.0))))