Creating Sequences

Square brackets are used for the definition of enumerated sequences; formal sequences are delimited by the composite brackets [! and !].

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

U

the universe: any Magma structure;

E

the range set for enumerated sequences: any enumerated structure (it must be possible to loop over its elements -- see the Introduction to this Part);

F

the range set for formal sequences: any structure for which membership testing using in is defined -- see the Introduction to this Part);

x

a free variable which successively takes the elements of E (or F in the formal case) as its values;

P

a Boolean expression that usually involves the variable(s) x, x₁, ..., x_k;

e

an expression that also usually involves the variable(s) x, x₁, ..., x_k.

The Formal Sequence Constructor

The formal sequence constructor has the following fixed format (the expressions appearing in the construct are defined above):

[! x in F | P(x) !]

Create the formal sequence consisting of the subsequence of elements x of F for which P(x) is true. If P(x) is true for every element of F, the sequence constructor may be abbreviated to [! x in F !]

The Enumerated Sequence Constructor

Sequences can be constructed by expressions enclosed in square brackets, provided that the values of all expressions can be automatically coerced into some common structure, as outlined in the Introduction. All general constructors have the universe U optionally up front, which allows the user to specify into which structure all terms of the sequences should be coerced.

[ ] : Null -> ESeqEnum

The null sequence (empty, and no universe specified).

[ U | ] : Str -> SeqEnum

The empty sequence with universe U.

[ e₁, e₂, ..., e_n ] : Elt, ..., Elt -> SeqEnum

Given a list of expressions e₁, ..., e_n, defining elements a₁, a₂, ..., a_n all belonging to (or automatically coercible into) a single algebraic structure U, create the sequence Q = [ a₁, a₂, ..., a_n ] of elements of U.

As for multisets, one may use the expression x^^ n to specify the object x with multiplicity n: this is simply interpreted to mean x repeated n times (i.e., no internal compaction of the repetition is done).

[ U | e₁, e₂, ..., e_m ] : Str, Elt, ..., Elt -> SeqEnum

Given a list of expressions e₁, ..., e_m, which define elements a₁, a₂, ..., a_n that are all coercible into U, create the sequence Q = [ a₁, a₂, ..., a_n ] of elements of U.

[ e(x) : x in E | P(x) ]

Form the sequence of elements e(x), all belonging to some common structure, for those x ∈E with the property that the predicate P(x) is true. The expressions appearing in this construct have the interpretation given at the beginning of this section.

If P(x) is true for every element of E, the sequence constructor may be abbreviated to [ e(x) : x in E ] .

[ U | e(x) : x in E | P(x) ]

Form the sequence of elements of U consisting of the values e(x) for those x∈E for which the predicate P(x) is true (an error results if not all e(x) are coercible into U). The expressions appearing in this construct have the same interpretation as above.

[ e(x₁,...,x_k) : x₁ in E₁, ..., x_kin E_k | P(x₁, ..., x_k) ]

The sequence consisting of those elements e(x₁, ..., x_k), in some common structure, for which x₁, ..., x_k in E₁, ..., E_k have the property that P(x₁, ..., x_k) is true.

The expressions appearing in this construct have the interpretation given at the beginning of this section.

Note that if two successive ranges E_i and E_{i + 1} are identical, then the specification of the ranges for x_i and x_{i + 1} may be abbreviated to x_i, x_{i + 1} in E_i.

Also, if P(x₁, ..., x_k) is always true, it may be omitted.

[ U | e(x₁,...,x_k) : x₁ in E₁, ...,x_k in E_k | P(x₁, ..., x_k) ]

As in the previous entry, the sequence consisting of those elements e(x₁, ..., x_k) for which P(x₁, ..., x_k) is true is formed, as a sequence of elements of U (an error occurs if not all e(x₁, ..., x_k) are coercible into U).

The Arithmetic Progression Constructors

Since enumerated sequences of integers arise so often, there are a few special constructors to create and handle them efficiently in case the entries are in arithmetic progression. The universe must be the ring of integers. Some effort is made to preserve the special way of storing arithmetic progressions under sequence operations.

[ i..j ] : RngIntElt, RngIntElt -> SeqEnum

[ U | i..j ] : Str, RngIntElt, RngIntElt -> SeqEnum

The enumerated sequence of integers whose elements form the arithmetic progression i, i + 1, i + 2, ..., j, where i and j are (expressions defining) arbitrary integers. If j is less than i then the empty sequence of integers will be created.

The universe U, if it is specified, has to be the ring of integers; any other universe will lead to an error.

[ i .. j by k ] : RngIntElt, RngIntElt, RngIntElt -> SeqEnum

[ U | i .. j by k ] : Str, RngIntElt, RngIntElt, RngIntElt -> SeqEnum

The enumerated sequence consisting of the integers forming the arithmetic progression i, i + k, i + 2 * k, ..., j, where i, j and k are (expressions defining) arbitrary integers (but k≠0).

If k is positive then the last element in the progression will be the greatest integer of the form i + n * k that is less than or equal to j; if j is less than i, the empty sequence of integers will be constructed.

If k is negative then the last element in the progression will be the least integer of the form i + n * k that is greater than or equal to j; if j is greater than i, the empty sequence of integers will be constructed.

The universe U, if it is specified, has to be the ring of integers; any other universe will lead to an error.

> s := [ IntegerRing(200) | x : x in [ 25..125 ] ];