What inputs would cause this function to not terminate?

Question

I am trying to prove this function in ACL2s/Lisp, but it is returning a stack overflow error, though I can't see the flaw in the code.

(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

Wouldn't any positive x and y cause this to overflow? Let's look at (foo 1 1).

Neither x nor y is zero, so it gets to the t branch of the cond, and calls:

(foo 0
     (foo 1 2))

Ok, let's evaluate the inner foo call:

(foo 1 2)

Similarly, it gets to the t branch of the cond, and calls:

(foo 0
     (foo 1 3))

Let's evaluate the inner foo:

(foo 1 3)

You can see where this is going. The t branch calls:

(foo 0
     (foo 1 4))

And so forth. This will happen anytime both x and y are nonzero. Where did you get this code? What are you trying to do with it? Running it's also a good idea to see what overflows. In this case, you would get stack overflows with nearly every possible call.