A set in Magma is a (usually unordered) collection of objects belonging to some common structure (called the universe of the set). There are three basic types of sets: enumerated sets, whose elements are all stored explicitly (with one exception, see below); formal sets, whose elements are stored implicitly by means of a predicate that allows for testing membership; and indexed sets, which are restricted enumerated sets having a numbering on elements. In particular, enumerated and indexed sets are always finite, and formal sets are allowed to be infinite.

Subsections

• Enumerated Sets
• Formal Sets
• Indexed Sets
• Compatibility
• Notation

Enumerated sets are finite, and can be specified in three basic ways (see also section 2 below): by listing all elements; by an expression involving elements of some finite structure; and by an arithmetic progression. If an arithmetic progression is specified, the elements are not calculated explicitly until a modification of the set necessitates it; in all other cases all elements of the enumerated set are stored explicitly.

Formal Sets

A formal set consists of the subset of elements of some carrier set (structure) on which a certain predicate assumes the value `true'.

The only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.

Indexed Sets

For some purposes it is useful to be able to access elements of a set through an index map, which numbers the elements of the set. For that purpose Magma has indexed sets, on which a very few basic set operations are allowed (element membership testing) as well as some sequence-like operations (such as accessing the i-th term, getting the index of an element, appending and pruning).

Compatibility

The binary operators for sets do not allow mixing of the three types of sets (so one cannot take the intersection of an enumerated set and a formal set, for example), but it is easy to convert an enumerated set into a formal set -- see the section on binary operators below -- and there are functions provided for making an enumerated set out of an indexed set (and vice versa).

By the limitation on their construction formal sets can only contain elements from one structure in Magma. The elements of enumerated sets are also restricted, in the sense that either some universe must be specified upon creation, or Magma must be able to find such universe automatically. The rules for compatibility of elements and the way Magma deals with these universes are the same for sequences and sets, and are described in the previous chapter. The restrictions on indexed sets are the same as those for enumerated sets.

Notation

Certain expressions appearing in the sections below (possibly with subscripts) have a standard interpretation:

• the universe: any Magma structure;
• the carrier set for enumerated sets: any enumerated structure (it must be possible to loop over its elements -- see the Introduction to this Part);
• the carrier set for formal sets: any structure for which membership testing using in is defined -- see the Introduction to this Part);
• a free variable which successively takes the elements of E (or F in the formal case) as its values;
• a Boolean expression that usually involves the variable(s) x, x_1, ..., x_k;
• an expression that also usually involves the variable(s) x, x_1, ..., x_k.