Falkner and Boettcher, Appendix B, 2

?

Percentage Accurate: 100.0% → 100.0%
Time: 6.9s
Precision: binary64
Cost: 7232

?

\[\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{\left(v \cdot v\right) \cdot -0.375 + 0.125} \]
(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 (+ (* (* v v) -0.375) 0.125))))
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((((v * v) * -0.375) + 0.125));
}

real(8) function code(v)
    real(8), intent (in) :: v
    code = ((sqrt(2.0d0) / 4.0d0) * sqrt((1.0d0 - (3.0d0 * (v * v))))) * (1.0d0 - (v * v))
end function
↓
real(8) function code(v)
    real(8), intent (in) :: v
    code = (1.0d0 - (v * v)) * sqrt((((v * v) * (-0.375d0)) + 0.125d0))
end function

public static double code(double v) {
	return ((Math.sqrt(2.0) / 4.0) * Math.sqrt((1.0 - (3.0 * (v * v))))) * (1.0 - (v * v));
}
↓
public static double code(double v) {
	return (1.0 - (v * v)) * Math.sqrt((((v * v) * -0.375) + 0.125));
}

def code(v):
	return ((math.sqrt(2.0) / 4.0) * math.sqrt((1.0 - (3.0 * (v * v))))) * (1.0 - (v * v))
↓
def code(v):
	return (1.0 - (v * v)) * math.sqrt((((v * v) * -0.375) + 0.125))

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(Float64(Float64(v * v) * -0.375) + 0.125)))
end

function tmp = code(v)
	tmp = ((sqrt(2.0) / 4.0) * sqrt((1.0 - (3.0 * (v * v))))) * (1.0 - (v * v));
end
↓
function tmp = code(v)
	tmp = (1.0 - (v * v)) * sqrt((((v * v) * -0.375) + 0.125));
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[(N[(N[(v * v), $MachinePrecision] * -0.375), $MachinePrecision] + 0.125), $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{\left(v \cdot v\right) \cdot -0.375 + 0.125}

Local Percentage Accuracy?

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 6 alternatives:

AlternativeAccuracySpeedup

Accuracy vs Speed

The accuracy (vertical axis) and speed (horizontal axis) of each of Herbie's proposed alternatives. Up and to the right is better. Each dot represents an alternative program; the red square represents the initial program.

Bogosity?

Bogosity

Try it out?

Your Program's Arguments

Results

Enter valid numbers for all inputs

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}{\frac{\sqrt{2}}{4} \cdot \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)\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}}{4} \cdot \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)\right)} \]

  3. Applied egg-rr100.0%

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

    [Start]100.0

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

    add-sqr-sqrt [=>]98.5

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

    sqrt-unprod [=>]100.0

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

    *-commutative [=>]100.0

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

    *-commutative [=>]100.0

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

    swap-sqr [=>]100.0

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

  4. Simplified100.0%

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

    [Start]100.0

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

    associate-*l* [=>]100.0

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

    fma-udef [=>]100.0

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

    *-commutative [=>]100.0

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

    fma-def [=>]100.0

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

    *-commutative [=>]100.0

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

    fma-udef [=>]100.0

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

    +-commutative [=>]100.0

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

    distribute-rgt-neg-out [=>]100.0

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

    unsub-neg [=>]100.0

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

  5. Applied egg-rr100.0%

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

    [Start]100.0

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

    add-log-exp [=>]100.0

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

    *-un-lft-identity [=>]100.0

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

    log-prod [=>]100.0

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

    metadata-eval [=>]100.0

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

    add-log-exp [<=]100.0

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

    associate-*r* [=>]100.0

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

    sqrt-prod [=>]100.0

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

    fma-udef [=>]100.0

    \[ 0 + \sqrt{\color{blue}{\left(-3 \cdot \left(v \cdot v\right) + 1\right)} \cdot 0.125} \cdot \sqrt{{\left(1 - v \cdot v\right)}^{2}} \]

    associate-*r* [=>]100.0

    \[ 0 + \sqrt{\left(\color{blue}{\left(-3 \cdot v\right) \cdot v} + 1\right) \cdot 0.125} \cdot \sqrt{{\left(1 - v \cdot v\right)}^{2}} \]

    fma-def [=>]100.0

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

    unpow2 [=>]100.0

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

    sqrt-prod [=>]100.0

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

    add-sqr-sqrt [<=]100.0

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

  6. Simplified100.0%

    \[\leadsto \color{blue}{\left(1 - v \cdot v\right) \cdot \sqrt{-0.375 \cdot \left(v \cdot v\right) + 0.125}} \]
    Step-by-step derivation

    [Start]100.0

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

    +-lft-identity [=>]100.0

    \[ \color{blue}{\sqrt{\mathsf{fma}\left(-3 \cdot v, v, 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(-3 \cdot v, v, 1\right) \cdot 0.125}} \]

    *-commutative [=>]100.0

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

    fma-udef [=>]100.0

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

    distribute-lft-in [=>]100.0

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

    *-commutative [<=]100.0

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

    *-commutative [=>]100.0

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

    associate-*l* [<=]100.0

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

    unpow2 [<=]100.0

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

    *-commutative [=>]100.0

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

    associate-*r* [=>]100.0

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

    metadata-eval [=>]100.0

    \[ \left(1 - v \cdot v\right) \cdot \sqrt{\color{blue}{-0.375} \cdot {v}^{2} + 0.125 \cdot 1} \]

    unpow2 [=>]100.0

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

    metadata-eval [=>]100.0

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

  7. Final simplification100.0%

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

Alternatives

Alternative 1
Accuracy99.6%
Cost7104
\[\frac{\sqrt{2}}{4} \cdot \left(1 + \left(v \cdot v\right) \cdot -2.5\right) \]
Alternative 2
Accuracy99.6%
Cost7104
\[\frac{\sqrt{2}}{4} \cdot \left(1 + v \cdot \left(v \cdot -2.5\right)\right) \]
Alternative 3
Accuracy99.1%
Cost6848
\[\left(1 - v \cdot v\right) \cdot \sqrt{0.125} \]
Alternative 4
Accuracy99.1%
Cost6848
\[\sqrt{\left(v \cdot v\right) \cdot -0.375 + 0.125} \]
Alternative 5
Accuracy99.0%
Cost6464
\[\sqrt{0.125} \]

Reproduce?

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