Numeric.SpecFunctions:log1p from math-functions-0.1.5.2, A

Average Error: 0.16% → 0.16%

Time: 6.2s

Precision: binary64

Cost: 6784

Math

\[x \cdot \left(1 - x \cdot y\right) \]

↓

\[x \cdot \left(-\mathsf{fma}\left(y, x, -1\right)\right) \]

FPCore

(FPCore (x y) :precision binary64 (* x (- 1.0 (* x y))))

↓

(FPCore (x y) :precision binary64 (* x (- (fma y x -1.0))))

C

double code(double x, double y) {
	return x * (1.0 - (x * y));
}

↓

double code(double x, double y) {
	return x * -fma(y, x, -1.0);
}

Julia

function code(x, y)
	return Float64(x * Float64(1.0 - Float64(x * y)))
end

↓

function code(x, y)
	return Float64(x * Float64(-fma(y, x, -1.0)))
end

Wolfram

code[x_, y_] := N[(x * N[(1.0 - N[(x * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[x_, y_] := N[(x * (-N[(y * x + -1.0), $MachinePrecision])), $MachinePrecision]

Derivation

1. Initial program 0.16

   \[x \cdot \left(1 - x \cdot y\right) \]

2. Simplified 0.15

   \[\leadsto \color{blue}{x - x \cdot \left(x \cdot y\right)} \]
   Proof

   [Start] 0.16	\[ x \cdot \left(1 - x \cdot y\right) \]
   distribute-lft-out-- [<=] 0.15	\[ \color{blue}{x \cdot 1 - x \cdot \left(x \cdot y\right)} \]
   *-rgt-identity [=>] 0.15	\[ \color{blue}{x} - x \cdot \left(x \cdot y\right) \]

3. Applied egg-rr 47.32

   \[\leadsto \color{blue}{\left(x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}\right) \cdot \frac{1}{x + x \cdot \left(x \cdot y\right)}} \]

4. Simplified 0.22

   \[\leadsto \color{blue}{\frac{x}{\frac{1}{1 - y \cdot x}}} \]
   Proof

   [Start] 47.32	\[ \left(x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}\right) \cdot \frac{1}{x + x \cdot \left(x \cdot y\right)} \]
   associate-*r/ [=>] 47.19	\[ \color{blue}{\frac{\left(x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}\right) \cdot 1}{x + x \cdot \left(x \cdot y\right)}} \]
   *-rgt-identity [=>] 47.19	\[ \frac{\color{blue}{x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}}}{x + x \cdot \left(x \cdot y\right)} \]
   associate-*r* [=>] 49.21	\[ \frac{x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}}{x + \color{blue}{\left(x \cdot x\right) \cdot y}} \]
   cancel-sign-sub [<=] 49.21	\[ \frac{x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}}{\color{blue}{x - \left(-x \cdot x\right) \cdot y}} \]
   distribute-lft-neg-in [<=] 49.21	\[ \frac{x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}}{x - \color{blue}{\left(-\left(x \cdot x\right) \cdot y\right)}} \]
   distribute-rgt-neg-out [<=] 49.21	\[ \frac{x \cdot x - {\left(x \cdot \left(x \cdot y\right)\right)}^{2}}{x - \color{blue}{\left(x \cdot x\right) \cdot \left(-y\right)}} \]
   div-sub [=>] 49.21	\[ \color{blue}{\frac{x \cdot x}{x - \left(x \cdot x\right) \cdot \left(-y\right)} - \frac{{\left(x \cdot \left(x \cdot y\right)\right)}^{2}}{x - \left(x \cdot x\right) \cdot \left(-y\right)}} \]
   unpow2 [=>] 49.21	\[ \frac{x \cdot x}{x - \left(x \cdot x\right) \cdot \left(-y\right)} - \frac{\color{blue}{\left(x \cdot \left(x \cdot y\right)\right) \cdot \left(x \cdot \left(x \cdot y\right)\right)}}{x - \left(x \cdot x\right) \cdot \left(-y\right)} \]
   sqr-neg [<=] 49.21	\[ \frac{x \cdot x}{x - \left(x \cdot x\right) \cdot \left(-y\right)} - \frac{\color{blue}{\left(-x \cdot \left(x \cdot y\right)\right) \cdot \left(-x \cdot \left(x \cdot y\right)\right)}}{x - \left(x \cdot x\right) \cdot \left(-y\right)} \]
   associate-*r* [=>] 49	\[ \frac{x \cdot x}{x - \left(x \cdot x\right) \cdot \left(-y\right)} - \frac{\left(-\color{blue}{\left(x \cdot x\right) \cdot y}\right) \cdot \left(-x \cdot \left(x \cdot y\right)\right)}{x - \left(x \cdot x\right) \cdot \left(-y\right)} \]
   distribute-rgt-neg-out [<=] 49	\[ \frac{x \cdot x}{x - \left(x \cdot x\right) \cdot \left(-y\right)} - \frac{\color{blue}{\left(\left(x \cdot x\right) \cdot \left(-y\right)\right)} \cdot \left(-x \cdot \left(x \cdot y\right)\right)}{x - \left(x \cdot x\right) \cdot \left(-y\right)} \]
   associate-*r* [=>] 49.16	\[ \frac{x \cdot x}{x - \left(x \cdot x\right) \cdot \left(-y\right)} - \frac{\left(\left(x \cdot x\right) \cdot \left(-y\right)\right) \cdot \left(-\color{blue}{\left(x \cdot x\right) \cdot y}\right)}{x - \left(x \cdot x\right) \cdot \left(-y\right)} \]
   distribute-rgt-neg-out [<=] 49.16	\[ \frac{x \cdot x}{x - \left(x \cdot x\right) \cdot \left(-y\right)} - \frac{\left(\left(x \cdot x\right) \cdot \left(-y\right)\right) \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(-y\right)\right)}}{x - \left(x \cdot x\right) \cdot \left(-y\right)} \]

