Falkner and Boettcher, Appendix B, 2

?

Percentage Accurate: 100.0% → 100.0%
Time: 9.2s
Precision: binary64
Cost: 13632

?

\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right) \]
↓
\[\left(1 - v \cdot v\right) \cdot \sqrt{0.125 \cdot \mathsf{fma}\left(v \cdot v, -3, 1\right)} \]
(FPCore (v)
 :precision binary64
 (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))
↓
(FPCore (v)
 :precision binary64
 (* (- 1.0 (* v v)) (sqrt (* 0.125 (fma (* v v) -3.0 1.0)))))
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 (1.0 - (v * v)) * sqrt((0.125 * fma((v * v), -3.0, 1.0)));
}

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(Float64(1.0 - Float64(v * v)) * sqrt(Float64(0.125 * fma(Float64(v * v), -3.0, 1.0))))
end

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[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision] * N[Sqrt[N[(0.125 * N[(N[(v * v), $MachinePrecision] * -3.0 + 1.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\left(1 - v \cdot v\right) \cdot \sqrt{0.125 \cdot \mathsf{fma}\left(v \cdot v, -3, 1\right)}

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Herbie found 4 alternatives:

AlternativeAccuracySpeedup

Accuracy vs Speed

The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Bogosity?

Bogosity

Derivation?

  1. Initial program 100.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. Simplified100.0%

    \[\leadsto \color{blue}{\sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{-4}{\mathsf{fma}\left(v, v, -1\right)}}} \]
    Step-by-step derivation

    [Start]100.0%

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

    associate-*l/ [=>]100.0%

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

    associate-/r/ [<=]100.0%

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

    associate-*r/ [<=]100.0%

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

    sub-neg [=>]100.0%

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

    +-commutative [=>]100.0%

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

    *-commutative [=>]100.0%

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

    distribute-rgt-neg-in [=>]100.0%

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

    fma-def [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\color{blue}{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}}{\frac{4}{1 - v \cdot v}} \]

    metadata-eval [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, \color{blue}{-3}, 1\right)}}{\frac{4}{1 - v \cdot v}} \]

    sub-neg [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{4}{\color{blue}{1 + \left(-v \cdot v\right)}}} \]

    +-commutative [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{4}{\color{blue}{\left(-v \cdot v\right) + 1}}} \]

    neg-sub0 [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{4}{\color{blue}{\left(0 - v \cdot v\right)} + 1}} \]

    associate-+l- [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{4}{\color{blue}{0 - \left(v \cdot v - 1\right)}}} \]

    sub0-neg [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{4}{\color{blue}{-\left(v \cdot v - 1\right)}}} \]

    neg-mul-1 [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{4}{\color{blue}{-1 \cdot \left(v \cdot v - 1\right)}}} \]

    associate-/r* [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\color{blue}{\frac{\frac{4}{-1}}{v \cdot v - 1}}} \]

    metadata-eval [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{\color{blue}{-4}}{v \cdot v - 1}} \]

    fma-neg [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{-4}{\color{blue}{\mathsf{fma}\left(v, v, -1\right)}}} \]

    metadata-eval [=>]100.0%

    \[ \sqrt{2} \cdot \frac{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{-4}{\mathsf{fma}\left(v, v, \color{blue}{-1}\right)}} \]

  3. Applied egg-rr100.0%

    \[\leadsto \color{blue}{\frac{\left(\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)} \cdot \sqrt{0.125}\right) \cdot \left(1 - {v}^{4}\right)}{v \cdot v + 1}} \]
    Step-by-step derivation

    [Start]100.0%

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

    associate-*r/ [=>]100.0%

    \[ \color{blue}{\frac{\sqrt{2} \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{-4}{\mathsf{fma}\left(v, v, -1\right)}}} \]

    frac-2neg [=>]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\color{blue}{\frac{--4}{-\mathsf{fma}\left(v, v, -1\right)}}} \]

    metadata-eval [=>]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{\frac{\color{blue}{4}}{-\mathsf{fma}\left(v, v, -1\right)}} \]

    associate-/r/ [=>]100.0%

    \[ \color{blue}{\frac{\sqrt{2} \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}{4} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right)} \]

    fma-udef [=>]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\color{blue}{\left(v \cdot v\right) \cdot -3 + 1}}}{4} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right) \]

    metadata-eval [<=]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\left(v \cdot v\right) \cdot \color{blue}{\left(-3\right)} + 1}}{4} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right) \]

    distribute-rgt-neg-in [<=]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\color{blue}{\left(-\left(v \cdot v\right) \cdot 3\right)} + 1}}{4} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right) \]

    *-commutative [<=]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\left(-\color{blue}{3 \cdot \left(v \cdot v\right)}\right) + 1}}{4} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right) \]

    +-commutative [=>]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\color{blue}{1 + \left(-3 \cdot \left(v \cdot v\right)\right)}}}{4} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right) \]

    sub-neg [<=]100.0%

    \[ \frac{\sqrt{2} \cdot \sqrt{\color{blue}{1 - 3 \cdot \left(v \cdot v\right)}}}{4} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right) \]

    associate-*l/ [<=]100.0%

    \[ \color{blue}{\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)} \cdot \left(-\mathsf{fma}\left(v, v, -1\right)\right) \]

    fma-udef [=>]100.0%

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

    distribute-neg-in [=>]100.0%

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

    metadata-eval [=>]100.0%

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

    +-commutative [<=]100.0%

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

    sub-neg [<=]100.0%

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

  4. Applied egg-rr98.4%

    \[\leadsto \color{blue}{e^{\mathsf{log1p}\left(\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right) \cdot 0.125} \cdot \left(1 - v \cdot v\right)\right)} - 1} \]
    Step-by-step derivation

    [Start]100.0%

    \[ \frac{\left(\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)} \cdot \sqrt{0.125}\right) \cdot \left(1 - {v}^{4}\right)}{v \cdot v + 1} \]

    expm1-log1p-u [=>]100.0%

    \[ \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\left(\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)} \cdot \sqrt{0.125}\right) \cdot \left(1 - {v}^{4}\right)}{v \cdot v + 1}\right)\right)} \]

    expm1-udef [=>]98.4%

    \[ \color{blue}{e^{\mathsf{log1p}\left(\frac{\left(\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)} \cdot \sqrt{0.125}\right) \cdot \left(1 - {v}^{4}\right)}{v \cdot v + 1}\right)} - 1} \]

  5. Simplified100.0%

    \[\leadsto \color{blue}{\left(1 - v \cdot v\right) \cdot \sqrt{0.125 \cdot \mathsf{fma}\left(v \cdot v, -3, 1\right)}} \]
    Step-by-step derivation

    [Start]98.4%

    \[ e^{\mathsf{log1p}\left(\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right) \cdot 0.125} \cdot \left(1 - v \cdot v\right)\right)} - 1 \]

    expm1-def [=>]100.0%

    \[ \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right) \cdot 0.125} \cdot \left(1 - v \cdot v\right)\right)\right)} \]

    expm1-log1p [=>]100.0%

    \[ \color{blue}{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right) \cdot 0.125} \cdot \left(1 - v \cdot v\right)} \]

    *-commutative [=>]100.0%

    \[ \color{blue}{\left(1 - v \cdot v\right) \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right) \cdot 0.125}} \]

    *-commutative [=>]100.0%

    \[ \left(1 - v \cdot v\right) \cdot \sqrt{\color{blue}{0.125 \cdot \mathsf{fma}\left(v \cdot v, -3, 1\right)}} \]

  6. Final simplification100.0%

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

Alternatives

Alternative 1
Accuracy100.0%
Cost13632
\[\left(1 - v \cdot v\right) \cdot \sqrt{0.125 \cdot \mathsf{fma}\left(v \cdot v, -3, 1\right)} \]
Alternative 2
Accuracy99.5%
Cost7104
\[\frac{\sqrt{2}}{4} \cdot \left(1 + \left(v \cdot v\right) \cdot -2.5\right) \]
Alternative 3
Accuracy98.8%
Cost6848
\[\left(1 - v \cdot v\right) \cdot \sqrt{0.125} \]
Alternative 4
Accuracy98.8%
Cost6464
\[\sqrt{0.125} \]

Reproduce?

herbie shell --seed 2023263 
(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))))