Example: Comparison of Sets

The following example illustrates the use of recursion along with logical connectives.

According to the set theory, two sets are considered to be equal, if they contain the same elements. Suppose we want to define a Refal Plus function testing two sets for equality. The first thing we have to invent is the representation of sets by ground expressions. First, let us consider the sets whose elements may be Refal symbols only. A set of symbols {Gs1, Gs2, ..., Gsn} can, obviously, be represented by the ground expression
    Gs1 Gs2 ... Gsn

A feature of this representation is that any non-empty set of symbols has lots of different representations. For example, the set {John, Mary} may be represented as John Mary or Mary John , or even Mary John John Mary . Thus, different representations may correspond to equal sets.

It is well known that an element of a set can be a set itself. So, we must be able to represent sets containing symbols as well as sets, which may contain sets, etc. How shell we represent set elements that are sets?

A simple solution is the following. If an element of a set is a symbol Gs, the element is represented by the symbol Gs. Otherwise, if an element of a set is a set X, the element is represented by the ground term (X'), where X' is a representation of X. For example, the set {A, {A,B}, {A}} may be represented by the ground expression A (A B) (A) .

Now we define the predicate function IsEqSet determining whether its two arguments represent the same set. This function performs the test for equality by reducing it to several simpler tests.

Namely, two sets A and B are equal iff:
where

Thus, instead of defining a single function, we have to define four mutually recursive predicate functions. IsEqSet determines whether its two arguments are representations of the same set. IsSubset determines whether the set represented by the first argument is a subset of the set represented by the second argument. IsEl determines whether the first argument represents a set belonging to the set represented by the second argument. And, finally, IsEqEl determines whether its two arguments represent the same element of a set.

Note that, to test for equality two set elements that are sets themselves, we have to test for equality the corresponding sets, for which reason the function IsEqEl has to call the function IsEqSet. Thus, finally, IsEqSet turns out to be defined in terms of itself.

$func? IsEqSet  (eA)(eB) = ;
$func? IsSubset (eA)(eB) = ;
$func? IsEl     tX  (eA) = ;
$func? IsEqEl   tX  tY   =;

IsEqSet (eA)(eB) =
  <IsSubset (eA)(eB)><IsSubset (eB)(eA)>;

IsSubset (eA)(eB) =
  eA :
  {
  = ;
  tX eR = <IsEl tX (eB)><IsSubset (eR)(eB)>;
  };

IsEl tX (eA) =
  eA : tY eR,
  \{ <IsEqEl tX tY>; <IsEl tX (eR)>; };

IsEqEl tX tY =
  \{
  tX tY : s s
    = tX : tY;
  tX tY : (eA)(eB)
    = <IsEqSet (eA)(eB)>;
  };