\[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]

↓

\[0.5 \cdot \left(y + \frac{x - z}{\frac{y}{x + z}}\right) \]

(FPCore (x y z)
 :precision binary64
 (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2.0)))

↓

(FPCore (x y z) :precision binary64 (* 0.5 (+ y (/ (- x z) (/ y (+ x z))))))

double code(double x, double y, double z) {
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
}

↓

double code(double x, double y, double z) {
	return 0.5 * (y + ((x - z) / (y / (x + z))));
}

real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = (((x * x) + (y * y)) - (z * z)) / (y * 2.0d0)
end function

↓

real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = 0.5d0 * (y + ((x - z) / (y / (x + z))))
end function

public static double code(double x, double y, double z) {
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
}

↓

public static double code(double x, double y, double z) {
	return 0.5 * (y + ((x - z) / (y / (x + z))));
}

def code(x, y, z):
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0)

↓

def code(x, y, z):
	return 0.5 * (y + ((x - z) / (y / (x + z))))

function code(x, y, z)
	return Float64(Float64(Float64(Float64(x * x) + Float64(y * y)) - Float64(z * z)) / Float64(y * 2.0))
end

↓

function code(x, y, z)
	return Float64(0.5 * Float64(y + Float64(Float64(x - z) / Float64(y / Float64(x + z)))))
end

function tmp = code(x, y, z)
	tmp = (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
end

↓

function tmp = code(x, y, z)
	tmp = 0.5 * (y + ((x - z) / (y / (x + z))));
end

code[x_, y_, z_] := N[(N[(N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision] - N[(z * z), $MachinePrecision]), $MachinePrecision] / N[(y * 2.0), $MachinePrecision]), $MachinePrecision]

↓

code[x_, y_, z_] := N[(0.5 * N[(y + N[(N[(x - z), $MachinePrecision] / N[(y / N[(x + z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}

↓

0.5 \cdot \left(y + \frac{x - z}{\frac{y}{x + z}}\right)

Original	28.9
Target	0.2
Herbie	0.1

Derivation

Initial program 28.9
\[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
Taylor expanded in x around 0 28.9
\[\leadsto \color{blue}{0.5 \cdot \frac{{y}^{2} - {z}^{2}}{y} + 0.5 \cdot \frac{{x}^{2}}{y}} \]
Simplified0.1
\[\leadsto \color{blue}{0.5 \cdot \mathsf{fma}\left(\frac{z + x}{y}, x - z, y\right)} \]
Proof
(*.f64 1/2 (fma.f64 (/.f64 (+.f64 z x) y) (-.f64 x z) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (fma.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x z)) y) (-.f64 x z) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (+.f64 x z) y) (-.f64 x z)) y))): 3 points increase in error, 1 points decrease in error
(*.f64 1/2 (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (+.f64 x z) (-.f64 x z)) y)) y)): 63 points increase in error, 15 points decrease in error
(*.f64 1/2 (+.f64 (/.f64 (Rewrite<= difference-of-squares_binary64 (-.f64 (*.f64 x x) (*.f64 z z))) y) y)): 1 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 (/.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) (*.f64 z z)) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 (/.f64 (-.f64 (pow.f64 x 2) (Rewrite<= unpow2_binary64 (pow.f64 z 2))) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (Rewrite<= +-commutative_binary64 (+.f64 y (/.f64 (-.f64 (pow.f64 x 2) (pow.f64 z 2)) y)))): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 y (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (pow.f64 x 2) y) (/.f64 (pow.f64 z 2) y))))): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 y (/.f64 (pow.f64 x 2) y)) (/.f64 (pow.f64 z 2) y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 1/2 (+.f64 y (/.f64 (pow.f64 x 2) y))) (*.f64 1/2 (/.f64 (pow.f64 z 2) y)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 (*.f64 1/2 (+.f64 y (/.f64 (pow.f64 x 2) y))) (*.f64 (neg.f64 1/2) (/.f64 (pow.f64 z 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 1/2 y) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))) (*.f64 (neg.f64 1/2) (/.f64 (pow.f64 z 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 y) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))) (*.f64 (Rewrite=> metadata-eval -1/2) (/.f64 (pow.f64 z 2) y))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-+l+_binary64 (+.f64 (*.f64 1/2 y) (+.f64 (*.f64 1/2 (/.f64 (pow.f64 x 2) y)) (*.f64 -1/2 (/.f64 (pow.f64 z 2) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 y) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= /-rgt-identity_binary64 (/.f64 y 1))) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (/.f64 y (Rewrite<= *-inverses_binary64 (/.f64 y y)))) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y y) y))) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 78 points increase in error, 1 points decrease in error
(+.f64 (*.f64 1/2 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 y 2)) y)) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (*.f64 -1/2 (/.f64 (pow.f64 z 2) y))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (*.f64 (Rewrite<= metadata-eval (*.f64 1/2 -1)) (/.f64 (pow.f64 z 2) y))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (Rewrite<= associate-*r*_binary64 (*.f64 1/2 (*.f64 -1 (/.f64 (pow.f64 z 2) y))))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (*.f64 1/2 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (pow.f64 z 2) y))))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 1/2 (+.f64 (/.f64 (pow.f64 y 2) y) (neg.f64 (/.f64 (pow.f64 z 2) y))))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 (pow.f64 y 2) y) (/.f64 (pow.f64 z 2) y)))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (pow.f64 y 2) (pow.f64 z 2)) y))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 2 points decrease in error
Applied egg-rr0.1
\[\leadsto 0.5 \cdot \color{blue}{\left(\frac{x - z}{\frac{y}{z + x}} + y\right)} \]
Final simplification0.1
\[\leadsto 0.5 \cdot \left(y + \frac{x - z}{\frac{y}{x + z}}\right) \]

