ENA, Section 1.4, Exercise 1

Average Error: 3.5 → 3.5

Time: 11.9s

Precision: binary64

Cost: 67520

\[1.99 \leq x \land x \leq 2.01\]

Math

\[\cos x \cdot e^{10 \cdot \left(x \cdot x\right)} \]

↓

\[\begin{array}{l} t_0 := e^{10 \cdot \left(x \cdot x\right)}\\ t_1 := t_0 \cdot \frac{1}{t_0}\\ \left(\frac{1}{t_1 \cdot \left(t_1 \cdot t_0\right)} \cdot \left(\cos x \cdot t_0\right)\right) \cdot \left(t_0 \cdot \frac{\cos x}{\cos x}\right) - 0 \end{array} \]

FPCore

(FPCore (x) :precision binary64 (* (cos x) (exp (* 10.0 (* x x)))))

↓

(FPCore (x)
 :precision binary64
 (let* ((t_0 (exp (* 10.0 (* x x)))) (t_1 (* t_0 (/ 1.0 t_0))))
   (-
    (*
     (* (/ 1.0 (* t_1 (* t_1 t_0))) (* (cos x) t_0))
     (* t_0 (/ (cos x) (cos x))))
    0.0)))

C

double code(double x) {
	return cos(x) * exp((10.0 * (x * x)));
}

↓

double code(double x) {
	double t_0 = exp((10.0 * (x * x)));
	double t_1 = t_0 * (1.0 / t_0);
	return (((1.0 / (t_1 * (t_1 * t_0))) * (cos(x) * t_0)) * (t_0 * (cos(x) / cos(x)))) - 0.0;
}

Fortran

real(8) function code(x)
    real(8), intent (in) :: x
    code = cos(x) * exp((10.0d0 * (x * x)))
end function

↓

real(8) function code(x)
    real(8), intent (in) :: x
    real(8) :: t_0
    real(8) :: t_1
    t_0 = exp((10.0d0 * (x * x)))
    t_1 = t_0 * (1.0d0 / t_0)
    code = (((1.0d0 / (t_1 * (t_1 * t_0))) * (cos(x) * t_0)) * (t_0 * (cos(x) / cos(x)))) - 0.0d0
end function

Java

public static double code(double x) {
	return Math.cos(x) * Math.exp((10.0 * (x * x)));
}

↓

public static double code(double x) {
	double t_0 = Math.exp((10.0 * (x * x)));
	double t_1 = t_0 * (1.0 / t_0);
	return (((1.0 / (t_1 * (t_1 * t_0))) * (Math.cos(x) * t_0)) * (t_0 * (Math.cos(x) / Math.cos(x)))) - 0.0;
}

Python

def code(x):
	return math.cos(x) * math.exp((10.0 * (x * x)))

↓

def code(x):
	t_0 = math.exp((10.0 * (x * x)))
	t_1 = t_0 * (1.0 / t_0)
	return (((1.0 / (t_1 * (t_1 * t_0))) * (math.cos(x) * t_0)) * (t_0 * (math.cos(x) / math.cos(x)))) - 0.0

Julia

function code(x)
	return Float64(cos(x) * exp(Float64(10.0 * Float64(x * x))))
end

↓

function code(x)
	t_0 = exp(Float64(10.0 * Float64(x * x)))
	t_1 = Float64(t_0 * Float64(1.0 / t_0))
	return Float64(Float64(Float64(Float64(1.0 / Float64(t_1 * Float64(t_1 * t_0))) * Float64(cos(x) * t_0)) * Float64(t_0 * Float64(cos(x) / cos(x)))) - 0.0)
end

MATLAB

function tmp = code(x)
	tmp = cos(x) * exp((10.0 * (x * x)));
end

↓

function tmp = code(x)
	t_0 = exp((10.0 * (x * x)));
	t_1 = t_0 * (1.0 / t_0);
	tmp = (((1.0 / (t_1 * (t_1 * t_0))) * (cos(x) * t_0)) * (t_0 * (cos(x) / cos(x)))) - 0.0;
end

Wolfram

