0

这应该是一个函数的定义，如果输入的值是偶数自然数，则返回t，如果输入的值是奇数自然数，则返回nil：

(defun evec (n)
    (if (zp n)
        (if (zerop n)
            t
            nil)
        (evec (- n 2))))

当我输入一个偶数时，它会正确返回t并且它应该为其他任何东西返回nil但它没有！其实我猜它不会停止，我不明白为什么。当我输入像 -1 这样显然不是偶数自然数的数字时，我希望这段代码首先通过“if”，因为 (zp -1) 等于t，并且由于 -1 不等于 0，因此 (zerop - 1) 应该是nil，这意味着输出应该是nil并且程序应该终止。

事实上，我知道如何以实际工作的方式更好地实现这个功能，我只需要知道为什么这段代码不起作用，以便更好地理解这种语言，因为我刚刚开始学习 ACL2！...

谢谢您的考虑。

4

1 回答 1

2

查看 ACL2 文档，您想要的可能很简单：

(defun evec (n)
  (and (not (zp n))
       (evenp n)

因为zp对于任何不是自然数（大于零的整数）的对象（包括根本不是数字的对象）都会产生 true，所以以下应该成立：

(evec "string") -> nil
(evec -40 -> nil ;; in spite of -4 being even!
(evec 0) -> nil ;; in spite of 0 being even!
(evec 1) -> nil
(evec 2) -> t

Howeerzp有一个叫做“守卫”的东西，因为参数是自然数，所以上面忽略了守卫的问题。

如果正在检查守卫，那么evec如果输入不是自然数，由于将其参数传递给zp.

因此，只有上述(evec 1)和(evec 2)情况是合法的；其他人在里面违反了守卫zp。

（考虑到这一切，我们为什么要使用evec而不是evenp？也就是说，如果我们有一个X必须是自然的数字，为什么我们要通过测试均匀性的函数来验证这个事实？这似乎是一个强加给函数的无关紧要的次要责任。在数学中，自然数没有单独的均匀度定义。）

于 2021-06-23T18:47:40.403 回答