Possibly incorrect output?

[LeventErkok]

Thanks for Herbie! I think this is a very nice addition to the Haskell tool-suite.. I gave it a shot, however, and am a bit confused about some of the output. I tried the following program:

module Test where

foo :: Float -> Float -> Float
foo x y = (x * x) + (2 * x * y) + (y * y)

Herbie said:

Compiling with Herbie floating point stabilization
Found math expression within binding foo :: Float -> Float -> Float
  original expression = (x * x) + (2 * x * y) + (y * y)
  improved expression = (x * x) + (2 * y * x) + (y * y)
  original error = 1.5625e-2 bits
  improved error = 3.90625e-3 bits
  WARNING: Not substituting the improved expression into your code
  WARNING: Cannot satisfy the constraint: Num Float

Given the complete symmetry between x and y; is the improvement due to NaN/Infinity results only? When both expressions produce actual floating point values, can they actually differ? What does it mean to have the error bits in this case?

It would be uber cool if Herbie printed examples of x and y when the results differed, to start with.

Also, I'm not sure what to make of the WARNING, as Float is clearly an instance of Num.

Thanks!

[mikeizbicki]

I'm not sure why Herbie is reporting the two expressions as having different errors. I'll contact the Herbie program developers about what's going on.

The issue with the warnings is because HerbiePlugin does not fully support the standard Prelude. There is a detailed description of this bug in the known bugs section of the README.

[mikeizbicki]

I've figured out why those expressions are giving different results. This is related to bug #16. The problem is that I was too aggressive in removing parenthesis from the expression. Here's the new output:

Found math expression within binding test5 :: Float -> Float -> Float
  original expression = ((x * x) + ((2 * x) * y)) + (y * y)
  Not found in database.  Running Herbie...
  improved expression = (x * x) + ((y * y) + ((x * y) * 2))
  original error = 1.5625e-2 bits
  improved error = 3.90625e-3 bits

The change in association is the cause of the change in error reported.

I still want to get Herbie to report some actual cases where the results differ at.

[LeventErkok]

Cool.. It would indeed be nice for Herbie to print values where the results do differ. I did a bit of experimentation, and found the following. For the original expression, my version of Herbie actually produced the following optimized expression:

(x * x) + ((2 * (y * x)) + (y * y))

which is different than what you provided above; but still seems to be a valid rewrite. With this output, I found the following values:

     x =        +5024.234000
     y =      +106856.310000
  orig = +12517257000.000000
   opt = +12517256000.000000
 exact = +12517256125.735936

orig is the result of the original expression; opt is the result of the Herbie-optimized expression, and exact is the result with infinite precision. It is nice to note that the original differs from the exact result by about 875, while Herbie's expression only differs by 125. It would be so cool if Herbie printed this sort of an output indeed.