Rational Numbers in K

K provides support for arbitrary-precision rational numbers represented as a quotient between two integers. The sort representing these values is Rat. Int is a subsort of Rat, and it is guaranteed that any integer will be represented as an Int and can be matched as such on the left hand side of rules. K also supports the usual arithmetic operators over rational numbers.

module RAT-SYNTAX imports INT-SYNTAX imports private BOOL syntax Rat syntax Rat ::= Int


You can:

  • Raise a rational number to any negative or nonnegative integer.
  • Multiply or divide two rational numbers to obtain a product or quotient.
  • Add or subtract two rational numbers to obtain a sum or difference.
syntax Rat ::= left: Rat "^Rat" Int [function, total, klabel(_^Rat_), symbol, smtlib(ratpow), hook(RAT.pow)] > left: Rat "*Rat" Rat [function, total, klabel(_*Rat_), symbol, left, smtlib(ratmul), hook(RAT.mul)] | Rat "/Rat" Rat [function, klabel(_/Rat_), symbol, left, smtlib(ratdiv), hook(RAT.div)] > left: Rat "+Rat" Rat [function, total, klabel(_+Rat_), symbol, left, smtlib(ratadd), hook(RAT.add)] | Rat "-Rat" Rat [function, total, klabel(_-Rat_), symbol, left, smtlib(ratsub), hook(RAT.sub)]


You can determine whether two rational numbers are equal, unequal, or compare one of less than, less than or equalto, greater than, or greater than or equal to the other:

syntax Bool ::= Rat "==Rat" Rat [function, total, klabel(_==Rat_), symbol, smtlib(rateq), hook(RAT.eq)] | Rat "=/=Rat" Rat [function, total, klabel(_=/=Rat_), symbol, smtlib(ratne), hook(RAT.ne)] | Rat ">Rat" Rat [function, total, klabel(_>Rat_), symbol, smtlib(ratgt), hook(RAT.gt)] | Rat ">=Rat" Rat [function, total, klabel(_>=Rat_), symbol, smtlib(ratge), hook(RAT.ge)] | Rat "<Rat" Rat [function, total, klabel(_<Rat_), symbol, smtlib(ratlt), hook(RAT.lt)] | Rat "<=Rat" Rat [function, total, klabel(_<=Rat_), symbol, smtlib(ratle), hook(RAT.le)]


You can compute the minimum and maximum of two rational numbers:

syntax Rat ::= minRat(Rat, Rat) [function, total, klabel(minRat), symbol, smtlib(ratmin), hook(RAT.min)] | maxRat(Rat, Rat) [function, total, klabel(maxRat), symbol, smtlib(ratmax), hook(RAT.max)]

Conversion to Floating Point

You can convert a rational number to the nearest floating point number that is representable in a Float of a specified number of precision and exponent bits:

syntax Float ::= Rat2Float(Rat, precision: Int, exponentBits: Int) [function] endmodule

Implementation of Rational Numbers

The remainder of this file consists of an implementation in K of the operations listed above. Users of the RAT module should not use any of the syntax defined in any of these modules.

As a point of reference for users, it is worth noting that rational numbers are normalized to a canonical form by this module,. with the canonical form bearing the property that it is either an Int, or a pair of integers I /Rat J such that I =/=Int 0 andBool J >=Int 2 andBool gcdInt(I, J) ==Int 1 is always true.

