Go backward to C.11 Modular Arithmetic Go up to C Logic Evaluator Definitions Go forward to C.13 Rationals as Equivalence Classes |
// ---------------------------------------------------------------- // $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $ // the integer numbers as equivalence classes // // (c) 1999, Wolfgang Schreiner, see file COPYRIGHT // http://www.risc.uni-linz.ac.at/software/formal // ---------------------------------------------------------------- read equiv; read natural0; // just consider subset of N x N fun Z' = set(x in nat(0, 6), y in nat(0, 6): true, tuple(x, y)); // x0-x1 = y0-y1 fun ~Z = set(x in Z', y in Z': =(+N(.0(x), .1(y)), +N(.0(y), .1(x))), tuple(x, y)); // Z as a quotient set fun Z = /(Z', ~Z); // selector function fun _(x) = such(a in x: true, a); // equivalence class of x fun []Z(x in Z') = [](x, ~Z); // constants fun Z0 = []Z(tuple(N0, N0)); fun Z1 = []Z(tuple(N1, N0)); fun Z2 = []Z(tuple(N2, N0)); // arithmetic fun +Z(x in Z, y in Z) = []Z(tuple(+N(.0(_(x)), .0(_(y))), +N(.1(_(x)), .1(_(y))))); fun -Z(x in Z) = []Z(tuple(.1(_(x)), .0(_(x)))); fun -Z(x in Z, y in Z) = []Z(tuple(+N(.0(_(x)), .1(_(y))), +N(.0(_(y)), .1(_(x))))); fun *Z(x in Z, y in Z) = []Z(tuple(+N(*N(.0(_(x)), .0(_(y))), *N(.1(_(x)), .1(_(y)))), +N(*N(.0(_(x)), .1(_(y))), *N(.1(_(x)), .0(_(y)))))); // order pred <=Z(x in Z, y in Z) <=> <=N(+N(.0(_(x)), .1(_(y))), +N(.0(_(y)), .1(_(x)))); // ---------------------------------------------------------------- // $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $ // ----------------------------------------------------------------