5

Assume all numbers and operations below are in floating-point arithmetic with finite precision, bounded exponent, and rounding to the nearest integer.

Are there $x,y$ positive such that $$\begin{align}(x+y)-x&>y\\(x+y)-s(x)&>y\end{align}$$ where $s(x)$ denotes the successor of $x$?

This question appeared while designing a test for a software.

It is easy to write a program that searches for such an example, but it is unfeasible to test all possibilities and show that the example doesn't exist. So far my code hasn't got any example.

Example: In case seeing an example of $(x+y)-x>y$ helps somehow, take $$ \begin{align} x&=1.1234567891234568\\ y&=1e-5\text{ ( denoting }10^{-5}) \end{align} $$ Then $(x+y)-x=1.0000000000065512e-05 > y$. There are many examples of the first inequality.

Link to scicomp.stackexchange's copy of this post in case a solution appears there first. There is already a solution there.

Rodrigo de Azevedo
  • 1
EEE
  • 111
  • I don't see this question as being about mathematics. – 5xum Oct 03 '17 at 12:10
  • 3
    @5xum There is a field of mathematics called Numerical Analysis that studies floating point arithmetic. The question explores the magnitude of the failure of asociativity in floating point arithmetic. – EEE Oct 03 '17 at 12:14
  • 2
    @5xum And not only mathematics, it belongs to the far narrower scope that this website handles. Observe how the tag (floating-point) exists here. – EEE Oct 03 '17 at 12:28
  • Try also https://scicomp.stackexchange.com – lhf Oct 03 '17 at 14:04
  • I guess you want to work with rounding-to-nearest mode. For round-up mode there are examples for both. – gammatester Oct 03 '17 at 14:46
  • @gammatester Yes. Let me add that to the question since it is important. – EEE Oct 03 '17 at 22:35
  • Let $x$ be the largest number with $1-s(x)=1$. IIRC, this still makes $y+x=1$ if $y$ is the largest number $<1$. – Hagen von Eitzen Oct 03 '17 at 23:28
  • @HagenvonEitzen Doesn't seem to be the case. For double, $x$ would be the predecessor of $5.551115123125783e-17$. This is, $x = 5.5511151231257821e-17$. For $y$ we have that $y=0.99999999999999989$. When I compute $x+y$, I get $y$. – EEE Oct 04 '17 at 01:09

1 Answers1

0

This is precisely the kind of question that an SMT solver like Z3 was made to solve. We can use the following python code:

from z3 import *

x = FP('x', FPSort(8,24))
y = FP('y', FPSort(8,24))


s = Solver()
s.add((x + y) - x > y)
s.add((x + y) - (x+1) > y)
print(s.check())
print(s.model())

This will create two local representations of floating point numbers (the FPSort specifies how many bits of exponent, followed by how many bits of data, so these are 32 bit floats), and then attempt to find a model where both of the required statements are true. We run this code and get the following model:

[x = -1.869740962982177734375*(2**127),
y = -1.47381579875946044921875*(2**127)]
Lucas
  • 1