Go backward to C.1 SetsGo up to C Logic Evaluator DefinitionsGo 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
// ----------------------------------------------------------------

// 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 \$
// ----------------------------------------------------------------
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999