ACL2 function to recognize even numbers does not halt

Question

This is supposed to be a definition of a function which returns t if the entered value is an even natural number and returns nil if the entered value is an odd natural number:

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

It correctly returns t when I enter an even number and It's supposed to return nil literally for anything else but it doesn't! Actually I guess it does not halt and I don't understand why. When I enter a number like -1 which is obviously not an even natural number, I expect from this code to go through first 'if' because (zp -1) equals t and since -1 is not equal to 0 then (zerop -1) should be nil which means that the output should be nil and the program should terminate.

In fact I know how to implement this function better in way that it actually work and all I need to know is why this code doesn't work, in order to understand this language better because I've just started learning ACL2!...

Thank you for your consideration.

Answer 1

Looking at ACL2 documentation, what you want could be as simple as:

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

Because zp yields true for any object that is not a natural number (integer greater than zero), including objects that are not numbers at all, the following should hold:

(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

Howeer, zp has something called a "guard" for the argument being a natural number, so the above ignore the issue of guards.

If guards are being checked then evec will somehow blow up if the input isn't a natural number, due to passing its argument to zp.

Thus only the (evec 1) and (evec 2) cases above are legitimate; the others violate the guard in zp.

(Given all that, why would we ever want to use evec rather than evenp? That is to say, if we have a number X which must be natural, why would we want that fact to be validated by the function which tests evenness? It seems like an irrelevant secondary responsibility to foist onto a function. In mathematics, there isn't a separate definition of evenness for natural numbers.)