Beckmann Sample, normalization factor

Average Error: 0.7 → 0.8

Time: 22.8s

Precision: binary32

Cost: 137280

\[\left(0 < cosTheta \land cosTheta < 0.9999\right) \land \left(-1 < c \land c < 1\right)\]

Math

\[\frac{1}{\left(1 + c\right) + \left(\frac{1}{\sqrt{\pi}} \cdot \frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta}\right) \cdot e^{\left(-cosTheta\right) \cdot cosTheta}} \]

↓

\[\begin{array}{l} t_0 := {\left(\sqrt{\pi}\right)}^{3}\\ t_1 := \sqrt{\frac{1}{\pi}}\\ t_2 := -t_1\\ t_3 := -1 - \left(t_2 + c\right)\\ t_4 := t_2 + \left(1 + c\right)\\ t_5 := {t_4}^{2} \cdot \left(-t_0\right) + t_1 \cdot \left(\pi \cdot -1.5\right)\\ cosTheta \cdot \sqrt{\pi} + \left(-\left(\pi \cdot \left({cosTheta}^{2} \cdot t_4\right) + \left(t_5 \cdot {cosTheta}^{3} + \left(\sqrt{\pi} \cdot \left(t_5 \cdot t_3\right) + \left(t_0 \cdot \left(\left(t_1 \cdot -1.5\right) \cdot t_3\right) + \pi \cdot \left(t_1 + t_1 \cdot -0.5\right)\right)\right) \cdot {cosTheta}^{4}\right)\right)\right) \end{array} \]

FPCore

(FPCore (cosTheta c)
 :precision binary32
 (/
  1.0
  (+
   (+ 1.0 c)
   (*
    (* (/ 1.0 (sqrt PI)) (/ (sqrt (- (- 1.0 cosTheta) cosTheta)) cosTheta))
    (exp (* (- cosTheta) cosTheta))))))

↓

(FPCore (cosTheta c)
 :precision binary32
 (let* ((t_0 (pow (sqrt PI) 3.0))
        (t_1 (sqrt (/ 1.0 PI)))
        (t_2 (- t_1))
        (t_3 (- -1.0 (+ t_2 c)))
        (t_4 (+ t_2 (+ 1.0 c)))
        (t_5 (+ (* (pow t_4 2.0) (- t_0)) (* t_1 (* PI -1.5)))))
   (+
    (* cosTheta (sqrt PI))
    (-
     (+
      (* PI (* (pow cosTheta 2.0) t_4))
      (+
       (* t_5 (pow cosTheta 3.0))
       (*
        (+
         (* (sqrt PI) (* t_5 t_3))
         (+ (* t_0 (* (* t_1 -1.5) t_3)) (* PI (+ t_1 (* t_1 -0.5)))))
        (pow cosTheta 4.0))))))))

C

float code(float cosTheta, float c) {
	return 1.0f / ((1.0f + c) + (((1.0f / sqrtf(((float) M_PI))) * (sqrtf(((1.0f - cosTheta) - cosTheta)) / cosTheta)) * expf((-cosTheta * cosTheta))));
}

↓

float code(float cosTheta, float c) {
	float t_0 = powf(sqrtf(((float) M_PI)), 3.0f);
	float t_1 = sqrtf((1.0f / ((float) M_PI)));
	float t_2 = -t_1;
	float t_3 = -1.0f - (t_2 + c);
	float t_4 = t_2 + (1.0f + c);
	float t_5 = (powf(t_4, 2.0f) * -t_0) + (t_1 * (((float) M_PI) * -1.5f));
	return (cosTheta * sqrtf(((float) M_PI))) + -((((float) M_PI) * (powf(cosTheta, 2.0f) * t_4)) + ((t_5 * powf(cosTheta, 3.0f)) + (((sqrtf(((float) M_PI)) * (t_5 * t_3)) + ((t_0 * ((t_1 * -1.5f) * t_3)) + (((float) M_PI) * (t_1 + (t_1 * -0.5f))))) * powf(cosTheta, 4.0f))));
}

Julia

