previous up next
Go up to Top
Go forward to 2 Language
 RISC-Linz logo

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
previous up next