Ian Simplification

Average Error: 93.01% → 91.52%

Time: 16.6s

Precision: binary64

Cost: 26368

Math

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

↓

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

FPCore

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

↓

(FPCore (x)
 :precision binary64
 (- (* PI -0.5) (* -2.0 (acos (exp (* (log1p (+ -0.5 (* -0.5 x))) 0.5))))))

C

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

↓

double code(double x) {
	return (((double) M_PI) * -0.5) - (-2.0 * acos(exp((log1p((-0.5 + (-0.5 * x))) * 0.5))));
}

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) {
	return (Math.PI * -0.5) - (-2.0 * Math.acos(Math.exp((Math.log1p((-0.5 + (-0.5 * x))) * 0.5))));
}

Python

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

↓

def code(x):
	return (math.pi * -0.5) - (-2.0 * math.acos(math.exp((math.log1p((-0.5 + (-0.5 * x))) * 0.5))))

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)
	return Float64(Float64(pi * -0.5) - Float64(-2.0 * acos(exp(Float64(log1p(Float64(-0.5 + Float64(-0.5 * x))) * 0.5)))))
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_] := N[(N[(Pi * -0.5), $MachinePrecision] - N[(-2.0 * N[ArcCos[N[Exp[N[(N[Log[1 + N[(-0.5 + N[(-0.5 * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * 0.5), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Target

Original	93.01%
Target	0%
Herbie	91.52%

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

Derivation

1. Initial program 93.01

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

2. Applied egg-rr 91.52

   \[\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.52

   \[\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.52

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

   [Start] 91.52	\[ 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.52	\[ \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.52	\[ \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.52	\[ \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) \]
   cancel-sign-sub-inv [=>] 91.52	\[ \color{blue}{\pi \cdot 0.5 + \left(-2\right) \cdot \left(0.5 \cdot \pi - \cos^{-1} \left(\sqrt{0.5 + -0.5 \cdot x}\right)\right)} \]
   metadata-eval [=>] 91.52	\[ \pi \cdot 0.5 + \color{blue}{-2} \cdot \left(0.5 \cdot \pi - \cos^{-1} \left(\sqrt{0.5 + -0.5 \cdot x}\right)\right) \]
   *-commutative [<=] 91.52	\[ \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.52	\[ \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.52	\[ \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.52	\[ \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.52	\[ \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.52	\[ \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) \]

5. Applied egg-rr 91.52

   \[\leadsto \pi \cdot -0.5 - -2 \cdot \cos^{-1} \color{blue}{\left(e^{\log \left(\mathsf{fma}\left(-0.5, x, 0.5\right)\right) \cdot 0.5}\right)} \]

6. Applied egg-rr 91.52

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

7. Final simplification 91.52

   \[\leadsto \pi \cdot -0.5 - -2 \cdot \cos^{-1} \left(e^{\mathsf{log1p}\left(-0.5 + -0.5 \cdot x\right) \cdot 0.5}\right) \]

Alternatives

Alternative 1
Error	91.52%
Cost	19840

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

Alternative 2
Error	94.63%
Cost	19584

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

Reproduce

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

  :herbie-target
  (asin x)

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