Go up to TopGo forward to 2 Language

# 1 Examples

You may reinitialize the applets in this page by pressing the keys `Shift`+`Reload` (Netscape Communicator) respectively `Refresh` (Microsoft Internet Explorer).

The following example demonstrates the use of the evaluator on some set-theoretic notions. We define the product of two sets A and B as

A x B := {<a, b>: a in A /\ b in B}.

This is written in the language of the evaluator as

```fun x(A, B) = set(a in A, b in B: true, tuple(a, b));
```

(where "true" is a placeholder for additional restrictions on a and b).

This function definition is stored in a file `set.txt` which is loaded in the evaluator as shown below. When pressing the `Enter` key, the product of the sets {1, 2, 3} and {0, 1} is computed (you may also experiment with other examples).

File `set.txt` also includes a definition of the unary function `Powerset` that returns the set of all subsets of a given set

Powerset(A) := {S : S subset A}

where the subset relationship

A subset B :<=> (forall x in A: x in B)

is defined in the evaluator as

```pred isSubset(A, B) <=> forall(x in A: in(x, B));
```

For instance, if we take S as {1, 2, 3, 4, 5}, then its powerset is computed as

We now want to check whether every element in this powerset is indeed a subset of the input, i.e.,

(forall A in Powerset(S): A subset S).

The test is computed by the following program:

Now for some geometry: a tuple p = <px, py> of numbers may be interpreted as a point in the plane with horizontal coordinate px and vertical coordinate py, respectively. The relation

 p ~ q :<=> r = s where (r = (px-cx)2+(py-cy)2, s = (qx-cx)2+(qy-cy)2)

expresses the fact that two points p and q have the same distance from a given point c. The set of points

circle(p) := {q: p ~ q}

therefore describes the circle with center c that goes through p.

Using the corresponding definitions

```pred ~(p: Point, q: Point) <=>
let (r = +(-^2(.0(p), .0(c)), -^2(.1(p), .1(c))),
s = +(-^2(.0(q), .0(c)), -^2(.1(q), .1(c))):
~=(r, s));

fun circle(p: Point) =
set(x in rangeX, y in rangeY, q = tuple(x, y): ~(p, q), q);
```

stored in file `circle.txt` we can visualize such a circle as shown below (this may take a few seconds; you have to stay with the cursor on the input field such that it remains gray).

Likewise, we may partition (a subset of) the plane into the set of all such circles

{circle(p): p = <x, y>, x in rangeX, y in rangeY}

In the executable version, we take a fixed value for y in order to speed up the computation (the result is the same). It will nevertheless take some minutes; please stay with the cursor on the gray input field:

Maintained by: Wolfgang Schreiner
Last Modification: September 16, 2004