5. Taylor expanded in x around 0 12.7

   \[\leadsto \color{blue}{-1 \cdot \left(y \cdot {x}^{2}\right) + x} \]

6. Simplified 0.16

   \[\leadsto \color{blue}{-x \cdot \mathsf{fma}\left(y, x, -1\right)} \]
   Proof

   [Start] 12.7	\[ -1 \cdot \left(y \cdot {x}^{2}\right) + x \]
   unpow2 [=>] 12.7	\[ -1 \cdot \left(y \cdot \color{blue}{\left(x \cdot x\right)}\right) + x \]
   associate-*r* [=>] 0.15	\[ -1 \cdot \color{blue}{\left(\left(y \cdot x\right) \cdot x\right)} + x \]
   associate-*l* [<=] 0.15	\[ \color{blue}{\left(-1 \cdot \left(y \cdot x\right)\right) \cdot x} + x \]
   mul-1-neg [=>] 0.15	\[ \color{blue}{\left(-y \cdot x\right)} \cdot x + x \]
   distribute-rgt-neg-out [<=] 0.15	\[ \color{blue}{\left(y \cdot \left(-x\right)\right)} \cdot x + x \]
   distribute-lft1-in [=>] 0.16	\[ \color{blue}{\left(y \cdot \left(-x\right) + 1\right) \cdot x} \]
   +-commutative [<=] 0.16	\[ \color{blue}{\left(1 + y \cdot \left(-x\right)\right)} \cdot x \]
   metadata-eval [<=] 0.16	\[ \left(\color{blue}{\left(--1\right)} + y \cdot \left(-x\right)\right) \cdot x \]
   distribute-rgt-neg-out [=>] 0.16	\[ \left(\left(--1\right) + \color{blue}{\left(-y \cdot x\right)}\right) \cdot x \]
   distribute-neg-in [<=] 0.16	\[ \color{blue}{\left(-\left(-1 + y \cdot x\right)\right)} \cdot x \]
   *-commutative [<=] 0.16	\[ \color{blue}{x \cdot \left(-\left(-1 + y \cdot x\right)\right)} \]
   /-rgt-identity [<=] 0.16	\[ \color{blue}{\frac{x}{1}} \cdot \left(-\left(-1 + y \cdot x\right)\right) \]
   *-inverses [<=] 8.66	\[ \frac{x}{\color{blue}{\frac{1 - {\left(y \cdot x\right)}^{2}}{1 - {\left(y \cdot x\right)}^{2}}}} \cdot \left(-\left(-1 + y \cdot x\right)\right) \]
   associate-/l* [<=] 12.78	\[ \color{blue}{\frac{x \cdot \left(1 - {\left(y \cdot x\right)}^{2}\right)}{1 - {\left(y \cdot x\right)}^{2}}} \cdot \left(-\left(-1 + y \cdot x\right)\right) \]
   distribute-rgt-neg-out [=>] 12.78	\[ \color{blue}{-\frac{x \cdot \left(1 - {\left(y \cdot x\right)}^{2}\right)}{1 - {\left(y \cdot x\right)}^{2}} \cdot \left(-1 + y \cdot x\right)} \]
   associate-/l* [=>] 8.66	\[ -\color{blue}{\frac{x}{\frac{1 - {\left(y \cdot x\right)}^{2}}{1 - {\left(y \cdot x\right)}^{2}}}} \cdot \left(-1 + y \cdot x\right) \]
   *-inverses [=>] 0.16	\[ -\frac{x}{\color{blue}{1}} \cdot \left(-1 + y \cdot x\right) \]
   /-rgt-identity [=>] 0.16	\[ -\color{blue}{x} \cdot \left(-1 + y \cdot x\right) \]
   +-commutative [=>] 0.16	\[ -x \cdot \color{blue}{\left(y \cdot x + -1\right)} \]
   fma-def [=>] 0.16	\[ -x \cdot \color{blue}{\mathsf{fma}\left(y, x, -1\right)} \]

7. Final simplification 0.16

   \[\leadsto x \cdot \left(-\mathsf{fma}\left(y, x, -1\right)\right) \]

Alternatives

Alternative 1
Error	23.15%
Cost	649

\[\begin{array}{l} \mathbf{if}\;y \leq -3.1 \cdot 10^{+64} \lor \neg \left(y \leq 1.3 \cdot 10^{+91}\right):\\ \;\;\;\;x \cdot \left(x \cdot \left(-y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 2
Error	0.16%
Cost	448

\[x \cdot \left(1 - x \cdot y\right) \]

Alternative 3
Error	34.36%
Cost	64

\[x \]

Reproduce

herbie shell --seed 2023090 
(FPCore (x y)
  :name "Numeric.SpecFunctions:log1p from math-functions-0.1.5.2, A"
  :precision binary64
  (* x (- 1.0 (* x y))))