ENA, Section 1.4, Mentioned, A

Percentage Accurate: 54.3% → 100.0%

Time: 3.8s

Precision: binary64

Cost: 320

\[-0.01 \leq x \land x \leq 0.01\]

Math

\[1 - \cos x \]

↓

\[x \cdot \frac{x}{2} \]

FPCore

(FPCore (x) :precision binary64 (- 1.0 (cos x)))

↓

(FPCore (x) :precision binary64 (* x (/ x 2.0)))

C

double code(double x) {
	return 1.0 - cos(x);
}

↓

double code(double x) {
	return x * (x / 2.0);
}

Fortran

real(8) function code(x)
    real(8), intent (in) :: x
    code = 1.0d0 - cos(x)
end function

↓

real(8) function code(x)
    real(8), intent (in) :: x
    code = x * (x / 2.0d0)
end function

Java

public static double code(double x) {
	return 1.0 - Math.cos(x);
}

↓

public static double code(double x) {
	return x * (x / 2.0);
}

Python

def code(x):
	return 1.0 - math.cos(x)

↓

def code(x):
	return x * (x / 2.0)

Julia

function code(x)
	return Float64(1.0 - cos(x))
end

↓

function code(x)
	return Float64(x * Float64(x / 2.0))
end

MATLAB

function tmp = code(x)
	tmp = 1.0 - cos(x);
end

↓

function tmp = code(x)
	tmp = x * (x / 2.0);
end

Wolfram

code[x_] := N[(1.0 - N[Cos[x], $MachinePrecision]), $MachinePrecision]

↓

code[x_] := N[(x * N[(x / 2.0), $MachinePrecision]), $MachinePrecision]

Target

Original	54.3%
Target	100.0%
Herbie	100.0%

\[\frac{\sin x \cdot \sin x}{1 + \cos x} \]

Derivation

1. Initial program 58.0%

   \[1 - \cos x \]

2. Taylor expanded in x around 0 100.0%

   \[\leadsto \color{blue}{0.5 \cdot {x}^{2}} \]

3. Simplified 100.0%

   \[\leadsto \color{blue}{0.5 \cdot \left(x \cdot x\right)} \]
   Step-by-step derivation

   [Start] 100.0%	\[ 0.5 \cdot {x}^{2} \]
   unpow2 [=>] 100.0%	\[ 0.5 \cdot \color{blue}{\left(x \cdot x\right)} \]

4. Applied egg-rr 99.4%

   \[\leadsto \color{blue}{{\left(x \cdot \sqrt{0.5}\right)}^{2}} \]
   Step-by-step derivation

   [Start] 100.0%	\[ 0.5 \cdot \left(x \cdot x\right) \]
   add-sqr-sqrt [=>] 99.6%	\[ \color{blue}{\sqrt{0.5 \cdot \left(x \cdot x\right)} \cdot \sqrt{0.5 \cdot \left(x \cdot x\right)}} \]
   pow2 [=>] 99.6%	\[ \color{blue}{{\left(\sqrt{0.5 \cdot \left(x \cdot x\right)}\right)}^{2}} \]
   *-commutative [=>] 99.6%	\[ {\left(\sqrt{\color{blue}{\left(x \cdot x\right) \cdot 0.5}}\right)}^{2} \]
   sqrt-prod [=>] 99.3%	\[ {\color{blue}{\left(\sqrt{x \cdot x} \cdot \sqrt{0.5}\right)}}^{2} \]
   sqrt-prod [=>] 46.9%	\[ {\left(\color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} \cdot \sqrt{0.5}\right)}^{2} \]
   add-sqr-sqrt [<=] 99.4%	\[ {\left(\color{blue}{x} \cdot \sqrt{0.5}\right)}^{2} \]

5. Taylor expanded in x around 0 99.1%

   \[\leadsto \color{blue}{{\left(\sqrt{0.5}\right)}^{2} \cdot {x}^{2}} \]

6. Simplified 100.0%

   \[\leadsto \color{blue}{\frac{x}{2} \cdot x} \]
   Step-by-step derivation

   [Start] 99.1%	\[ {\left(\sqrt{0.5}\right)}^{2} \cdot {x}^{2} \]
   unpow2 [=>] 99.1%	\[ \color{blue}{\left(\sqrt{0.5} \cdot \sqrt{0.5}\right)} \cdot {x}^{2} \]
   rem-square-sqrt [=>] 100.0%	\[ \color{blue}{0.5} \cdot {x}^{2} \]
   unpow2 [=>] 100.0%	\[ 0.5 \cdot \color{blue}{\left(x \cdot x\right)} \]
   rem-log-exp [<=] 58.0%	\[ 0.5 \cdot \color{blue}{\log \left(e^{x \cdot x}\right)} \]
   log-pow [<=] 58.0%	\[ \color{blue}{\log \left({\left(e^{x \cdot x}\right)}^{0.5}\right)} \]
   unpow1/2 [=>] 58.0%	\[ \log \color{blue}{\left(\sqrt{e^{x \cdot x}}\right)} \]
   exp-prod [=>] 58.0%	\[ \log \left(\sqrt{\color{blue}{{\left(e^{x}\right)}^{x}}}\right) \]
   sqr-pow [=>] 58.0%	\[ \log \left(\sqrt{\color{blue}{{\left(e^{x}\right)}^{\left(\frac{x}{2}\right)} \cdot {\left(e^{x}\right)}^{\left(\frac{x}{2}\right)}}}\right) \]
   rem-sqrt-square [=>] 58.0%	\[ \log \color{blue}{\left(\left|{\left(e^{x}\right)}^{\left(\frac{x}{2}\right)}\right|\right)} \]
   sqr-pow [=>] 58.0%	\[ \log \left(\left|\color{blue}{{\left(e^{x}\right)}^{\left(\frac{\frac{x}{2}}{2}\right)} \cdot {\left(e^{x}\right)}^{\left(\frac{\frac{x}{2}}{2}\right)}}\right|\right) \]
   fabs-sqr [=>] 58.0%	\[ \log \color{blue}{\left({\left(e^{x}\right)}^{\left(\frac{\frac{x}{2}}{2}\right)} \cdot {\left(e^{x}\right)}^{\left(\frac{\frac{x}{2}}{2}\right)}\right)} \]
   sqr-pow [<=] 58.0%	\[ \log \color{blue}{\left({\left(e^{x}\right)}^{\left(\frac{x}{2}\right)}\right)} \]
   log-pow [=>] 58.2%	\[ \color{blue}{\frac{x}{2} \cdot \log \left(e^{x}\right)} \]
   rem-log-exp [=>] 100.0%	\[ \frac{x}{2} \cdot \color{blue}{x} \]

7. Final simplification 100.0%

   \[\leadsto x \cdot \frac{x}{2} \]

Alternatives

Alternative 1
Accuracy	100.0%
Cost	320

\[x \cdot \frac{x}{2} \]

Alternative 2
Accuracy	100.0%
Cost	320

\[0.5 \cdot \left(x \cdot x\right) \]

Reproduce

herbie shell --seed 2023272 
(FPCore (x)
  :name "ENA, Section 1.4, Mentioned, A"
  :precision binary64
  :pre (and (<= -0.01 x) (<= x 0.01))

  :herbie-target
  (/ (* (sin x) (sin x)) (+ 1.0 (cos x)))

  (- 1.0 (cos x)))