Alternatives

Alternative 1
Error	7.4
Cost	1104

\[\begin{array}{l} t_0 := 0.5 \cdot \left(y + \frac{x}{\frac{y}{x}}\right)\\ t_1 := 0.5 \cdot \left(y - \frac{z}{\frac{y}{z}}\right)\\ \mathbf{if}\;z \leq -26679039.31550349:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \leq -2.6755016075328835 \cdot 10^{-32}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq -8.7175668416721 \cdot 10^{-82}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \leq 3.9549661420208875 \cdot 10^{-99}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 2
Error	23.3
Cost	844

\[\begin{array}{l} \mathbf{if}\;y \leq -1.15 \cdot 10^{-25}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq 9.5 \cdot 10^{-225}:\\ \;\;\;\;0.5 \cdot \left(x \cdot \frac{x}{y}\right)\\ \mathbf{elif}\;y \leq 9.5 \cdot 10^{-56}:\\ \;\;\;\;\frac{z}{\frac{y}{z}} \cdot -0.5\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 3
Error	15.2
Cost	840

\[\begin{array}{l} t_0 := 0.5 \cdot \left(y + \frac{x}{\frac{y}{x}}\right)\\ \mathbf{if}\;y \leq 1.2 \cdot 10^{-184}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 8.8 \cdot 10^{-63}:\\ \;\;\;\;\frac{z}{\frac{y}{z}} \cdot -0.5\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 4
Error	23.3
Cost	712

\[\begin{array}{l} \mathbf{if}\;y \leq -1.15 \cdot 10^{-25}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq 2.5 \cdot 10^{-47}:\\ \;\;\;\;x \cdot \frac{0.5}{\frac{y}{x}}\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 5
Error	23.3
Cost	712

\[\begin{array}{l} \mathbf{if}\;y \leq -1.15 \cdot 10^{-25}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq 2.5 \cdot 10^{-47}:\\ \;\;\;\;0.5 \cdot \left(x \cdot \frac{x}{y}\right)\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 6
Error	27.1
Cost	192

\[0.5 \cdot y \]

Error

Try it out

Target

Derivation

Alternatives

Error

Reproduce

In
Out