Ian Simplification

Average Error: 93.21% → 91.72%

Time: 23.3s

Precision: binary64

Cost: 196672

Math

\[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

↓

\[\begin{array}{l} t_0 := \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)\\ t_1 := 8 \cdot {t_0}^{3}\\ \frac{\left({t_1}^{3} + {\left(-0.125 \cdot {\pi}^{3}\right)}^{3}\right) \cdot \frac{1}{4 \cdot {t_0}^{2} + \left(-0.5 \cdot \pi\right) \cdot \left(-0.5 \cdot \pi + t_0 \cdot -2\right)}}{t_1 \cdot t_1 + \left(\log \left({\left(e^{0.015625}\right)}^{\left({\pi}^{6}\right)}\right) + t_1 \cdot \left({\pi}^{3} \cdot 0.125\right)\right)} \end{array} \]

FPCore

(FPCore (x)
 :precision binary64
 (- (/ PI 2.0) (* 2.0 (asin (sqrt (/ (- 1.0 x) 2.0))))))

↓

(FPCore (x)
 :precision binary64
 (let* ((t_0 (acos (sqrt (- 0.5 (* 0.5 x))))) (t_1 (* 8.0 (pow t_0 3.0))))
   (/
    (*
     (+ (pow t_1 3.0) (pow (* -0.125 (pow PI 3.0)) 3.0))
     (/
      1.0
      (+ (* 4.0 (pow t_0 2.0)) (* (* -0.5 PI) (+ (* -0.5 PI) (* t_0 -2.0))))))
    (+
     (* t_1 t_1)
     (+
      (log (pow (exp 0.015625) (pow PI 6.0)))
      (* t_1 (* (pow PI 3.0) 0.125)))))))

C

