Rational numbers

Uses Integers. Requires special terms (rationalNumbers) that cannot be implemented in Leibniz itself. Rational number literals are written with a division slash, which may not be surrounded by spaces, e.g. 1/3 or -2/5.

The sort ℚ describes the rational numbers. The integers are a subsort: ℤ ⊆ ℚ.

There is a subsort ℚ.nz ⊆ ℚ for the non-zero rational numbers, with ℤ.nz ⊆ ℚ.nz.

Another subsort, ℚ.nn ⊆ ℚ, describes the non-negative rational numbers.

The positive rational numbers, ℚ.p, are both non-zero (ℚ.p ⊆ ℚ.nz) and non-negative (ℚ.p ⊆ ℚ.nn).

The natural numbers are always non-negative (ℕ ⊆ ℚ.nn), and the non-zero natural numbers are positive (ℕ.nz ⊆ ℚ.p).

Arithmetic

Addition

The sum of two rational numbers is a rational number:
 ℚ + ℚ : ℚ

Important special cases are:
 ℚ.p + ℚ.p : ℚ.p
 ℚ.nn + ℚ.nn : ℚ.nn

Addition is commutative:
 x:ℚ, y:ℚ, x + y = y + x
and associative:
 x:ℚ, y:ℚ, z:ℚ, (x + y) + z = x + (y + z)

Rules:

Eliminate zeros:
 (x:ℚ) + (zero:zero) ⇒ x
 (zero:zero) + (x:ℚ) ⇒ x

Evaluation for number terms:
 (x:ℚ) + (y:ℚ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x + y"

Subtraction

The difference between two rational numbers is a rational number:
 ℚ - ℚ : ℚ

The negative of a rational number is a rational number:
 -(ℚ) : ℚ

Rules:

Eliminate zeros:
 (x:ℚ) - (zero:zero) ⇒ x
 (zero:zero) - (x:ℚ) ⇒ -(x)

Evaluation for number terms:
 (x:ℚ) - (y:ℚ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x - y"
 -(x:ℚ) ⇒ Pharo:"x ensureNumber. x negated"

Multiplication

The product of two rational numbers is a rational number:
 ℚ × ℚ : ℚ

Important special cases are:
 ℚ.p × ℚ.p : ℚ.p
 ℚ.nn × ℚ.nn : ℚ.nn
 ℚ.nz × ℚ.nz : ℚ.nz

Multiplication is commutative:
 x:ℚ, y:ℚ, x × y = y × x
and associative:
 x:ℚ, y:ℚ, z:ℚ, (x × y) × z = x × (y × z)

Addition is distributive over multiplication:
 x:ℚ, y:ℚ, z:ℚ, x × (y + z) = (x × y) + (x × z)

Rules:

Eliminate zeros:
 (x:ℚ) × (zero:zero) ⇒ 0
 (zero:zero) × (x:ℚ) ⇒ 0

Eliminate ones:
 (one:one) × (x:ℚ) ⇒ x
 (x:ℚ) × (one:one) ⇒ x

Evaluate for number terms:
 (x:ℚ) × (y:ℚ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x * y"

Division

The quotient of a rational number and a non-zero rational number is a rational number:
 ℚ ÷ ℚ.nz : ℚ

Important special cases are:
 ℚ.nz ÷ ℚ.nz : ℚ.nz
 ℚ.nn ÷ ℚ.p : ℚ.nn
 ℚ.p ÷ ℚ.p : ℚ.p

Rules:

Elimination of zeros and ones:
 (z:zero) ÷ (x:ℚ.nz) ⇒ 0
 (x:ℚ) ÷ (one:one) ⇒ x

Evaluate for number terms:
 (x:ℚ) ÷ (y:ℚ.nz) ⇒ Pharo:"x ensureNumber. y ensureNumber. x / y"

Note that division by zero is excluded by the definition of the division operator. 1 ÷ 0 : [ℚ] has no sort, only a kind, which is an error indicator. There is no rewrite rule either that would transform this term into a valid one.

Exponentiation

Exponentiation is defined for non-zero rational number to any integer power:
 ℚ.nzℤ.nz : ℚ.nz
 ℚ.nzzero : ℕ.nz

An important special case is:
 ℚ.pℤ.nz : ℚ.p

Rules:

Eliminate zeros:
 (x:ℚ.nz)z:zero ⇒ 1
 (z:zero)x:ℕ.nz ⇒ 0

Eliminate ones:
 (x:ℚ.nz)one:one ⇒ x

Evaluate for number terms:
 (x:ℤ)y:ℕ.nz ⇒ Pharo:"x raisedTo: y"
 (x:ℚ.nz)y:ℤ.nz ⇒ Pharo:"x raisedTo: y"

Comparison

ℚ < ℚ : 𝔹
ℚ > ℚ : 𝔹
ℚ ≤ ℚ : 𝔹
ℚ ≥ ℚ : 𝔹

Evaluation rules for number terms:
 (x:ℚ) < (y:ℚ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x < y"
 (x:ℚ) > (y:ℚ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x > y"
 (x:ℚ) ≤ (y:ℚ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x <= y"
 (x:ℚ) ≥ (y:ℚ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x >= y"