# 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 .

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.