\chapter{SETS: A basic set theory package}
\label{SETS}
\typeout{{SETS: A basic set theory package}}
{\footnotesize
\begin{center}
Francis J. Wright \\
School of Mathematical Sciences, Queen Mary and Westfield College \\
University of London \\
Mile End Road \\
London E1 4NS, England \\[0.05in]
e--mail: F.J.Wright@QMW.ac.uk
\end{center}
}
\ttindex{SETS}
The SETS package provides set theoretic operations on lists and represents
the results as normal algebraic-mode lists, so that all other \REDUCE{}
facilities that apply to lists can still be applied to lists that have
been constructed by explicit set operations.
\section{Infix operator precedence}
The set operators are currently inserted into the standard \REDUCE{}
precedence list (see section~\ref{sec-operators}) as follows:
\begin{verbatim}
or and not member memq = set_eq neq eq >= > <= < subset_eq
subset freeof + - setdiff union intersection * / ^ .
\end{verbatim}
\section{Explicit set representation and MKSET}
Explicit sets are represented by lists, and there is a need to convert
standard \REDUCE\ lists into a set by removing duplicates. The
package also orders the members of the set so the standard {\tt =}
predicate will provide set equality.\ttindex{MKSET}
\begin{verbatim}
mkset {1,2,y,x*y,x+y};
{x + y,x*y,y,1,2}
\end{verbatim}
The empty set is represented by the empty list \verb|{}|.
\section{Union and intersection}
The intersection operator has the name\ttindex{intersect} {\tt
intersect}, and set union is denotes by\ttindex{union}{\tt union}.
These operators will probably most commonly be used as binary infix
operators applied to explicit sets,
\begin{verbatim}
{1,2,3} union {2,3,4};
{1,2,3,4}
{1,2,3} intersect {2,3,4};
{2,3}
\end{verbatim}
\section{Symbolic set expressions}
If one or more of the arguments evaluates to an unbound identifier
then it is regarded as representing a symbolic implicit set, and the
union or intersection will evaluate to an expression that still
contains the union or intersection operator. These two operators are
symmetric, and so if they remain symbolic their arguments will be
sorted as for any symmetric operator. Such symbolic set expressions
are simplified, but the simplification may not be complete in
non-trivial cases. For example:
\begin{verbatim}
a union b union {} union b union {7,3};
{3,7} union a union b
a intersect {};
{}
\end{verbatim}
Intersection distributes over union, which is not applied by default
but is implemented as a rule list assigned to the variable {\tt
set\_distribution\_rule}, {\em e.g.}
\begin{verbatim}
a intersect (b union c);
(b union c) intersection a
a intersect (b union c) where set_distribution_rule;
a intersection b union a intersection c
\end{verbatim}
\section{Set difference}
The set difference operator is represented by the symbol \verb|\| and
is always output using this symbol, although it can also be input using
\ttindex{setdiff} {\tt setdiff}. It is a binary operator.
\begin{verbatim}
{1,2,3} \ {2,4};
{1,3}
a \ {1,2};
a\{1,2}
a \ a;
{}
\end{verbatim}
\section{Predicates on sets}
Set membership, inclusion or equality are all binary infix operators.
They can only be used within conditional statements or within the
argument of the {\tt evalb}\ttindex{evalb} operator provided by this
package, and they cannot remain symbolic -- a predicate that cannot be
evaluated to a Boolean value causes a normal \REDUCE\ error.
The {\tt evalb} operator provides a convenient shorthand for an {\tt
if} statement designed purely to display the value of any Boolean
expression (not only predicates defined in this package).
\begin{verbatim}
if a = a then true else false;
true
evalb(a = a);
true
if a = b then true else false;
false
\end{verbatim}
\subsection{Set membership}
Set membership is tested by the predicate \ttindex{member}{\tt member}.
Its left operand is regarded as a potential set element and
its right operand {\em must\/} evaluate to an explicit set. There is
currently no sense in which the right operand could be an implicit set.
\begin{verbatim}
evalb(1 member {1,2,3});
true
evalb(2 member {1,2} intersect {2,3});
true
evalb(a member b);
***** b invalid as list
\end{verbatim}
\subsection{Set inclusion}
Set inclusion is tested by the predicate {\tt subset\_eq}
\ttindex{subset\_eq} where {\tt a subset\_eq b} is true if the set $a$
is either a subset of or equal to the set $b$; strict inclusion is
tested by the predicate {\tt subset}\ttindex{subset}
where {\tt a subset b} is true if the set $a$ is {\em strictly\/} a
subset of the set $b$ and is false is $a$ is equal to $b$. These
predicates provide some support for symbolic set expressions, but is
incomplete.
\begin{verbatim}
evalb({1,2} subset_eq {1,2,3});
true
evalb({1,2} subset_eq {1,2});
true
evalb({1,2} subset {1,2});
false
evalb(a subset a union b);
true
\end{verbatim}
\newpage
\begin{verbatim}
evalb(a\b subset a);
true
\end{verbatim}
An undecidable predicate causes a normal \REDUCE\ error, {\em e.g.\ }
\begin{verbatim}
evalb(a subset_eq {b});
***** Cannot evaluate a subset_eq {b} as Boolean-valued set
expression
\end{verbatim}
\subsection{Set equality}
As explained above, equality of two sets in canonical form can be
reliably tested by the standard \REDUCE\ equality predicate ({\tt =}).