3

I am at a point where I need to know whether there is a polynomial $f \in \mathbb Z [X,Y]$ such that:

  • $f(1,y) \ge 0$ for all $y \ge 0$

  • $y-1,x \ge 0 \wedge f(x,y) \ge 0 \Rightarrow 0 \le f(2x,y-1) < f(x,y)$

  • $ x-1 \ge 0 \wedge f(x,0) \ge 0 \Rightarrow 0 \le f(x-1,0) < f(x,0)$

and so far I didn't come up with an idea how to construct such a polynomial or how to disprove its existence.

If anyone wonders where this problem came up: I am trying to prove that a certain while program cannot be shown to be correct within a specific set of Hoare rules and reduced it to this problem. We are only expected to "argue" that this indeed is impossible, but I really want to see a proof, since it isn't that obvious - I guess.

Stefan Mesken
  • 16,651

1 Answers1

3

Let $f(1, y) = n$ for some fixed, positive $y$. Successive uses of point 2. shows that $0 \leq f(2^y, 0) \leq n - y$. Then successive uses of 3. show that $0 \leq f(0, 0) \leq n - y - 2^y$, which means that $y + 2^y \leq f(1, y)$. The function $f(1, y)$ must therefore grow (at least) exponentially in $y$, but no polynomial can do that for very long.

Arthur
  • 199,419