Go backward to C.12 Integers as Equivalence ClassesGo up to C Logic Evaluator DefinitionsGo forward to C.14 Order Relations

## C.13 Rationals as Equivalence Classes

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

// just consider subset of Z x Z
fun Q' =
set(x in Z[](I(3, 0)), y in Z[](I(3, 0)):
not(=(y, Z0)), tuple(x, y));

// x0/x1 = y0/y1
fun ~Q =
set(x in Q', y in Q':
=(*Z(.0(x), .1(y)), *Z(.0(y), .1(x))), tuple(x, y));

// Q as a quotient set
fun Q = /(Q', ~Q);

// selector function
fun _(x) = such(a in x: true, a);

// equivalence class of x
fun []Q(x in Q') = [](x, ~Q);

// constants
fun Q0 = []Q(tuple(Z0, Z1));
fun Q1 = []Q(tuple(Z1, Z1));
fun Q2 = []Q(tuple(Z2, Z1));

// arithmetic
fun +Q(x in Q, y in Q) =
[]Q(tuple(+Z(*Z(.0(_(x)), .1(_(y))), *Z(.0(_(y)), .1(_(x)))),
*Z(.1(_(x)), .1(_(y)))));
fun -Q(x in Q) =
[]Q(tuple(-Z(.0(_(x))), .1(_(x))));
fun -Q(x in Q, y in Q) =
[]Q(tuple(-Z(*Z(.0(_(x)), .1(_(y))), *Z(.0(_(y)), .1(_(x)))),
*Z(.1(_(x)), .1(_(y)))));
fun *Q(x in Q, y in Q) =
[]Q(tuple(*Z(.0(_(x)), .0(_(y))), *Z(.1(_(x)), .1(_(y)))));
fun ^-1Q(x in Q) =
[]Q(tuple(.1(_(x)), .0(_(x))));
fun /Q(x in Q, y in Q) =
[]Q(tuple(*Z(.0(_(x)), .1(_(y))), *Z(.0(_(y)), .1(_(x)))));

// order
pred <=Q(x in Q, y in 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 \$
// ----------------------------------------------------------------
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999