Go backward to C.1 Sets Go up to C Logic Evaluator Definitions Go forward to C.3 Natural Numbers

C.2 Relations and Functions

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

read set;

// R is a relation
pred Relation(R) <=> 
  forall(x in R: and(Tuple(x), =(length(x), 2)));

// R is a relation between A and B
pred isRelation(R, A, B) <=> 
  and(Relation(R), forall(x in R: and(in(.0(x), A), in(.1(x), B))));

// domain of R
fun domain(R: Relation) = 
  set(x in R: true, .0(x));

// range of R
fun range(R: Relation) = 
  set(x in R: true, .1(x));

// inverse of R
fun ^-1(R: Relation) =
  set(x in R: true, tuple(.1(x), .0(x)));

// composition of R and S
fun o(R: Relation, S: Relation) =
  let(A = domain(R), B = **(range(R), domain(S)), C = range(S):
    set(a in A, c in C:
      exists(b in B: and(in(tuple(a, b), R), in(tuple(b, c), S))),
      tuple(a, c)));

// f is a function
pred Function(f) <=>
  and(Relation(f),
    forall(t0 in f, t1 in f: 
      let(x0 = .0(t0), y0 = .1(t0), x1 = .0(t1), y1 = .1(t1):
        implies(=(x0, x1), =(y0, y1)))));

// f is a partial function from A to B
pred isPartialFunction(f, A, B) <=>
  and(isRelation(f, A, B), Function(f));

// f is a total function from A to B
pred isFunction(f, A, B) <=>
  and(isPartialFunction(f, A, B),
    forall(x in A: exists(y in B: in(tuple(x, y), f))));

// application of f to x
fun apply(f: Function, x) =
  such(y in range(f): in(tuple(x, y), f), y);

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