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

Question

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

ℤ := 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)，要么证明不可能这样做。

Answer 1

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

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

用更实用的术语来说，我们正在进行重复减法。如果 x >= y，商加一，x 减 y，并递归。否则，return0.

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

Answer 2

这不可能。

调用函数 f : Z -> Z 最终多项式 如果存在一个多项式 p 具有整数系数和阈值 t 这样，对于每 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 的另一种情况永远不会在这里触发。

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

Integer division using only addition, multiplication, subtraction and maximum

algorithm

math

integer

logic

lambda-calculus