只使用加法，乘法，减法和最大值运算进行整数除法

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)或证明不可能这样做。

- Aadit M Shah

---

ℤ 允许递归吗？ - stf

不，它不允许递归。绑定形式只是一种方便。不允许递归绑定形式。 - Aadit M Shah

这显然是不可能的，但我找不到证据。我猜你最好去cs.stackexchange试试看。 - Paul Hankin

更简单的问题：你能在这种语言中定义(odd x)吗？如果不能，那么(div x y)就没有希望了。 （我本来想问(even x)的，但看起来所有函数名称都必须是三个字母长的隐含要求...） - Mark Dickinson

我相信你应该能够证明（例如通过结构归纳），任何在这种语言中可表达的单变量x函数最终都是一个多项式：也就是说，存在某个整数x0和多项式p，使得对于所有超过x0的x，f(x)等于p(x)。然后，这应该证明了(odd x)是不可能的（因此无法构造(rem x y)和(div x y)）。 - Mark Dickinson

Answer 1

这是不可能的。

如果存在一个整数系数多项式 p 和阈值 t，使得对于每个大于 t 的 x，我们都有 f(x) = p(x)，则称函数 f: Z -> Z 最终为多项式。将 d(x) = [x/2] 定义为整除二的向下取整操作。由于差分序列中有无限多个零点（对于所有的 y，都有 f(2y) = y = f(2y+1)），因此 d 不是最终为多项式的函数。而对于所有可实现的函数，它们都是最终为多项式的。

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

设 f 是通过多项式 p 最终为多项式的函数，g 是通过多项式 q 最终为多项式的函数。如果 p = q，则显然 x |-> max(f(x), g(x)) 也是通过相同的多项式最终为多项式的。否则，观察到 p - q 有有限个实根。将阈值设为这些根的上界，我们可以得出 max 函数通过 p 或 q 最终为多项式，因为另一种情况下的 max 永远不会被触发。

- David Eisenstat

---

做得好；比我一直试图重建的符号逻辑证明更短更易懂。 - Prune

感谢您详细解释我的仓促而晦涩的评论回答！ - Mark Dickinson

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

- Prune

---

是的，但是这种语言不支持递归。请注意，在“div”的定义中使用了“div”。这是不允许的。绑定形式不是该语言的一部分，更不用说递归绑定形式了。它们只是一种方便的功能，可以避免编写冗长的表达式。 - Aadit M Shah

我明白了。我之前以为是递归，因为语法使用了递归。请编辑您的问题，区分绑定形式和法律语言字符串。 - Prune

我做了。BNF描述了合法的语言字符串。在我介绍绑定形式之前，我提到它们只是为了方便。 - Aadit M Shah

请注意，即使 ℤ 支持递归，您的函数仍然是错误的。如果除数为负整数且小于被除数，则它永远不会终止，否则当被除数为负整数时，它会错误地返回 0。 - Aadit M Shah