1.4.5 Rational and Complex Arithmetic

(* num ...)

Multiplies the given numbers together, taking any number of arguments. This is a macro that expands into calls of the function binary-*

Examples:

> (*)

1

> (* 2)

2

> (* 1 2 3)

6

(+ num ...)

Adds the given numbers together, taking any number of arguments. This is a macro that expands into calls of the function binary-+.

Examples:

> (+)

0

> (+ 2)

2

> (+ 1 2 3)

6

(- num num)

Subtracts the given numbers. If only one argument is given, returns the negation of the input.

Examples:

> (- 5)

-5

> (- 5 3)

2

(/ num num)

Divides the first number by the second. If only one argument is given, returns the reciprocal of the input.

Examples:

> (/ 2)

1/2

> (/ 16 4)

4

(1+ num)

Adds 1 to the given number.

Examples:

> (1+ 1)

2

(1- num)

Subtracts 1 from the given number.

Examples:

> (1- 1)

0

(binary-* x y) → t

x : (acl2-numberp x)

y : (acl2-numberp y)

Takes exactly two numbers and multiplies them together.

Examples:

> (binary-* 9 8)

72

(binary-+ x y) → t

x : (acl2-numberp x)

y : (acl2-numberp y)

Takes exactly two numbers and adds them together.

Examples:

> (binary-+ 9 8)

17

(/= x y) → t

x : (acl2-numberp x)

y : (acl2-numberp y)

Determines if the given numbers are not equal. Logically equivalent to (not (equal x y))

Examples:

> (/= 2 2)

()

> (/= 3 2)

t

(< x y) → t

x : (rationalp x)

y : (rationalp y)

Determines if x is less than y.

Examples:

> (< 1 2)

t

> (< 2 1)

()

> (< 2 2)

()

(<= x y) → t

x : (rationalp x)

y : (rationalp y)

Determines if x is less than or equal to y.

Examples:

> (<= 1 2)

t

> (<= 2 1)

()

> (<= 2 2)

t

(= x y) → t

x : (acl2-numberp x)

y : (acl2-numberp y)

Determines if x is equal to y. This is like equal, but has the guard that both of its arguments must be numbers. It usually executes more efficiently thatn equal.

Examples:

> (= 1 2)

()

> (= 2 1)

()

> (= 2 2)

t

(> x y) → t

x : (rationalp x)

y : (rationalp y)

Determines if x is greater than y.

Examples:

> (> 1 2)

()

> (> 2 1)

t

> (> 2 2)

()

(>= x y) → t

x : (rationalp x)

y : (rationalp y)

Determines if x is greater than or equal to y.

Examples:

> (>= 1 2)

()

> (>= 2 1)

t

> (>= 2 2)

t

(acl2-numberp x)

Returns true if and only if x is a rational or complex rational number.

Examples:

> (acl2-numberp 1)

t

> (acl2-numberp 12/5)

t

> (acl2-numberp "no")

()

(complex-rationalp z)

Determines if z is a complex number consisting of rational parts.

Examples:

> (complex-rationalp 3)

()

> (complex-rationalp (complex 3 0))

()

> (complex-rationalp t)

()

> (complex-rationalp (complex 3 1))

t

(complex/complex-rationalp z) → t

z : t

For most cases, this is simply a macro abbreviating complex-rationalp.

Examples:

> (complex/complex-rationalp 3)

()

> (complex/complex-rationalp (complex 3 0))

()

> (complex/complex-rationalp t)

()

> (complex/complex-rationalp (complex 3 1))

t

(minusp x) → t

x : (real/rationalp x)

Determines whether x is a negative number.

Examples:

> (minusp 1)

()

> (minusp -1)

t

(natp x) → t

x : t

Determines if x is a natural number.

Examples:

> (natp 1)

t

> (natp 0)

t

> (natp -1)

()

(oddp x) → t

x : (integerp x)

Determines if x is odd.

Examples:

> (oddp 3)

t

> (oddp 2)

()

(plusp x) → t

x : (real/rationalp x)

Determines if x is positive.

Examples:

> (plusp 1)

t

> (plusp -1)

()

> (plusp 1/2)

t

(posp x) → t

x : t

Determines if x is a positive integer.

Examples:

> (posp 1)

t

> (posp -1)

()

> (posp 1/2)

()

> (posp (complex 1 2))

()

> (posp "asdf")

()

(rationalp x)

Determines if x is a rational number.

Examples:

> (rationalp 2/5)

t

> (rationalp 2)

t

> (rationalp (complex 1 2))

()

> (rationalp "number")

()

(real/rationalp x)

In most cases, this is just a macro abbreviating rationalp.

Examples:

> (real/rationalp 2/5)

t

> (real/rationalp "number")

()

(abs x) → t

x : (real/rationalp x)

Computes the absolute value of x.

Examples:

> (abs 1)

1

> (abs -1)

1

(ceiling i j) → t

i : (real/rationalp i)

j : (and (real/rationalp j) (not (eql j 0)))

Returns the smallest integer greater the value of (/ i j).

Examples:

> (ceiling 4 2)

2

> (ceiling 4 3)

2

(complex n i) → t

n : (rationalp n)

i : (rationalp i)

Creates a complex number with real part n and imaginary part i.

Examples:

> (complex 2 1)

2+1i

> (complex 2 0)

2

> (complex 0 2)

0+2i

> (complex 1/2 3/2)

1/2+3/2i

(conjugate x) → t

x : (acl2-numberp x)

Computes the complex conjugate of x (the result of negating its imaginary part).

Examples:

> (conjugate (complex 3 1))

3-1i

(denominator x) → t

x : (rationalp x)

Returns the divisor of a rational number in lowest terms.

Examples:

> (denominator 5)

1

> (denominator 5/3)

3

> (denominator 5/3)

3

(evenp x) → t

x : (integerp x)

Determines if x is even.

Examples:

> (evenp 1)

()

> (evenp 2)

t

(explode-nonnegative-integer n r) → l

n : (and (integerp n) (>= n 0))

r : (print-base-p r)

Returns a list of characters representing n in base-r, and appends l to the end.

Examples:

> (explode-nonnegative-integer 925 10 nil)