function code(cosTheta, c)
	return Float32(Float32(1.0) / Float32(Float32(Float32(1.0) + c) + Float32(Float32(Float32(Float32(1.0) / sqrt(Float32(pi))) * Float32(sqrt(Float32(Float32(Float32(1.0) - cosTheta) - cosTheta)) / cosTheta)) * exp(Float32(Float32(-cosTheta) * cosTheta)))))
end

↓

function code(cosTheta, c)
	t_0 = sqrt(Float32(pi)) ^ Float32(3.0)
	t_1 = sqrt(Float32(Float32(1.0) / Float32(pi)))
	t_2 = Float32(-t_1)
	t_3 = Float32(Float32(-1.0) - Float32(t_2 + c))
	t_4 = Float32(t_2 + Float32(Float32(1.0) + c))
	t_5 = Float32(Float32((t_4 ^ Float32(2.0)) * Float32(-t_0)) + Float32(t_1 * Float32(Float32(pi) * Float32(-1.5))))
	return Float32(Float32(cosTheta * sqrt(Float32(pi))) + Float32(-Float32(Float32(Float32(pi) * Float32((cosTheta ^ Float32(2.0)) * t_4)) + Float32(Float32(t_5 * (cosTheta ^ Float32(3.0))) + Float32(Float32(Float32(sqrt(Float32(pi)) * Float32(t_5 * t_3)) + Float32(Float32(t_0 * Float32(Float32(t_1 * Float32(-1.5)) * t_3)) + Float32(Float32(pi) * Float32(t_1 + Float32(t_1 * Float32(-0.5)))))) * (cosTheta ^ Float32(4.0)))))))
end

MATLAB

function tmp = code(cosTheta, c)
	tmp = single(1.0) / ((single(1.0) + c) + (((single(1.0) / sqrt(single(pi))) * (sqrt(((single(1.0) - cosTheta) - cosTheta)) / cosTheta)) * exp((-cosTheta * cosTheta))));
end

↓

function tmp = code(cosTheta, c)
	t_0 = sqrt(single(pi)) ^ single(3.0);
	t_1 = sqrt((single(1.0) / single(pi)));
	t_2 = -t_1;
	t_3 = single(-1.0) - (t_2 + c);
	t_4 = t_2 + (single(1.0) + c);
	t_5 = ((t_4 ^ single(2.0)) * -t_0) + (t_1 * (single(pi) * single(-1.5)));
	tmp = (cosTheta * sqrt(single(pi))) + -((single(pi) * ((cosTheta ^ single(2.0)) * t_4)) + ((t_5 * (cosTheta ^ single(3.0))) + (((sqrt(single(pi)) * (t_5 * t_3)) + ((t_0 * ((t_1 * single(-1.5)) * t_3)) + (single(pi) * (t_1 + (t_1 * single(-0.5)))))) * (cosTheta ^ single(4.0)))));
end

Derivation

1. Initial program 0.7

   \[\frac{1}{\left(1 + c\right) + \left(\frac{1}{\sqrt{\pi}} \cdot \frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta}\right) \cdot e^{\left(-cosTheta\right) \cdot cosTheta}} \]

2. Simplified 0.7

   \[\leadsto \color{blue}{\frac{1}{\left(1 + c\right) + \frac{1}{\sqrt{\pi}} \cdot \left(\frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta} \cdot e^{cosTheta \cdot \left(-cosTheta\right)}\right)}} \]
   Proof

   [Start] 0.7	\[ \frac{1}{\left(1 + c\right) + \left(\frac{1}{\sqrt{\pi}} \cdot \frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta}\right) \cdot e^{\left(-cosTheta\right) \cdot cosTheta}} \]
   rational_best.json-simplify-2 [=>] 0.7	\[ \frac{1}{\left(1 + c\right) + \color{blue}{e^{\left(-cosTheta\right) \cdot cosTheta} \cdot \left(\frac{1}{\sqrt{\pi}} \cdot \frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta}\right)}} \]
   rational_best.json-simplify-44 [=>] 0.7	\[ \frac{1}{\left(1 + c\right) + \color{blue}{\frac{1}{\sqrt{\pi}} \cdot \left(e^{\left(-cosTheta\right) \cdot cosTheta} \cdot \frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta}\right)}} \]
   rational_best.json-simplify-2 [=>] 0.7	\[ \frac{1}{\left(1 + c\right) + \frac{1}{\sqrt{\pi}} \cdot \color{blue}{\left(\frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta} \cdot e^{\left(-cosTheta\right) \cdot cosTheta}\right)}} \]
   rational_best.json-simplify-2 [=>] 0.7	\[ \frac{1}{\left(1 + c\right) + \frac{1}{\sqrt{\pi}} \cdot \left(\frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta} \cdot e^{\color{blue}{cosTheta \cdot \left(-cosTheta\right)}}\right)} \]

