Go backward to C.4 Integer Numbers Go up to C Logic Evaluator Definitions Go forward to C.6 Real Numbers

C.5 Rational Numbers

// ----------------------------------------------------------------
// $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $
// the rational numbers
//
// (c) 1999, Wolfgang Schreiner, see file COPYRIGHT
// http://www.risc.uni-linz.ac.at/software/formal
// ----------------------------------------------------------------
read integer;

// conversion predicates
fun Z(x: N) = tuple(x, N0);
fun N(x: Z) = .0(||(x));

// rationals are pairs of integers
pred Q(x) <=> 
  and(Tuple(x), =(2, length(x)), 
    Z(.0(x)), Z(.1(x)), not(<=Z(.1(x), Z0)),
    relprime(N(.0(x)), N(.1(x))));

// rational constructor and selectors
fun @(x: Z, y: Z) = 
  let(g = Z(gcd(N(x), N(y))):
    tuple(*Z(sign(*Z(x, y)), divZ(||(x), g)), divZ(||(y), g)));
fun numerator(r: Z) = .0(r);
fun denominator(r: Z) = .1(r);

// constants
fun Q0 = @(Z0, Z1);
fun Q1 = @(Z1, Z1);
fun Q2 = @(Z2, Z1);

// basic arithmetic
fun +Q(x: Q, y: Q) = 
  @(+Z(*Z(.0(x), .1(y)), *Z(.1(x), .0(y))), *Z(.1(x), .1(y)));
fun *Q(x: Q, y: Q) = 
  @(*Z(.0(x), .0(y)), *Z(.1(x), .1(y)));
fun -Q(x: Q) = @(-Z(.0(x)), .1(x));
fun -Q(x: Q, y: Q) = +Q(x, -Q(y));
fun ^-1Q(x: Q) = @(.1(x), .0(x));
fun /Q(x: Q, y: Q) = *Q(x, ^-1Q(y));

// total order
pred <=Q(x: Q, y: Q) <=> <=Z(*Z(.0(x), .1(y)), *Z(.0(y), .1(x)));

// ----------------------------------------------------------------
// $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $
// ----------------------------------------------------------------