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

Posted 2023-05-08

【中文标题】仅使用加法、乘法、减法和最大值的整数除法

【英文标题】：Integer division using only addition, multiplication, subtraction and maximum

【发布时间】：2018-10-10 20:42:00

【问题描述】：

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

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

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

(not x) = (- 1 x) (abs x) = (- (max 0 (+ x x)) x) (min x y) = (- 0 (max (- 0 x) (- 0 y))) (nil x) = (not (min 1 (abs x)))

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

(if x y z) = (+ (* x y) (* (not x) z)) (eq x y) = (nil (- x y)) (ne x y) = (not (eq x y)) (le x y) = (nil (max 0 (- x y))) (gt x y) = (not (le x y)) (ge x y) = (le y x) (lt x y) = (not (ge x y))

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

(div x y) = ? (rem x y) = (- x (* y (div x y)))

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

【问题讨论】：

是否 ℤ 允许递归？

不，它不允许递归。绑定表格只是一种方便。不允许使用递归绑定表单。

这显然是不可能的，但我看不到证据。我想你最好在 cs.stackexchange 上尝试一下。

更简单的问题：你能用这种语言定义(odd x)吗？如果没有，那么(div x y) 就没有希望了。 （我会问(even x)，但似乎有一个隐含的要求，所有函数名称都是三个字母长......）

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

【参考方案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 情况。

【讨论】：

干得好；比我一直试图重构的符号逻辑证明更短更容易理解。

感谢您充实了我仓促神秘的回答作为评论！

【参考方案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

【讨论】：

是的，但是这种语言不支持递归。请注意，您在div 的定义中使用div。这是不允许的。绑定表单不是语言的一部分，而是递归绑定表单。它们只是避免编写长表达式的便利功能。

我明白了。我假设递归是因为语法使用递归。请编辑您的问题以区分绑定表格和法律语言字符串。

我做到了。 BNF 描述了合法的语言字符串。在介绍绑定表单之前，我确实提到它们只是为了方便。

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