Numbers in ACL2
ACL2 numbers are precisely represented and unbounded. They can be partitioned into the following subtypes:
ACL2 Numbers | |- Rationals | | | |- Integers | | |- Positive integers 3 | | |- Zero 0 | | |- Negative Integers -3 | | | |- Non-Integral Rationals | | | | | |- Positive Non-Integral Rationals 19/3 | | |- Negative Non-Integral Rationals -22/7 | |- Complex Rational Numbers #c(3 5/2) ; i.e., 3 + (5/2)i
Signed integer constants are usually written (as illustrated above) as
sequences of decimal digits, possibly preceded by
Of course, 4/2 = 2/1 = 2 (i.e., not every rational written with a slash is a non-integer). Similarly, #c(4/2 0) = #c(2 0) = 2.
The common arithmetic functions and relations are denoted by
The primitive predicates for recognizing numbers are illustrated below. The following ACL2 function will classify an object, x, according to its numeric subtype, or else return 'NaN (not a number). We show it this way just to illustrate programming in ACL2.
(defun classify-number (x) (cond ((rationalp x) (cond ((integerp x) (cond ((< 0 x) 'positive-integer) ((= 0 x) 'zero) (t 'negative-integer))) ((< 0 x) 'positive-non-integral-rational) (t 'negative-non-integral-rational))) ((complex-rationalp x) 'complex-rational) (t 'NaN)))