code[x_] := N[(N[Cos[x], $MachinePrecision] * N[Exp[N[(10.0 * N[(x * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

↓

code[x_] := Block[{t$95$0 = N[Exp[N[(10.0 * N[(x * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 * N[(1.0 / t$95$0), $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(N[(1.0 / N[(t$95$1 * N[(t$95$1 * t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(N[Cos[x], $MachinePrecision] * t$95$0), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 * N[(N[Cos[x], $MachinePrecision] / N[Cos[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 0.0), $MachinePrecision]]]

Derivation

1. Initial program 3.5

   \[\cos x \cdot e^{10 \cdot \left(x \cdot x\right)} \]

2. Simplified 3.6

   \[\leadsto \color{blue}{\cos x \cdot e^{x \cdot \left(x \cdot 10\right)}} \]
   Proof

   [Start] 3.5	\[ \cos x \cdot e^{10 \cdot \left(x \cdot x\right)} \]
   rational_best_oopsla_all_46_json_45_simplify-7 [=>] 3.6	\[ \cos x \cdot e^{\color{blue}{x \cdot \left(10 \cdot x\right)}} \]
   rational_best_oopsla_all_46_json_45_simplify-74 [=>] 3.6	\[ \cos x \cdot e^{x \cdot \color{blue}{\left(x \cdot 10\right)}} \]

3. Applied egg-rr 3.6

   \[\leadsto \cos x \cdot \color{blue}{\left(\left(e^{x \cdot \left(x \cdot 10\right)} \cdot \frac{1}{e^{x \cdot \left(x \cdot 10\right)}}\right) \cdot e^{x \cdot \left(x \cdot 10\right)}\right)} \]

4. Applied egg-rr 3.5

   \[\leadsto \color{blue}{\left(\frac{1}{e^{10 \cdot \left(x \cdot x\right)}} \cdot \left(\cos x \cdot e^{10 \cdot \left(x \cdot x\right)}\right)\right) \cdot \left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{\cos x}{\cos x}\right) - 0} \]

5. Applied egg-rr 3.5

   \[\leadsto \left(\frac{1}{\color{blue}{\left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{1}{e^{10 \cdot \left(x \cdot x\right)}}\right) \cdot e^{10 \cdot \left(x \cdot x\right)}}} \cdot \left(\cos x \cdot e^{10 \cdot \left(x \cdot x\right)}\right)\right) \cdot \left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{\cos x}{\cos x}\right) - 0 \]

6. Applied egg-rr 3.5

   \[\leadsto \left(\frac{1}{\left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{1}{e^{10 \cdot \left(x \cdot x\right)}}\right) \cdot \color{blue}{\left(\left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{1}{e^{10 \cdot \left(x \cdot x\right)}}\right) \cdot e^{10 \cdot \left(x \cdot x\right)}\right)}} \cdot \left(\cos x \cdot e^{10 \cdot \left(x \cdot x\right)}\right)\right) \cdot \left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{\cos x}{\cos x}\right) - 0 \]

7. Final simplification 3.5

   \[\leadsto \left(\frac{1}{\left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{1}{e^{10 \cdot \left(x \cdot x\right)}}\right) \cdot \left(\left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{1}{e^{10 \cdot \left(x \cdot x\right)}}\right) \cdot e^{10 \cdot \left(x \cdot x\right)}\right)} \cdot \left(\cos x \cdot e^{10 \cdot \left(x \cdot x\right)}\right)\right) \cdot \left(e^{10 \cdot \left(x \cdot x\right)} \cdot \frac{\cos x}{\cos x}\right) - 0 \]

Alternatives

Alternative 1
Error	3.5
Cost	53824

\[\begin{array}{l} t_0 := e^{10 \cdot \left(x \cdot x\right)}\\ \left(\frac{1}{\left(t_0 \cdot \frac{1}{t_0}\right) \cdot t_0} \cdot \left(\cos x \cdot t_0\right)\right) \cdot \left(t_0 \cdot \frac{\cos x}{\cos x}\right) - 0 \end{array} \]

Alternative 2
Error	3.5
Cost	40128

\[\begin{array}{l} t_0 := e^{x \cdot \left(x \cdot 10\right)}\\ \left(\frac{1}{t_0} \cdot \left(\cos x \cdot e^{10 \cdot \left(x \cdot x\right)}\right)\right) \cdot \left(t_0 \cdot \frac{\cos x}{\cos x}\right) - 0 \end{array} \]

Alternative 3
Error	3.5
Cost	27072

\[\begin{array}{l} t_0 := e^{10 \cdot \left(x \cdot x\right)}\\ t_0 \cdot \left(\frac{1}{t_0} \cdot \left(\cos x \cdot t_0\right)\right) - 0 \end{array} \]

Alternative 4
Error	3.5
Cost	26944

\[\begin{array}{l} t_0 := e^{x \cdot \left(x \cdot 10\right)}\\ \cos x \cdot \left(\left(t_0 \cdot \frac{1}{t_0}\right) \cdot e^{10 \cdot \left(x \cdot x\right)}\right) \end{array} \]

Alternative 5
Error	3.5
Cost	13248

\[\cos x \cdot e^{10 \cdot \left(x \cdot x\right)} \]

Alternative 6
Error	57.8
Cost	6592

\[\cos x \cdot 1 \]

Alternative 7
Error	63.0
Cost	64

\[1 \]

Reproduce

herbie shell --seed 2023090 
(FPCore (x)
  :name "ENA, Section 1.4, Exercise 1"
  :precision binary64
  :pre (and (<= 1.99 x) (<= x 2.01))
  (* (cos x) (exp (* 10.0 (* x x)))))