double code(double x) {
	return (((double) M_PI) / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
}

↓

double code(double x) {
	double t_0 = acos(sqrt((0.5 - (0.5 * x))));
	double t_1 = 8.0 * pow(t_0, 3.0);
	return ((pow(t_1, 3.0) + pow((-0.125 * pow(((double) M_PI), 3.0)), 3.0)) * (1.0 / ((4.0 * pow(t_0, 2.0)) + ((-0.5 * ((double) M_PI)) * ((-0.5 * ((double) M_PI)) + (t_0 * -2.0)))))) / ((t_1 * t_1) + (log(pow(exp(0.015625), pow(((double) M_PI), 6.0))) + (t_1 * (pow(((double) M_PI), 3.0) * 0.125))));
}

Java

public static double code(double x) {
	return (Math.PI / 2.0) - (2.0 * Math.asin(Math.sqrt(((1.0 - x) / 2.0))));
}

↓

public static double code(double x) {
	double t_0 = Math.acos(Math.sqrt((0.5 - (0.5 * x))));
	double t_1 = 8.0 * Math.pow(t_0, 3.0);
	return ((Math.pow(t_1, 3.0) + Math.pow((-0.125 * Math.pow(Math.PI, 3.0)), 3.0)) * (1.0 / ((4.0 * Math.pow(t_0, 2.0)) + ((-0.5 * Math.PI) * ((-0.5 * Math.PI) + (t_0 * -2.0)))))) / ((t_1 * t_1) + (Math.log(Math.pow(Math.exp(0.015625), Math.pow(Math.PI, 6.0))) + (t_1 * (Math.pow(Math.PI, 3.0) * 0.125))));
}

Python

def code(x):
	return (math.pi / 2.0) - (2.0 * math.asin(math.sqrt(((1.0 - x) / 2.0))))

↓

def code(x):
	t_0 = math.acos(math.sqrt((0.5 - (0.5 * x))))
	t_1 = 8.0 * math.pow(t_0, 3.0)
	return ((math.pow(t_1, 3.0) + math.pow((-0.125 * math.pow(math.pi, 3.0)), 3.0)) * (1.0 / ((4.0 * math.pow(t_0, 2.0)) + ((-0.5 * math.pi) * ((-0.5 * math.pi) + (t_0 * -2.0)))))) / ((t_1 * t_1) + (math.log(math.pow(math.exp(0.015625), math.pow(math.pi, 6.0))) + (t_1 * (math.pow(math.pi, 3.0) * 0.125))))

Julia

function code(x)
	return Float64(Float64(pi / 2.0) - Float64(2.0 * asin(sqrt(Float64(Float64(1.0 - x) / 2.0)))))
end

↓

function code(x)
	t_0 = acos(sqrt(Float64(0.5 - Float64(0.5 * x))))
	t_1 = Float64(8.0 * (t_0 ^ 3.0))
	return Float64(Float64(Float64((t_1 ^ 3.0) + (Float64(-0.125 * (pi ^ 3.0)) ^ 3.0)) * Float64(1.0 / Float64(Float64(4.0 * (t_0 ^ 2.0)) + Float64(Float64(-0.5 * pi) * Float64(Float64(-0.5 * pi) + Float64(t_0 * -2.0)))))) / Float64(Float64(t_1 * t_1) + Float64(log((exp(0.015625) ^ (pi ^ 6.0))) + Float64(t_1 * Float64((pi ^ 3.0) * 0.125)))))
end

MATLAB

function tmp = code(x)
	tmp = (pi / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
end

↓

function tmp = code(x)
	t_0 = acos(sqrt((0.5 - (0.5 * x))));
	t_1 = 8.0 * (t_0 ^ 3.0);
	tmp = (((t_1 ^ 3.0) + ((-0.125 * (pi ^ 3.0)) ^ 3.0)) * (1.0 / ((4.0 * (t_0 ^ 2.0)) + ((-0.5 * pi) * ((-0.5 * pi) + (t_0 * -2.0)))))) / ((t_1 * t_1) + (log((exp(0.015625) ^ (pi ^ 6.0))) + (t_1 * ((pi ^ 3.0) * 0.125))));
end

Wolfram

code[x_] := N[(N[(Pi / 2.0), $MachinePrecision] - N[(2.0 * N[ArcSin[N[Sqrt[N[(N[(1.0 - x), $MachinePrecision] / 2.0), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[x_] := Block[{t$95$0 = N[ArcCos[N[Sqrt[N[(0.5 - N[(0.5 * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[(8.0 * N[Power[t$95$0, 3.0], $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(N[Power[t$95$1, 3.0], $MachinePrecision] + N[Power[N[(-0.125 * N[Power[Pi, 3.0], $MachinePrecision]), $MachinePrecision], 3.0], $MachinePrecision]), $MachinePrecision] * N[(1.0 / N[(N[(4.0 * N[Power[t$95$0, 2.0], $MachinePrecision]), $MachinePrecision] + N[(N[(-0.5 * Pi), $MachinePrecision] * N[(N[(-0.5 * Pi), $MachinePrecision] + N[(t$95$0 * -2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(t$95$1 * t$95$1), $MachinePrecision] + N[(N[Log[N[Power[N[Exp[0.015625], $MachinePrecision], N[Power[Pi, 6.0], $MachinePrecision]], $MachinePrecision]], $MachinePrecision] + N[(t$95$1 * N[(N[Power[Pi, 3.0], $MachinePrecision] * 0.125), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]

Target

Original	93.21%
Target	0%
Herbie	91.72%

\[\sin^{-1} x \]

Derivation

1. Initial program 93.21

   \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

2. Applied egg-rr 91.72

   \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\pi \cdot 0.5 - \cos^{-1} \left(\sqrt{0.5 - x \cdot 0.5}\right)\right)} \]

3. Taylor expanded in x around 0 91.72

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

4. Simplified 91.72

   \[\leadsto \color{blue}{2 \cdot \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right) + \pi \cdot -0.5} \]
   Proof

   [Start] 91.72	\[ 0.5 \cdot \pi - 2 \cdot \left(0.5 \cdot \pi - \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)\right) \]
   *-commutative [<=] 91.72	\[ \color{blue}{\pi \cdot 0.5} - 2 \cdot \left(0.5 \cdot \pi - \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)\right) \]
   cancel-sign-sub-inv [=>] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(0.5 \cdot \pi - \cos^{-1} \left(\sqrt{\color{blue}{0.5 + \left(-0.5\right) \cdot x}}\right)\right) \]
   metadata-eval [=>] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(0.5 \cdot \pi - \cos^{-1} \left(\sqrt{0.5 + \color{blue}{-0.5} \cdot x}\right)\right) \]
   *-commutative [<=] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(\color{blue}{\pi \cdot 0.5} - \cos^{-1} \left(\sqrt{0.5 + -0.5 \cdot x}\right)\right) \]
   metadata-eval [<=] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(\pi \cdot 0.5 - \cos^{-1} \left(\sqrt{0.5 + \color{blue}{\left(-0.5\right)} \cdot x}\right)\right) \]
   cancel-sign-sub-inv [<=] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(\pi \cdot 0.5 - \cos^{-1} \left(\sqrt{\color{blue}{0.5 - 0.5 \cdot x}}\right)\right) \]
   cancel-sign-sub-inv [=>] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(\pi \cdot 0.5 - \cos^{-1} \left(\sqrt{\color{blue}{0.5 + \left(-0.5\right) \cdot x}}\right)\right) \]
   metadata-eval [=>] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(\pi \cdot 0.5 - \cos^{-1} \left(\sqrt{0.5 + \color{blue}{-0.5} \cdot x}\right)\right) \]
   *-commutative [<=] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \left(\pi \cdot 0.5 - \cos^{-1} \left(\sqrt{0.5 + \color{blue}{x \cdot -0.5}}\right)\right) \]
   unsub-neg [<=] 91.72	\[ \pi \cdot 0.5 - 2 \cdot \color{blue}{\left(\pi \cdot 0.5 + \left(-\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)\right)\right)} \]

5. Applied egg-rr 91.72

   \[\leadsto \color{blue}{\frac{\left({\left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right)}^{3} + {\left(-0.125 \cdot {\pi}^{3}\right)}^{3}\right) \cdot \frac{1}{4 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{2} + \left(\pi \cdot -0.5\right) \cdot \left(\pi \cdot -0.5 - 2 \cdot \cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)\right)}}{\left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right) \cdot \left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right) + \left(\left(-0.125 \cdot {\pi}^{3}\right) \cdot \left(-0.125 \cdot {\pi}^{3}\right) - \left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right) \cdot \left(-0.125 \cdot {\pi}^{3}\right)\right)}} \]

6. Applied egg-rr 91.72

   \[\leadsto \frac{\left({\left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right)}^{3} + {\left(-0.125 \cdot {\pi}^{3}\right)}^{3}\right) \cdot \frac{1}{4 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{2} + \left(\pi \cdot -0.5\right) \cdot \left(\pi \cdot -0.5 - 2 \cdot \cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)\right)}}{\left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right) \cdot \left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right) + \left(\color{blue}{\log \left({\left(e^{0.015625}\right)}^{\left({\pi}^{6}\right)}\right)} - \left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 + x \cdot -0.5}\right)}^{3}\right) \cdot \left(-0.125 \cdot {\pi}^{3}\right)\right)} \]

7. Final simplification 91.72

   \[\leadsto \frac{\left({\left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)}^{3}\right)}^{3} + {\left(-0.125 \cdot {\pi}^{3}\right)}^{3}\right) \cdot \frac{1}{4 \cdot {\cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)}^{2} + \left(-0.5 \cdot \pi\right) \cdot \left(-0.5 \cdot \pi + \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right) \cdot -2\right)}}{\left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)}^{3}\right) \cdot \left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)}^{3}\right) + \left(\log \left({\left(e^{0.015625}\right)}^{\left({\pi}^{6}\right)}\right) + \left(8 \cdot {\cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)}^{3}\right) \cdot \left({\pi}^{3} \cdot 0.125\right)\right)} \]

