# Sequences

A sequence is a mathematical collection of objects in a particular order

For example: , in that order. A sequence can be seen as the total bijective function . Following this definition, we can access the element of a sequence using function application notation. Given , .

The empty sequence is defined as . Sequences are homogeneous. They must contain elements of the same type.

If is a set, then represents all the finite sequences of elements of , and its defined as: .

## Basic Operations

### Concatenation

Given sequences and , their concatenation is denoted as . Notice that . Of course, , and concatenation is an associative operation. It also follows that if , then and .

### Filtering (or Restriction)

Given a sequence , the sequence represents all the elements of that are included in , preserving the ordering. For example, . Notice that given set , .

Filtering the empty sequence always yields back the empty sequence: , and filtering any sequence by the empty set also yields the empty sequence: .

Applying multiple restrictions over the same sequence is the same as restricting by the intersection of those sets. Given sequence and sets and , then .

### Head

The first element of a sequence is called its head. For example, given , , or alternatively . The head of the empty sequence is the empty sequence. Notice that , and that given a non empty sequence , then .

### Tail

The tail of a sequence is a sequence containing all the original elements except for the first one. For example, given , then , or alternatively . Notice that for any sequence , , and .

### Indexing

Sequences are indexed from 0 using square bracket notation. For example .

### Prefix

A sequence is a *prefix* of sequence if the elements if there
is a sequence such that . For example:
but . Notice that
given any set , . Also, given a sequence , .

If follows that given any sequence , , and that . This operation is asymmetric: , and transitive: . Of course, if , then .

An easy way to check if a prefix expression holds is by checking that .

Notice that if two sequences are prefixes of the same sequence, then one is the prefix of the other or viceversa: .

The operator may have an exponent, in which case is an
*n*-prefix of if starts with and it has up to
elements removed. For example: , ,
but . This
operator is defined as . It follows that and that . Also notice that .

### Cardinality

Since a sequence is a relation from natural numbers to the sequence elements, we can re-use the cardinality notation from sets. Thus, , or .

### Flattening

A sequence containing other sequences might be flattened to a single sequence by using a ditributed version of the concatenation operator. Given , then .

### Repetition

A sequence to the power of is equal to the sequence concatenated to itself times. For example: .

### Reverse

Given a sequence , its inverse is the same sequence from right to left: . Of course, , and . Also, . The reverse of a concatenation is equal to the reverse concatenation of the inverse: .

### Star

The star sequence of a set is the infinite set of *finite* sequences
made of elements from . More formally: . It follows that for any set , .

Membership on a set can be expressed in terms of membership to the star sequence of the set: . Also, means that both and are members of the star of .

### Count

Given a sequence , represents the amount of time is inside the sequence . For example: . Formally, is defined as .

### Includes

The operation represents whether a sequence is contained within a sequence . For example: . Notice that not .

### Interleaves

A sequence is an interleave of sequences and if can be constructed by arbitrarily extracting elements from and in order. For example , and . Of course, it holds that .

This operation is defined like this:

## Properties

### Injection

An injective sequence is one where its elements donâ€™t appear more than once. Remember that sequences are defined as functions whose range is the set of natural numbers, and therefore the functional definition of injection (one-to-one) holds: a sequence without duplicates is one where every natural number from the domain points to a different element.