The module RAT extends INT with a binary division operator
_/_ to construct the rationals from integers and nonzero naturals.
Rationals can be input, and by default are output, in normal decimal notation;
however -5/42 is equivalent to -5 / 42, which is equivalent
to - 5 / 42, which really denotes - s_^5(0) / s_^42(0). The
command
set print rat off .
switches off the special printing for _/_ so that rational numbers will be printed with spaces around the foreslash sign. Note that set print number off also affects the printing of rational numbers, so with both number and rational pretty-printing switches turned off -5/42 is printed using the final notation given above.
The numerator and denominator of a rational may contain common factors but these are removed by a single built-in rewrite whenever the rational is reduced (thus _/_ is not a free constructor).
Notice that, in addition to the subsort NzRat of nonzero rational numbers, there is a subsort PosRat of positive rational numbers.
fmod RAT is
protecting INT .
sorts PosRat NzRat Rat .
subsorts NzInt < NzRat Int < Rat .
subsorts NzNat < PosRat < NzRat .
op _/_ : NzInt NzNat -> NzRat
[ctor prec 31 gather (E e) special (...)] .
vars I J : NzInt .
vars N M : NzNat .
var K : Int .
var Z : Nat .
var Q : NzRat .
var R : Rat .
The basic arithmetic operations on integers are extended to rational numbers as usual. The operator _/_ is declared special for the case when the first argument is of sort NzInt to enhance performance. The remaining operators are defined in Maude by equations and may do some rewriting even when their arguments are not properly constructed rationals. Note that the choice of equations for defining operators on the rationals is motivated by performance: simpler equations are possible in many cases but they turn out to incur a big performance penalty.
*** ARITHMETIC OPERATIONS
op _/_ : NzNat NzNat -> PosRat [ctor ditto] .
op _/_ : PosRat PosRat -> PosRat [ditto] .
op _/_ : NzRat NzRat -> NzRat [ditto] .
op _/_ : Rat NzRat -> Rat [ditto] .
eq 0 / Q = 0 .
eq I / - N = - I / N .
eq (I / N) / (J / M) = (I * M) / (J * N) .
eq (I / N) / J = I / (J * N) .
eq I / (J / M) = (I * M) / J .
op -_ : NzRat -> NzRat [ditto] .
op -_ : Rat -> Rat [ditto] .
eq - (I / N) = - I / N .
op _+_ : PosRat PosRat -> PosRat [ditto] .
op _+_ : PosRat Nat -> PosRat [ditto] .
op _+_ : Rat Rat -> Rat [ditto] .
eq I / N + J / M = (I * M + J * N) / (N * M) .
eq I / N + K = (I + K * N) / N .
op _-_ : Rat Rat -> Rat [ditto] .
eq I / N - J / M = (I * M - J * N) / (N * M) .
eq I / N - K = (I - K * N) / N .
eq K - J / M = (K * M - J ) / M .
op _*_ : PosRat PosRat -> PosRat [ditto] .
op _*_ : NzRat NzRat -> NzRat [ditto] .
op _*_ : Rat Rat -> Rat [ditto] .
eq Q * 0 = 0 .
eq (I / N) * (J / M) = (I * J) / (N * M).
eq (I / N) * K = (I * K) / N .
op _^_ : PosRat Nat -> PosRat [ditto] .
op _^_ : NzRat Nat -> NzRat [ditto] .
op _^_ : Rat Nat -> Rat [ditto] .
eq (I / N) ^ Z = (I ^ Z) / (N ^ Z) .
op abs : NzRat -> PosRat [ditto] .
op abs : Rat -> Rat [ditto] .
eq abs(I / N) = abs(I) / N .
The integer operations quo, rem, gcd, lcm,
min, and max are also extended to the rational numbers.
The operator quo gives the number of whole times a rational can
be divided by another, rem gives the rational remainder.
The operator gcd returns the largest rational that divides
into each of its arguments a whole number of times, while
lcm returns the smallest rational that is an integer multiple
of its arguments.
op _quo_ : PosRat PosRat -> Nat [ditto] .
op _quo_ : Rat NzRat -> Int [ditto] .
eq (I / N) quo Q = I quo (N * Q) .
eq K quo (J / M) = (K * M) quo J .
op _rem_ : Rat NzRat -> Rat [ditto] .
eq (I / N) rem (J / M) = ((I * M) rem (J * N)) / (N * M) .
eq K rem (J / M) = ((K * M) rem J) / M .
eq (I / N) rem J = (I rem (J * N)) / N .
op gcd : NzRat Rat -> PosRat [ditto] .
op gcd : Rat Rat -> Rat [ditto] .
eq gcd(I / N, R) = gcd(I, N * R) / N .
op lcm : NzRat NzRat -> PosRat [ditto] .
op lcm : Rat Rat -> Rat [ditto] .
eq lcm(I / N, R) = lcm(I, N * R) / N .
op min : PosRat PosRat -> PosRat [ditto] .
op min : NzRat NzRat -> NzRat [ditto] .
op min : Rat Rat -> Rat [ditto] .
eq min(I / N, R) = min(I, N * R) / N .
op max : PosRat Rat -> PosRat [ditto] .
op max : NzRat NzRat -> NzRat [ditto] .
op max : Rat Rat -> Rat [ditto] .
eq max(I / N, R) = max(I, N * R) / N .
Some examples involving these operations are the following:
Maude> red in RAT : 1/2 quo 1/3 . result NzNat: 1
Maude> red 1/2 rem 1/3 . result PosRat: 1/6
Maude> red gcd(1/2, 1/3) . result PosRat: 1/6
Maude> red lcm(1/2, 1/3) . result NzNat: 1
Tests on integers are extended to rational numbers. The test divides returns true if a rational number divides another rational number a whole number of times.
*** tests
op _<_ : Rat Rat -> Bool [ditto] .
eq (I / N) < (J / M) = (I * M) < (J * N) .
eq (I / N) < K = I < (K * N) .
eq K < (J / M) = (K * M) < J .
op _<=_ : Rat Rat -> Bool [ditto] .
eq (I / N) <= (J / M) = (I * M) <= (J * N) .
eq (I / N) <= K = I <= (K * N) .
eq K <= (J / M) = (K * M) <= J .
op _>_ : Rat Rat -> Bool [ditto] .
eq (I / N) > (J / M) = (I * M) > (J * N) .
eq (I / N) > K = I > (K * N) .
eq K > (J / M) = (K * M) > J .
op _>=_ : Rat Rat -> Bool [ditto] .
eq (I / N) >= (J / M) = (I * M) >= (J * N) .
eq (I / N) >= K = I >= (K * N) .
eq K >= (J / M) = (K * M) >= J .
op _divides_ : NzRat Rat -> Bool [ditto] .
eq (I / N) divides K = I divides N * K .
eq Q divides (J / M) = Q * M divides J .
There are four new operators: trunc, frac, floor, and ceiling. The operator floor converts a rational number to an integer by rounding down to the nearest integer, ceiling rounds up, and trunc rounds towards 0. The operator frac gives the fraction part of its argument and this always has the same sign as its argument.
*** ROUNDING
op trunc : PosRat -> Nat .
op trunc : Rat -> Int .
eq trunc(K) = K .
eq trunc(I / N) = I quo N .
op frac : Rat -> Rat .
eq frac(K) = 0 .
eq frac(I / N) = (I rem N) / N .
op floor : PosRat -> Nat .
op floor : Rat -> Int .
eq floor(K) = K .
eq floor(N / M) = N quo M .
eq floor(- N / M) = - ceiling(N / M) .
op ceiling : PosRat -> NzNat .
op ceiling : Rat -> Int .
eq ceiling(K) = K .
eq ceiling(N / M) = ((N + M) - 1) quo M .
eq ceiling(- N / M) = - floor(N / M) .
endfm
Here are some examples of reductions involving the rounding operators:
Maude> red in RAT : trunc(9/7) . result NzNat: 1
Maude> red floor(9/7) . result NzNat: 1
Maude> red ceiling(9/7) . result NzNat: 2
Maude> red frac(9/7) . result PosRat: 2/7
Maude> red trunc(-9/7) . result NzInt: -1
Maude> red floor(-9/7) . result NzInt: -2
Maude> red ceiling(-9/7) . result NzInt: -1
Maude> red frac(-9/7) . result NzRat: -2/7