3. Taylor expanded in cosTheta around 0 0.8

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

4. Simplified 0.8

   \[\leadsto \color{blue}{cosTheta \cdot \sqrt{\pi} + \left(-\left(\pi \cdot \left({cosTheta}^{2} \cdot \left(\left(-\sqrt{\frac{1}{\pi}}\right) + \left(1 + c\right)\right)\right) + \left(\left({\left(\left(-\sqrt{\frac{1}{\pi}}\right) + \left(1 + c\right)\right)}^{2} \cdot \left(-{\left(\sqrt{\pi}\right)}^{3}\right) + \sqrt{\frac{1}{\pi}} \cdot \left(\pi \cdot -1.5\right)\right) \cdot {cosTheta}^{3} + \left(\sqrt{\pi} \cdot \left(\left({\left(\left(-\sqrt{\frac{1}{\pi}}\right) + \left(1 + c\right)\right)}^{2} \cdot \left(-{\left(\sqrt{\pi}\right)}^{3}\right) + \sqrt{\frac{1}{\pi}} \cdot \left(\pi \cdot -1.5\right)\right) \cdot \left(-1 - \left(\left(-\sqrt{\frac{1}{\pi}}\right) + c\right)\right)\right) + \left({\left(\sqrt{\pi}\right)}^{3} \cdot \left(\left(\sqrt{\frac{1}{\pi}} \cdot -1.5\right) \cdot \left(-1 - \left(\left(-\sqrt{\frac{1}{\pi}}\right) + c\right)\right)\right) + \pi \cdot \left(\sqrt{\frac{1}{\pi}} + \sqrt{\frac{1}{\pi}} \cdot -0.5\right)\right)\right) \cdot {cosTheta}^{4}\right)\right)\right)} \]
   Proof

   [Start] 0.8

   \[ -1 \cdot \left(\left(-1 \cdot \left(\left(\left(-0.5 \cdot \sqrt{\frac{1}{\pi}} + -1 \cdot \sqrt{\frac{1}{\pi}}\right) \cdot \left(c + \left(1 + -1 \cdot \sqrt{\frac{1}{\pi}}\right)\right)\right) \cdot \sqrt{{\pi}^{3}}\right) + \left(\left(-0.5 \cdot \sqrt{\frac{1}{\pi}} + \sqrt{\frac{1}{\pi}}\right) \cdot \pi + -1 \cdot \left(\left(\left(-1 \cdot \left({\left(c + \left(1 + -1 \cdot \sqrt{\frac{1}{\pi}}\right)\right)}^{2} \cdot \sqrt{{\pi}^{3}}\right) + \left(-1 \cdot \sqrt{\frac{1}{\pi}} + -0.5 \cdot \sqrt{\frac{1}{\pi}}\right) \cdot \pi\right) \cdot \left(c + \left(1 + -1 \cdot \sqrt{\frac{1}{\pi}}\right)\right)\right) \cdot \sqrt{\pi}\right)\right)\right) \cdot {cosTheta}^{4}\right) + \left(cosTheta \cdot \sqrt{\pi} + \left(-1 \cdot \left(\left(-1 \cdot \left({\left(c + \left(1 + -1 \cdot \sqrt{\frac{1}{\pi}}\right)\right)}^{2} \cdot \sqrt{{\pi}^{3}}\right) + \left(-0.5 \cdot \sqrt{\frac{1}{\pi}} + -1 \cdot \sqrt{\frac{1}{\pi}}\right) \cdot \pi\right) \cdot {cosTheta}^{3}\right) + -1 \cdot \left({cosTheta}^{2} \cdot \left(\left(c + \left(1 + -1 \cdot \sqrt{\frac{1}{\pi}}\right)\right) \cdot \pi\right)\right)\right)\right) \]

