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)>;
};