Falkner and Boettcher, Appendix B, 2

Average Error: 0.0 → 0.0

Time: 5.3s

Precision: binary64

Cost: 26432

Math

\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right) \]

↓

\[\sqrt{\mathsf{fma}\left(v, v \cdot -3, 1\right)} \cdot \left(\sqrt{2} \cdot \left(\mathsf{fma}\left(v, v, -1\right) \cdot -0.25\right)\right) \]

FPCore

(FPCore (v)
 :precision binary64
 (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))

↓

(FPCore (v)
 :precision binary64
 (* (sqrt (fma v (* v -3.0) 1.0)) (* (sqrt 2.0) (* (fma v v -1.0) -0.25))))

C

double code(double v) {
	return ((sqrt(2.0) / 4.0) * sqrt((1.0 - (3.0 * (v * v))))) * (1.0 - (v * v));
}

↓

double code(double v) {
	return sqrt(fma(v, (v * -3.0), 1.0)) * (sqrt(2.0) * (fma(v, v, -1.0) * -0.25));
}

Julia

function code(v)
	return Float64(Float64(Float64(sqrt(2.0) / 4.0) * sqrt(Float64(1.0 - Float64(3.0 * Float64(v * v))))) * Float64(1.0 - Float64(v * v)))
end

↓

function code(v)
	return Float64(sqrt(fma(v, Float64(v * -3.0), 1.0)) * Float64(sqrt(2.0) * Float64(fma(v, v, -1.0) * -0.25)))
end

Wolfram

code[v_] := N[(N[(N[(N[Sqrt[2.0], $MachinePrecision] / 4.0), $MachinePrecision] * N[Sqrt[N[(1.0 - N[(3.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[v_] := N[(N[Sqrt[N[(v * N[(v * -3.0), $MachinePrecision] + 1.0), $MachinePrecision]], $MachinePrecision] * N[(N[Sqrt[2.0], $MachinePrecision] * N[(N[(v * v + -1.0), $MachinePrecision] * -0.25), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 0.0

   \[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right) \]

2. Simplified 0.0

   \[\leadsto \color{blue}{\sqrt{\mathsf{fma}\left(v, v \cdot -3, 1\right)} \cdot \left(\sqrt{2} \cdot \left(\mathsf{fma}\left(v, v, -1\right) \cdot -0.25\right)\right)} \]
   Proof
   (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v -3) 1)) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v (Rewrite<= metadata-eval (neg.f64 3))) 1)) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (fma.f64 v (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 v 3))) 1)) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (fma.f64 v (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 3 v))) 1)) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 v (neg.f64 (*.f64 3 v))) 1))) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 v (*.f64 3 v)))) 1)) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 3 v) v))) 1)) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (+.f64 (neg.f64 (Rewrite<= associate-*r*_binary64 (*.f64 3 (*.f64 v v)))) 1)) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 1 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (neg.f64 (*.f64 3 (*.f64 v v)))))) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 (*.f64 3 (*.f64 v v))))) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v -1) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (*.f64 (fma.f64 v v (Rewrite<= metadata-eval (neg.f64 1))) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 v v) 1)) -1/4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (*.f64 (-.f64 (*.f64 v v) 1) (Rewrite<= metadata-eval (/.f64 -1 4))))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 -1 4) (-.f64 (*.f64 v v) 1))))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 (-.f64 (*.f64 v v) 1)))))): 0 points increase in error, 1 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (-.f64 (*.f64 v v) 1)) 4)))): 1 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 (*.f64 v v) 1))) 4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (*.f64 v v) 1))) 4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (*.f64 v v)) 1)) 4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (*.f64 v v))) 1) 4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (neg.f64 (*.f64 v v)))) 4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (*.f64 (sqrt.f64 2) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 (*.f64 v v))) 4))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 1 (*.f64 v v)) 4) (sqrt.f64 2)))): 0 points increase in error, 0 points decrease in error
   (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 1 (*.f64 v v)) (/.f64 4 (sqrt.f64 2))))): 0 points increase in error, 0 points decrease in error
   (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (-.f64 1 (*.f64 v v))) (/.f64 4 (sqrt.f64 2)))): 2 points increase in error, 0 points decrease in error
   (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (/.f64 4 (sqrt.f64 2))) (-.f64 1 (*.f64 v v)))): 0 points increase in error, 1 points decrease in error
   (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (sqrt.f64 2)) 4)) (-.f64 1 (*.f64 v v))): 0 points increase in error, 0 points decrease in error
   (*.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))) (/.f64 (sqrt.f64 2) 4))) (-.f64 1 (*.f64 v v))): 0 points increase in error, 0 points decrease in error
   (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (sqrt.f64 2) 4) (sqrt.f64 (-.f64 1 (*.f64 3 (*.f64 v v)))))) (-.f64 1 (*.f64 v v))): 0 points increase in error, 0 points decrease in error

3. Final simplification 0.0

   \[\leadsto \sqrt{\mathsf{fma}\left(v, v \cdot -3, 1\right)} \cdot \left(\sqrt{2} \cdot \left(\mathsf{fma}\left(v, v, -1\right) \cdot -0.25\right)\right) \]

Alternatives

Alternative 1
Error	0.0
Cost	7360

\[\sqrt{\left(1 + v \cdot \left(v \cdot -3\right)\right) \cdot 0.125} \cdot \left(1 - v \cdot v\right) \]

Alternative 2
Error	0.3
Cost	6976

\[\left(1 + v \cdot \left(v \cdot -2.5\right)\right) \cdot \sqrt{0.125} \]

Alternative 3
Error	0.6
Cost	6848

\[\left(1 - v \cdot v\right) \cdot \sqrt{0.125} \]

Alternative 4
Error	0.7
Cost	6464

\[\sqrt{0.125} \]

Reproduce

herbie shell --seed 2022300 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  :precision binary64
  (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))