5. Final simplification 0.8

   \[\leadsto cosTheta \cdot \sqrt{\pi} + \left(-\left(\pi \cdot \left({cosTheta}^{2} \cdot \left(\left(-\sqrt{\frac{1}{\pi}}\right) + \left(1 + c\right)\right)\right) + \left(\left({\left(\left(-\sqrt{\frac{1}{\pi}}\right) + \left(1 + c\right)\right)}^{2} \cdot \left(-{\left(\sqrt{\pi}\right)}^{3}\right) + \sqrt{\frac{1}{\pi}} \cdot \left(\pi \cdot -1.5\right)\right) \cdot {cosTheta}^{3} + \left(\sqrt{\pi} \cdot \left(\left({\left(\left(-\sqrt{\frac{1}{\pi}}\right) + \left(1 + c\right)\right)}^{2} \cdot \left(-{\left(\sqrt{\pi}\right)}^{3}\right) + \sqrt{\frac{1}{\pi}} \cdot \left(\pi \cdot -1.5\right)\right) \cdot \left(-1 - \left(\left(-\sqrt{\frac{1}{\pi}}\right) + c\right)\right)\right) + \left({\left(\sqrt{\pi}\right)}^{3} \cdot \left(\left(\sqrt{\frac{1}{\pi}} \cdot -1.5\right) \cdot \left(-1 - \left(\left(-\sqrt{\frac{1}{\pi}}\right) + c\right)\right)\right) + \pi \cdot \left(\sqrt{\frac{1}{\pi}} + \sqrt{\frac{1}{\pi}} \cdot -0.5\right)\right)\right) \cdot {cosTheta}^{4}\right)\right)\right) \]

Alternatives

Alternative 1
Error	0.7
Cost	13472

\[\frac{1}{\left(1 + c\right) + \left(\frac{1}{\sqrt{\pi}} \cdot \frac{\sqrt{\left(1 - cosTheta\right) - cosTheta}}{cosTheta}\right) \cdot e^{\left(-cosTheta\right) \cdot cosTheta}} \]

Alternative 2
Error	0.8
Cost	13312

\[\frac{1}{1 + \frac{e^{-{cosTheta}^{2}}}{cosTheta} \cdot \sqrt{\frac{1 - cosTheta \cdot 2}{\pi}}} \]

Alternative 3
Error	1.2
Cost	6912

\[\frac{1}{1 + \sqrt{\frac{1}{\pi}} \cdot \left(-1 + \left(\frac{1}{cosTheta} + -1.5 \cdot cosTheta\right)\right)} \]

Alternative 4
Error	1.6
Cost	6848

\[\frac{1}{\left(1 + c\right) + \sqrt{\frac{1}{\pi}} \cdot \left(\frac{1}{cosTheta} + -1\right)} \]

Alternative 5
Error	1.6
Cost	6784

\[\frac{1}{1 + \sqrt{\frac{1}{\pi}} \cdot \left(-1 + \frac{1}{cosTheta}\right)} \]

Alternative 6
Error	2.2
Cost	6464

\[cosTheta \cdot \sqrt{\pi} \]

Alternative 7
Error	28.6
Cost	128

\[1 + \left(-c\right) \]

Alternative 8
Error	28.6
Cost	32

\[1 \]

Reproduce

herbie shell --seed 2023090 
(FPCore (cosTheta c)
  :name "Beckmann Sample, normalization factor"
  :precision binary32
  :pre (and (and (< 0.0 cosTheta) (< cosTheta 0.9999)) (and (< -1.0 c) (< c 1.0)))
  (/ 1.0 (+ (+ 1.0 c) (* (* (/ 1.0 (sqrt PI)) (/ (sqrt (- (- 1.0 cosTheta) cosTheta)) cosTheta)) (exp (* (- cosTheta) cosTheta))))))