2.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. Takes one or more arguments.

Examples:

> (- 5)

-5

> (- 5 3)

2

> (- 10 5 3 1)

eval:1234:0: -: Expects only one or two arguments, but

given 4 in: (- 10 5 3 1)

> (-)

eval:1237:0: -: Expects only one or two arguments, but

given 0 in: (-)

(/ 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

> (/)

eval:1246:0: /: Expected one or two arguments, but got 0

in: (/)

> (/ 100 5 2)

eval:1249:0: /: Expected one or two arguments, but got 3

in: (/ 100 5 2)

(1+ num)

Adds 1 to the given number.

Examples:

> (1+ 1)

2

> (1+)

eval:1255:0: 1+: Expected 1 arguments, but got 0 in: (1+)

> (1+ 1 2)

eval:1258:0: 1+: Expected 1 arguments, but got 2 in: (1+ 1

2)

(1- num)

Subtracts 1 from the given number.

Examples:

> (1- 1)

0

> (1-)

eval:1264:0: 1-: Expected 1 arguments, but got 0 in: (1-)

> (1- 1 2)

eval:1267:0: 1-: Expected 1 arguments, but got 2 in: (1- 1

2)

(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-* 1)

eval:1273:0: binary-*: Expected 2 arguments, but got 1 in:

(binary-* 1)

> (binary-* "5" 10)

*: expects type <number> as 1st argument, given: "5"; other

arguments were: 10

(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

> (binary-+ 1)

eval:1282:0: binary-+: Expected 2 arguments, but got 1 in:

(binary-+ 1)

> (binary-+ "5" 10)

+: expects type <number> as 1st argument, given: "5"; other

arguments were: 10

(/= 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

> (/= "3" 2)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> acl2-number? acl2-number? any) on here;

expected <acl2-number?>, given: "3"

(< 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

> (minusp (complex 1 2))

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> rational? any) on here; expected <rational?>,

given: 1+2i

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

()

> (oddp 1/2)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> integer? any) on here; expected <integer?>,

given: 1/2

(plusp x) → t

x : (real/rationalp x)

Determines if x is positive.

Examples:

> (plusp 1)

t

> (plusp -1)

()

> (plusp 1/2)

t

> (plusp (complex 1 2))

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> rational? any) on here; expected <rational?>,

given: 1+2i

(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

> (abs (complex 1 1))

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> rational? any) on here; expected <rational?>,

given: 1+1i

(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

> (ceiling "5" 3)

/: expects type <number> as 1st argument, given: "5"; other

arguments were: 3

(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

> (complex (complex 2 3) 5)

2+8i

(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

> (denominator (complex 1 2))

denominator: expects argument of type <rational number>;

given 1+2i

(evenp x) → t

x : (integerp x)

Determines if x is even.

Examples:

> (evenp 1)

()

> (evenp 2)

t

> (evenp 1/2)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> integer? any) on here; expected <integer?>,

given: 1/2

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

> (explode-nonnegative-integer -100 16 nil)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> natural-number/c (or/c (=/c 2) (=/c

8) (=/c 10) (=/c 16)) any/c any) on here; expected

<natural-number/c>, given: -100

(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

> (expt 10 1/2)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> acl2-number? integer? any) on here;

expected <integer?>, given: 1/2

> (expt 0 -2)

expt: undefined for 0 and -2

(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

> (floor "5" 3)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> rational? non-zero-real/rational? any) on

here; expected <rational?>, given: "5"

(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

> (imagpart "5")

imag-part: expects argument of type <number>; given "5"

(int= i j)

Checks to see if the two integers i and j are equal. This is like equal and =, but with the 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

> (int= 1/2 1/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

> (integer-length 1/2)

0

(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

> (max 4)

eval:1606:0: max: Expected 2 arguments, but got 1 in: (max

4)

> (max (complex 1 2) 2)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> rational? rational? any) on here; expected

<rational?>, given: 1+2i

(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

> (min 4)

eval:1618:0: min: Expected 2 arguments, but got 1 in: (min

4)

> (min (complex 1 2))

eval:1621:0: min: Expected 2 arguments, but got 1 in: (min

(complex 1 2))

(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

> (mod 8 0)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> rational? non-zero-real/rational? any) on

here; expected <non-zero-real/rational?>, given: 0

(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

> (numerator (complex 1 2))

numerator: expects argument of type <rational number>;

given 1+2i

(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

> (rem (complex 1 2) 3)

numerator: expects argument of type <rational number>;

given 1/3+2/3i

(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

> (round (complex 1 2) 3)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> rational? rational? any) on here; expected

<rational?>, given: 1/3+2/3i

(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

> (truncate (complex 1 2) 3)

numerator: expects argument of type <rational number>;

given 1/3+2/3i

(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-- "5")

-: expects argument of type <number>; given "5"

(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

> (unary-/ 0)

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> non-zero-acl2-number? any) on here;

expected <non-zero-acl2-number?>, given: 0

> (unary-/ "5")

/Volumes/Maldis/Users/cce/plt/research/dracula/release/src/l

anguage/checking-proc.scm:36:21: Dracula program broke the

contract (-> non-zero-acl2-number? any) on here;

expected <non-zero-acl2-number?>, given: "5"