Integer division using only addition, multiplication, subtraction and maximum

Question

Suppose we have a programming language ℤ which has the following syntax:

ℤ := 0 | 1 | (+ ℤ ℤ) | (* ℤ ℤ) | (- ℤ ℤ) | (max ℤ ℤ)

For convenience, we can define new binding forms in our language as follows:

1. (not x) = (- 1 x)
2. (abs x) = (- (max 0 (+ x x)) x)
3. (min x y) = (- 0 (max (- 0 x) (- 0 y)))
4. (nil x) = (not (min 1 (abs x)))

This language is powerful enough to express branching and comparison operators:

5. (if x y z) = (+ (* x y) (* (not x) z))
6. (eq x y) = (nil (- x y))
7. (ne x y) = (not (eq x y))
8. (le x y) = (nil (max 0 (- x y)))
9. (gt x y) = (not (le x y))
10. (ge x y) = (le y x)
11. (lt x y) = (not (ge x y))

Now, the question is whether we can define integer division is this language:

12. (div x y) = ?
13. (rem x y) = (- x (* y (div x y)))

I don't think that it's possible to define (div x y) because ℤ doesn't have loops. However, I don't know how to prove it. Note that if it's possible then the result of (div x 0) doesn't matter. Hence, either define (div x y) or prove that it's impossible to do so.

Answer 1

It's impossible.

Call a function f : Z -> Z eventually polynomial if there exists a polynomial p with integer coefficients and a threshold t such that, for every x > t, we have f(x) = p(x). Let d(x) = [x/2] be floor division by two. d is not eventually polynomial, because the difference sequence of d has infinitely many zeros (f(2y) = y = f(2y+1) for all y), whereas the difference sequence of every non constant polynomial has finitely many. It suffices to show that all implementable functions are eventually polynomial.

The proof proceeds by structural induction. 0 and 1 are polynomial. It's straightforward to show that sums, products, and differences of eventually polynomial functions are eventually polynomial: use the max of the two thresholds and the fact that the set of polynomials is closed under these operations. All that remains is closure under max.

Let f be eventually polynomial via a polynomial p, and g be eventually polynomial via a polynomial q. If p = q, then clearly x |-> max(f(x), g(x)) is eventually polynomial via the same polynomial. Otherwise, observe that p - q has finitely many real roots. Setting the threshold to an upper bound on the roots, we observe that the max function is eventually polynomial via p or q since the other case of the max never triggers here.