什么输入会导致此功能无法终止？

Question

我试图在ACL2s/Lisp中证明这个函数,但它返回一个堆栈溢出错误,虽然我看不到代码中的缺陷.

(defunc foo (x y)
 :input-contract (and (natp x) (natp y))
 :output-contract (natp (foo x y))
 (cond ((equal 0 x) (+ y 1))
       ((equal 0 y) (foo (- x 1) 1))
       (t (foo (- x 1) (foo x (+ y 1))))))

Answer 1

那不是任何积极x和y造成这种溢出？我们来看看吧(foo 1 1).

既不是x也不y是零,所以它到达tcond 的分支,并调用:

(foo 0
     (foo 1 2))

好吧,让我们评估一下内部foo呼叫:

(foo 1 2)

同样,它到达tcond 的分支,并调用:

(foo 0
     (foo 1 3))

让我们评估内心foo:

(foo 1 3)

你可以看到它的发展方向.该t分公司电话:

(foo 0
     (foo 1 4))

等等.这将在任何时候发生x,y并且非零.你从哪里得到这段代码？你想用它做什么？运行它也是一个好主意,看看溢出了什么.在这种情况下,几乎每个可能的调用都会出现堆栈溢出.