假设我们有一种编程语言ℤ,它具有以下语法:
ℤ := 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)
或证明不可能这样做。
(odd x)
吗?如果不能,那么(div x y)
就没有希望了。 (我本来想问(even x)
的,但看起来所有函数名称都必须是三个字母长的隐含要求...) - Mark Dickinsonx
函数最终都是一个多项式:也就是说,存在某个整数x0
和多项式p
,使得对于所有超过x0
的x
,f(x)
等于p(x)
。然后,这应该证明了(odd x)
是不可能的(因此无法构造(rem x y)
和(div x y)
)。 - Mark Dickinson