|
[____]
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.
[Next][Prev] [Right] [____] [Up] [Index] [Root]
|