Alternatives

Alternative 1
Error	91.72%
Cost	177536

\[\begin{array}{l} t_0 := \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)\\ t_1 := 8 \cdot {t_0}^{3}\\ \frac{\left({t_1}^{3} + {\left(-0.125 \cdot {\pi}^{3}\right)}^{3}\right) \cdot \frac{1}{4 \cdot {t_0}^{2} + \left(-0.5 \cdot \pi\right) \cdot \left(-0.5 \cdot \pi + t_0 \cdot -2\right)}}{t_1 \cdot t_1 + \left(0.015625 \cdot {\pi}^{6} + t_1 \cdot \left({\pi}^{3} \cdot 0.125\right)\right)} \end{array} \]

Alternative 2
Error	91.71%
Cost	163904

\[\begin{array}{l} t_0 := \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)\\ t_1 := \sqrt[3]{8 \cdot {t_0}^{3} + -0.125 \cdot {\pi}^{3}}\\ \frac{t_1 \cdot t_1}{\frac{4 \cdot {t_0}^{2} + \left(-0.5 \cdot \pi\right) \cdot \left(-0.5 \cdot \pi + t_0 \cdot -2\right)}{t_1}} \end{array} \]

Alternative 3
Error	91.71%
Cost	79040

\[\begin{array}{l} t_0 := \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right)\\ \frac{8 \cdot {t_0}^{3} + -0.125 \cdot {\pi}^{3}}{4 \cdot {t_0}^{2} + \left(-0.5 \cdot \pi\right) \cdot \left(-0.5 \cdot \pi + t_0 \cdot -2\right)} \end{array} \]

Alternative 4
Error	91.72%
Cost	19840

\[-0.5 \cdot \pi + \cos^{-1} \left(\sqrt{0.5 - 0.5 \cdot x}\right) \cdot 2 \]

Alternative 5
Error	94.61%
Cost	19584

\[-0.5 \cdot \pi + 2 \cdot \cos^{-1} \left(\sqrt{0.5}\right) \]

Reproduce

herbie shell --seed 2023088 
(FPCore (x)
  :name "Ian Simplification"
  :precision binary64

  :herbie-target
  (asin x)

  (- (/ PI 2.0) (* 2.0 (asin (sqrt (/ (- 1.0 x) 2.0))))))