Go backward to C.9 Real Functions Go up to C Logic Evaluator Definitions Go forward to C.11 Modular Arithmetic |
// ---------------------------------------------------------------- // $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $ // equivalence relations // // (c) 1999, Wolfgang Schreiner, see file COPYRIGHT // http://www.risc.uni-linz.ac.at/software/formal // ---------------------------------------------------------------- read relation; // R is reflexive on S pred isReflexive(R: Relation, S) <=> forall(x in S: in(tuple(x, x), R)); // R is symmetric on S pred isSymmetric(R: Relation, S) <=> forall(t in R: in(tuple(.1(t), .0(t)), R)); // R is transitive on S pred isTransitive(R: Relation, S) <=> forall(s in R, t in R: implies(=(.1(s), .0(t)), in(tuple(.0(s), .1(t)), R))); // R is equivalence relation on S pred isEquivalence(R: Relation, S) <=> and(isRelation(R, S, S), isReflexive(R, S), isSymmetric(R, S), isTransitive(R, S)); // class [x]_R fun [](x, R: Relation) = set(y in range(R): in(tuple(x, y), R), y); // quotient set S/R fun /(S, R: Relation) = set(x in S: true, [](x, R)); // D is partition on S pred isPartition(D, S) <=> and(forall(x in D: not(=(x, {}))), forall(x in D, y in D: or(=(x, y), =(**(x, y), {}))), =(++(D), S)); // induced relation ~D fun ~(D) = ++(set(d in D: true, set(x in d, y in d: true, tuple(x, y)))); // ---------------------------------------------------------------- // $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $ // ----------------------------------------------------------------