module RAT-COMMON imports RAT-SYNTAX // invariant of < I , J >Rat : I =/= 0, J >= 2, and I and J are coprime syntax Rat ::= "<" Int "," Int ">Rat" [format(%2 /Rat %4)] endmodule module RAT-SYMBOLIC [symbolic] imports private RAT-COMMON imports ML-SYNTAX imports private BOOL rule #Ceil(@R1:Rat /Rat @R2:Rat) => {(@R2 =/=Rat 0) #Equals true} #And #Ceil(@R1) #And #Ceil(@R2) [simplification] endmodule module RAT-KORE imports private RAT-COMMON imports private K-EQUAL /* * equalities */ // NOTE: the two rules below may not work correctly in non-kore backends rule R ==Rat S => R ==K S rule R =/=Rat S => R =/=K S endmodule module RAT [private] imports private RAT-COMMON imports public RAT-SYMBOLIC imports public RAT-KORE imports public RAT-SYNTAX imports private INT imports private BOOL /* * arithmetic */ rule < I , I' >Rat +Rat < J , J' >Rat => ((I *Int J') +Int (I' *Int J)) /Rat (I' *Int J') rule I:Int +Rat < J , J' >Rat => ((I *Int J') +Int J) /Rat J' rule < J , J' >Rat +Rat I:Int => I +Rat < J , J' >Rat rule I:Int +Rat J:Int => I +Int J rule < I , I' >Rat *Rat < J , J' >Rat => (I *Int J) /Rat (I' *Int J') rule I:Int *Rat < J , J' >Rat => (I *Int J) /Rat J' rule < J , J' >Rat *Rat I:Int => I *Rat < J , J' >Rat rule I:Int *Rat J:Int => I *Int J rule < I , I' >Rat /Rat < J , J' >Rat => (I *Int J') /Rat (I' *Int J) rule I:Int /Rat < J , J' >Rat => (I *Int J') /Rat J rule < I , I' >Rat /Rat J:Int => I /Rat (I' *Int J) requires J =/=Int 0 rule I:Int /Rat J:Int => makeRat(I, J) requires J =/=Int 0 // derived rule R -Rat S => R +Rat (-1 *Rat S) // normalize syntax Rat ::= makeRat(Int, Int) [function] | makeRat(Int, Int, Int) [function] rule makeRat(0, J) => 0 requires J =/=Int 0 rule makeRat(I, J) => makeRat(I, J, gcdInt(I,J)) requires I =/=Int 0 andBool J =/=Int 0 // makeRat(I, J, D) is defined when I =/= 0, J =/= 0, D > 0, and D = gcd(I,J) rule makeRat(I, J, D) => I /Int D requires J ==Int D // implies J > 0 since D > 0 rule makeRat(I, J, D) => < I /Int D , J /Int D >Rat requires J >Int 0 andBool J =/=Int D rule makeRat(I, J, D) => makeRat(0 -Int I, 0 -Int J, D) requires J <Int 0 // gcdInt(a,b) computes the gcd of |a| and |b|, which is positive. syntax Int ::= gcdInt(Int, Int) [function, public] rule gcdInt(A, 0) => A requires A >Int 0 rule gcdInt(A, 0) => 0 -Int A requires A <Int 0 rule gcdInt(A, B) => gcdInt(B, A %Int B) requires B =/=Int 0 // since |A %Int B| = |A| %Int |B| /* * exponentiation */ rule _ ^Rat 0 => 1 rule 0 ^Rat N => 0 requires N =/=Int 0 rule < I , J >Rat ^Rat N => powRat(< I , J >Rat, N) requires N >Int 0 rule X:Int ^Rat N => X ^Int N requires N >Int 0 rule X ^Rat N => (1 /Rat X) ^Rat (0 -Int N) requires X =/=Rat 0 andBool N <Int 0 // exponentiation by squaring syntax Rat ::= powRat(Rat, Int) [function] // powRat(X, N) is defined when X =/= 0 and N > 0 rule powRat(X, 1) => X rule powRat(X, N) => powRat(X *Rat X, N /Int 2) requires N >Int 1 andBool N %Int 2 ==Int 0 rule powRat(X, N) => powRat(X, N -Int 1) *Rat X requires N >Int 1 andBool N %Int 2 =/=Int 0 /* * inequalities */ rule R >Rat S => R -Rat S >Rat 0 requires S =/=Rat 0 rule < I , _ >Rat >Rat 0 => I >Int 0 rule I:Int >Rat 0 => I >Int 0 // derived rule R >=Rat S => notBool R <Rat S rule R <Rat S => S >Rat R rule R <=Rat S => S >=Rat R rule minRat(R, S) => R requires R <=Rat S rule minRat(R, S) => S requires S <=Rat R rule maxRat(R, S) => R requires R >=Rat S rule maxRat(R, S) => S requires S >=Rat R syntax Float ::= #Rat2Float(Int, Int, Int, Int) [function, hook(FLOAT.rat2float)] rule Rat2Float(Num:Int, Prec:Int, Exp:Int) => #Rat2Float(Num, 1, Prec, Exp) rule Rat2Float(< Num, Dem >Rat, Prec, Exp) => #Rat2Float(Num, Dem, Prec, Exp) endmodule