123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419 |
- \documentstyle[11pt]{article}
- \title{SETS: A Basic Set Theory Package}
- \author{Francis J. Wright \\
- School of Mathematical Sciences \\
- Queen Mary and Westfield College \\
- University of London \\
- Mile End Road, London E1 4NS, UK. \\
- Email: {\tt F.J.Wright@QMW.ac.uk}}
- \begin{document}
- \maketitle
- \begin{abstract}
- The SETS package for \REDUCE 3.5 and later versions provides
- algebraic-mode support for set operations on lists regarded as sets
- (or representing explicit sets) and on implicit sets represented by
- identifiers. It provides the set-valued infix operators (with
- synonyms) {\tt union}, {\tt intersection} ({\tt intersect}) and {\tt
- setdiff} (\verb|\|, {\tt minus}) and the Boolean-valued infix
- operators (predicates) {\tt member}, {\tt subset\_eq}, {\tt subset},
- {\tt set\_eq}. The union and intersection operators are n-ary and
- the rest are binary. A list can be explicitly converted to the
- canonical set representation by applying the operator {\tt mkset}.
- (The package also provides an operator not specifically related to
- set theory called {\tt evalb} that allows the value of any
- Boolean-valued expression to be displayed in algebraic mode.)
- \end{abstract}
- \section{Introduction}
- REDUCE has no specific representation for a set, neither in algebraic
- mode nor internally, and any object that is mathematically a set is
- represented in REDUCE as a list. The difference between a set and a
- list is that in a set the ordering of elements is not significant and
- duplicate elements are not allowed (or are ignored). Hence a list
- provides a perfectly natural and satisfactory representation for a set
- (but not vice versa). Some languages, such as Maple, provide
- different internal representations for sets and lists, which may allow
- sets to be processed more efficiently, but this is not {\em
- necessary}.
- This package supports 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. The algebraic-mode set
- operations provided by this package have all been available in
- symbolic mode for a long time, and indeed are used internally by the
- rest of REDUCE, so in that sense set theory facilities in REDUCE are
- far from new. What this package does is make them available in
- algebraic mode, generalize their operation by extending the arity of
- union and intersection, and allow their arguments to be implicit sets
- represented by unbound identifiers. It performs some simplifications
- on such symbolic set-valued expressions, but this is currently rather
- {\it ad hoc\/} and is probably incomplete.
- For examples of the operation of the SETS package see (or run) the
- test file {\tt sets.tst}. This package is experimental and
- developments are under consideration; if you have suggestions for
- improvements (or corrections) then please send them to me (FJW),
- preferably by email. The package is intended to be run under
- \REDUCE 3.5 and later versions; it may well run correctly under earlier
- versions although I cannot provide support for such use.
- \section{Infix operator precedence}
- The set operators are currently inserted into the standard REDUCE
- precedence list (see page 28, \S2.7, of the REDUCE 3.6 manual) 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 {\tt mkset}}
- Explicit sets are represented by lists, and this package does not
- require any restrictions at all on the forms of lists that are
- regarded as sets. Nevertheless, duplicate elements in a set
- correspond by definition to the same element and it is conventional
- and convenient to represent them by a single element, i.e.\ to remove
- any duplicate elements. I will call this a normal representation.
- Since the order of elements in a set is irrelevant it is also
- conventional and may be convenient to sort them into some standard
- order, and an appropriate ordering of a normal representation gives a
- canonical representation. This means that two identical sets have
- identical representations, and therefore the standard REDUCE equality
- predicate ({\tt =}) correctly determines set equality; without a
- canonical representation this is not the case.
- Pre-processing of explicit set-valued arguments of the set-valued
- operators to remove duplicates is always done because of the obvious
- efficiency advantage if there were any duplicates, and hence explicit
- sets appearing in the values of such operators will never contain any
- duplicate elements. Such sets are also currently sorted, mainly
- because the result looks better. The ordering used satisfies the {\tt
- ordp} predicate used for most sorting within REDUCE, except that
- explicit integers are sorted into increasing numerical order rather
- than the decreasing order that satisfies {\tt ordp}.
- Hence explicit sets appearing in the result of any set operator are
- currently returned in a canonical form. Any explicit set can also be
- put into this form by applying the operator {\tt mkset} to the list
- representing it. For example
- \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 operator {\tt intersection} (the name used internally) has the
- shorter synonym {\tt intersect}. These operators will probably most
- commonly be used as binary infix operators applied to explicit sets,
- e.g.
- \begin{verbatim}
- {1,2,3} union {2,3,4};
- {1,2,3,4}
- {1,2,3} intersect {2,3,4};
- {2,3}
- \end{verbatim}
- They can also be used as n-ary operators with any number of arguments,
- in which case it saves typing to use them as prefix operators (which
- is possible with all REDUCE infix operators), e.g.
- \begin{verbatim}
- {1,2,3} union {2,3,4} union {3,4,5};
- {1,2,3,4,5}
- intersect({1,2,3}, {2,3,4}, {3,4,5});
- {3}
- \end{verbatim}
- For completeness, they can currently also be used as unary operators,
- in which case they just return their arguments (in canonical form),
- and so act as slightly less efficient versions of {\tt mkset} (but
- this may change), e.g.
- \begin{verbatim}
- union {1,5,3,5,1};
- {1,3,5}
- \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}
- In implementations of REDUCE that provide fancy display using
- mathematical notation, such as PSL-REDUCE~3.6 for MS-Windows, the
- empty set, union, intersection and set difference are all displayed
- using their conventional mathematical symbols, namely $\emptyset$,
- $\cup$, $\cap$, $\setminus$.
- A symbolic set expression is a valid argument for any other set
- operator, e.g.
- \begin{verbatim}
- a union (b intersect c);
- b intersection c union a
- \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}, 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
- either of the two names {\tt setdiff} (the name used internally) or
- {\tt minus} (as used in Maple). It is a binary operator, its operands
- may be any combination of explicit or implicit sets, and it may be
- used in an argument of any other set operator. Here are some
- examples:
- \begin{verbatim}
- {1,2,3} \ {2,4};
- {1,3}
- {1,2,3} \ {};
- {1,2,3}
- a \ {1,2};
- a\{1,2}
- a \ a;
- {}
- a \ {};
- a
- {} \ a;
- {}
- \end{verbatim}
- \section{Predicates on sets}
- These are all binary infix operators. Currently, like all REDUCE
- predicates, they can only be used within conditional statements ({\tt
- if}, {\tt while}, {\tt repeat}) or within the argument of the {\tt
- 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). It has some
- similarity with the {\tt evalb} function in Maple, except that the
- values returned by {\tt evalb} in REDUCE (the identifiers {\tt true}
- and {\tt false}) have no significance to REDUCE itself. Hence, in
- REDUCE, use of {\tt evalb} is {\em never\/} necessary.
- \begin{verbatim}
- if a = a then true else false;
- true
- evalb(a = a);
- true
- if a = b then true else false;
- false
- evalb(a = b);
- false
- evalb 1;
- true
- evalb 0;
- false
- \end{verbatim}
- I will use the {\tt evalb} operator in preference to an explicit {\tt
- if} statement for purposes of illustration.
- \subsection{Set membership}
- Set membership is tested by the predicate {\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; this would
- require a mechanism for declaring implicit set membership (akin to
- implicit variable dependence) which is currently not implemented. Set
- membership testing works like this:
- \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} 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}
- 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 this
- is not yet correct as indicated below. Here are some examples:
- \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
- evalb(a\b subset a);
- true
- evalb(a intersect b subset a union b); %%% BUG
- false
- \end{verbatim}
- An undecidable predicate causes a normal REDUCE error, e.g.
- \begin{verbatim}
- evalb(a subset_eq {b});
- ***** Cannot evaluate a subset_eq {b} as Boolean-valued set
- expression
- evalb(a subset_eq b); %%% BUG
- false
- \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 =}).
- This package also provides the predicate {\tt set\_eq} to test
- equality of two sets not represented canonically. The two predicates
- behave identically for operands that are symbolic set expressions
- because these are always evaluated to canonical form (although
- currently this is probably strictly true only in simple cases). Here
- are some examples:
- \begin{verbatim}
- evalb({1,2,3} = {1,2,3});
- true
- evalb({2,1,3} = {1,3,2});
- false
- evalb(mkset{2,1,3} = mkset{1,3,2});
- true
- evalb({2,1,3} set_eq {1,3,2});
- true
- evalb(a union a = a\{});
- true
- \end{verbatim}
- \section{Installation}
- The source file {\tt sets.red} can be read into REDUCE when required
- using {\tt IN}. If the ``professional'' version is being used this
- should be done with {\tt ON COMP} set, but it is much better to
- compile the code as a {\tt FASL} file using {\tt FASLOUT} and then
- load it with {\tt LOAD\_PACKAGE} (or {\tt LOAD}). See the REDUCE
- manual and implementation-specific guide for further details.
- This package has to redefine the REDUCE internal procedure {\tt
- mk!*sq} and a warning about this can be expected and ignored. I
- believe (and hope!) that this redefinition is safe and will not have
- any unexpected consequences for the rest of REDUCE.
- \section{Possible future developments}
- \begin{itemize}
- \item Unary union/intersection to implement repeated
- union/intersection on a set of sets.
- \item More symbolic set algebra, canonical forms for set expressions,
- more complete simplification.
- \item Better support for Boolean variables via a version (evalb10?)
- of {\tt evalb} that returns 1/0 instead of {\tt true}/{\tt false},
- or predicates that return 1/0 directly.
- \end{itemize}
- \end{document}
|