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

假设我们有一种编程语言ℤ,它具有以下语法:

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

不可能.

如果存在具有整数系数和阈值的多项式,则调用函数f : Z -> Z 最终多项式,使得对于每个我们具有.让我们分两次.最终不是多项式,因为差分序列具有无穷多个零(对于所有),而每个非常数多项式的差分序列具有有限多个.足以证明所有可实现的函数最终都是多项式的.ptx > tf(x) = p(x)d(x) = [x/2]ddf(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的另一种情况在此处不会触发.