(#\9 #\2 #\5)

> (explode-nonnegative-integer 325 16 nil)

(#\1 #\4 #\5)

> (explode-nonnegative-integer 325 16 (list 'a 'b 'c))

(#\1 #\4 #\5 a b c)

> (explode-nonnegative-integer 325 16 'a)

(#\1 #\4 #\5 . a)

(expt i j) → t

i : (acl2-numberp i)

j : (and (integerp j) (not (and (eql i 0) (< j 0))))

Raises i to the jth power.

Examples:

> (expt 10 2)

100

> (expt 10 -2)

1/100

(fix x) → t

x : t

Coerces x to a number. If x is a number, (fix x) returns the argument unchanged. Otherwise, it returns 0.

Examples:

> (fix 20)

20

> (fix 2/3)

2/3

> (fix "hello")

0

> (fix nil)

0

(floor i j) → t

i : (real/rationalp i)

j : (and (real/rationalp j) (not (eql j 0)))

Returns the greatest integer not exceeding the value of (/ i j).

Examples:

> (floor 4 2)

2

> (floor 4 3)

1

(ifix [x t])

#<procedure:t>Coerces x to an integer. If x is an integer, (ifix x) returns the argument unchanged. Otherwise, it returns 0.

Examples:

> (ifix 16)

16

> (ifix 22/3)

0

> (ifix "hello")

0

(imagpart i) → t

i : (acl2-numberp i)

Returns the imaginary part of a complex number.

Examples:

> (imagpart (complex 3 2))

2

> (imagpart 5)

0

(int= i j)

Checks to see if the two integers i and j are equal. This is like equal and =, but with the added guard that the inputs are integers. This generally executes more efficiently on integers than equal or =.

Examples:

> (int= 1 2)

()

> (int= 2 1)

()

> (int= 2 2)

t

(integer-length x) → t

x : (integerp x)

Returns the number of bits in the two’s complement binary representation of x.

Examples:

> (integer-length 12)

4

> (integer-length 1234)

11

(integerp x)

Determines whether x is an integer.

Examples:

> (integerp 12)

t

> (integerp '12)

t

> (integerp nil)

()

(max i j) → t

i : (real/rationalp i)

j : (real/rationalp j)

Returns the greater of the two given numbers.

Examples:

> (max 1 2)

2

> (max 4 3)

4

(min i j) → t

i : (real/rationalp i)

j : (real/rationalp j)

Returns the lesser of the two given numbers.

Examples:

> (min 1 2)

1

> (min 4 3)

3

(mod i j) → t

i : (real/rationalp i)

j : (and (real/rationalp j) (not (eql j 0)))

Computes the remainder of dividing i by j.

Examples:

> (mod 4 2)

0

> (mod 8 3)

2

(nfix x) → t

x : t

Coerces x to a natural number. If x is a natural number, (nfix x) returns the argument unchanged. Otherwise, it returns 0.

Examples:
> (nfix 1)
1
> (nfix -1)
0
> (nfix 1/2)
0
> (nfix "5")
0

(nonnegative-integer-quotient x y) → t

x : (and (integerp x) (not (< x 0)))

y : (and (integerp j) (< 0 j))

Returns the integer quotient of x and y. That is, (nonnegative-integer-quotient x y) is the largest integer k such that (* j k) is less than or equal to x.

Examples:

> (nonnegative-integer-quotient 14 3)

4

> (nonnegative-integer-quotient 15 3)

5

(numerator x) → t

x : (rationalp x)

Returns the dividend of a rational number in lowest terms.

Examples:

> (numerator 4)

4

> (numerator 6/7)

6

> (numerator 1/2)

1

(realfix x) → t

x : t

Coerces x to a real number. If x satisfies (real/rationalp x), then it returns the argument unchanged. Otherwise, returns 0.

Examples:

> (realfix 2/5)

2/5

> (realfix (complex 3 2))

0

> (realfix "5")

0

(realpart x) → t

x : (acl2-numberp x)

Returns the real part of a complex number.

Examples:

> (realpart (complex 3 2))

3

> (realpart 1/2)

1/2

(rem i j) → t

i : (real/rationalp i)

j : (and (real/rationalp j) (not (eql j 0)))

Calculates the remainder of (/ i j) using truncate.

Examples:

> (rem 4 2)

0

> (rem 8 3)

2

(rfix x) → t

x : t

Coerces x into a rational number. If x is a rational number, then it returns x unchanged. Otherwise, it returns 0.

Examples:

> (rfix 2/5)

2/5

> (rfix (complex 3 2))

0

> (rfix "5")

0

(round i j) → t

i : (real/rationalp i)

j : (real/rationalp j)

Rounds (/ i j) to the nearest integer. When the quotient is exactly halfway between to integers, it rounds to the even one.

Examples:
> (round 4 2)
2
> (round 3 2)
2
> (round 5 2)
2
> (round 4 3)
1

(signum x) → t

x : (real/rationalp x)

Returns 0 if x is 0, -1 if it is negative, and 1 if it is positive.

Examples:

> (signum 5)

1

> (signum 0)

0

> (signum -5)

-1

(truncate i j) → t

i : (real/rationalp i)

j : (and (real/rationalp j) (not (eql j 0)))

Computes (/ i j) and rounds down to the nearest integer.

Examples:
> (truncate 5 2)
2
> (truncate 4 2)
2
> (truncate 19 10)
1
> (truncate 1 10)
0

(unary-- x) → t

x : (acl2-numberp x)

Computes the negative of the input.

Examples:

> (unary-- 5)

-5

> (unary-- -5)

5

> (unary-- (complex 1 -2))

-1+2i

(unary-/ x) → t

x : (and (acl2-numberp x) (not (eql x 0)))

Computes the reciprocal of the input.

Examples:

> (unary-/ 5)

1/5

> (unary-/ 1/5)

5

> (unary-/ (complex 1 2))

1/5-2/5i