Search code examples
schemelispstack-overflowtermination

What inputs would cause this function to not terminate?

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))))))
Solution

  • 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.