仅使用加法、乘法、减法和最大值的整数除法

Question

假设我们有一种编程语言ℤ，它的语法如下：

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

为方便起见，我们可以在我们的语言中定义新的绑定形式如下：

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)))

这种语言足够强大，可以表达分支和比较运算符：

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))

现在，问题是我们是否可以定义整数除法是这种语言：

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

我认为不可能定义(div x y)，因为ℤ 没有循环。但是，我不知道如何证明这一点。请注意，如果可能，那么(div x 0) 的结果无关紧要。因此，要么定义(div x y)，要么证明不可能这样做。

Answer 1

这是不可能的。

如果存在具有整数系数和阈值t 的多项式p，则调用函数f : Z -> Z 最终多项式，这样，对于每个x > t，我们都有f(x) = p(x)。设d(x) = [x/2] 为楼层除以二。 d 最终不是多项式，因为d 的差序列有无限多个零（f(2y) = y = f(2y+1) 对所有y），而每个非常数多项式的差序列有有限多个。足以证明所有可实现的函数最终都是多项式的。

证明通过结构归纳进行。 0 和 1 是多项式。很容易证明最终多项式函数的和、乘积和差最终是多项式：使用两个阈值的最大值以及多项式集合在这些操作下是封闭的事实。剩下的就是在max 下关闭。

让f 通过多项式p 最终成为多项式，而g 通过多项式q 最终成为多项式。如果p = q，那么显然x |-> max(f(x), g(x)) 最终是通过相同多项式的多项式。否则，观察p - q 有有限多个实根。将阈值设置为根的上限，我们观察到 max 函数最终是通过 p 或 q 的多项式，因为这里不会触发其他 max 情况。

Answer 2

递归和分支的组合会给你循环。

(div x y) = (iff gte(x y) (+ 1 (div((- x y) y))) 0)

在更多功能方面，我们正在做重复减法。如果 x >= y，则将商加一，从 x 中减去 y，然后重复。否则，返回 0。

if x >=y
    return 1 + div(x-y y)
else
    return 0