A sequence in Magma is a linearly ordered collection of objects belonging to some common structure (called the universe of the sequence).
There are two types of sequence: enumerated sequences, of which the elements are all stored explicitly (with one exception, see below); and formal sequences, of which elements are stored implicitly by means of a predicate that allows for testing membership. In particular, enumerated sequences are always finite, and formal sequences are allowed to be infinite. In this chapter a sequence will be either a formal or an enumerated sequence.
An enumerated sequence of length l is an array of indefinite length of which only finitely many terms -- including the l-th term, but no term of bigger index --- have been defined to be elements of some common structure. Such sequence is called complete if all of the terms (from index 1 up to the length l) are defined.
In practice the length of an enumerated sequence must be less than 230.
Incomplete enumerated sequences are allowed as a convenience for the programmer in building complete enumerated sequences. Some sequence functions require their arguments to be complete; if that is the case, it is mentioned explicitly in the description below. However, all functions using sequences in other Magma modules always assume that a sequence that is passed in as an argument is complete. Note that the following line converts a possibly incomplete sequence S into a complete sequence T:
T := [ s : s in S ];because the enumeration using the in operator simply ignores undefined terms.
Enumerated sequences of Booleans are highly optimized (stored as bit-vectors).
A formal sequence consists of elements of some range set on which a certain predicate assumes the value `true'.
There is only a very limited number of operations that can be performed on them.
The binary operators for sequences do not allow mixing of the formal and enumerated sequence types (so one cannot take the concatenation of an enumerated sequence and a formal sequence, for example); but it is easy to convert an enumerated sequence into a formal sequence -- see the section on binary operators below.
By the limitation on their construction formal sequences can only contain elements from one structure in Magma. The elements of enumerated sequences are also restricted, in the sense that either some common structure 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 parents is the same for sequences and sets, and is outlined in Chapter INTRODUCTION TO AGGREGATES.