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

For example: A=1,3,2A = \langle 1, 3, 2 \rangle, in that order. A sequence a,b,c\langle a, b, c \rangle can be seen as the total bijective function {(1,a),(2,b),(3,c)}\{ (1, a), (2, b), (3, c) \}. Following this definition, we can access the nn element of a sequence using function application notation. Given A=a,c,bA = \langle a, c, b \rangle, A(2)=cA(2) = c.

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

If XX is a set, then seq(X)seq(X) represents all the finite sequences of elements of XX, and its defined as: $ { s X n dom(s) = { 1 .. n } } $.

Basic Operations


Given sequences ss and tt, their concatenation is denoted as sts \frown t. Notice that sttss \frown t \neq t \frown s. Of course, s=ss \frown \langle \rangle = s, and concatenation is an associative operation. It also follows that if st=s \frown t = \langle \rangle, then s=s = \langle \rangle and t=t = \langle \rangle.

Filtering (or Restriction)

Given a sequence ss, the sequence sxs \restriction x represents all the elements of ss that are included in xx, preserving the ordering. For example, s=a,b,b,a,c,b,a{a,c}=a,a,c,as = \langle a, b, b, a, c, b, a \rangle \restriction \{ a, c \} = \langle a, a, c, a \rangle. Notice that given set AA, (st)A=(sA)(tA)(s \frown t) \restriction A = (s \restriction A) \frown (t \restriction A).

Filtering the empty sequence always yields back the empty sequence: XX=\forall X \bullet \langle \rangle \restriction X = \langle \rangle, and filtering any sequence by the empty set also yields the empty sequence: sseqs=\forall s \in seq \bullet s \restriction \emptyset = \langle \rangle.

Applying multiple restrictions over the same sequence is the same as restricting by the intersection of those sets. Given sequence ss and sets AA and BB, then (sA)B=s(AB)(s \restriction A) \restriction B = s \restriction (A \cap B).

The first element of a sequence is called its head. For example, given S=a,b,cS = \langle a, b, c \rangle, S0=aS_{0} = a, or alternatively head(S)=ahead(S) = a. The head of the empty sequence is the empty sequence. Notice that head(xs)=xhead(\langle x \rangle \frown s) = x, and that given a non empty sequence ss, then thead(s)t=s\exists t \bullet head(s) \frown t = s.


The tail of a sequence is a sequence containing all the original elements except for the first one. For example, given S=a,b,cS = \langle a, b, c \rangle, then $S’ = b, c $, or alternatively tail(S)=b,ctail(S) = \langle b, c \rangle. Notice that for any sequence SS, S=S0SS = S_{0} \frown S', and (xS)=S(\langle x \rangle \frown S)' = S.


Sequences are indexed from 0 using square bracket notation. For example a,b,c[1]=b\langle a, b, c \rangle[1] = b.


A sequence SS is a prefix of sequence TT if the elements if there is a sequence QinTQ in T such that T=SQT = S \frown Q. For example: a,ba,b,c,d\langle a, b \rangle \leq \langle a, b, c, d \rangle but b,ca,b,c,d\langle b, c \rangle \lneq \langle a, b, c, d \rangle. Notice that given any set AA, st(sA)(tA)s \leq t \implies (s \restriction A) \leq (t \restriction A). Also, given a sequence ss, tu(st)(su)t \leq u \implies (s \frown t) \leq (s \frown u).

If follows that given any sequence SS, S\langle \rangle \leq S, and that SSS \leq S. This operation is asymmetric: sttss=ts \leq t \land t \leq s \implies s = t, and transitive: sttusus \leq t \land t \leq u \implies s \leq u. Of course, if sts \leq t, then u(su)=t\exists u \bullet (s \frown u) = t.

An easy way to check if a prefix expression sts \leq t holds is by checking that (t)(s0=t0)(st)(t \neq \langle \rangle) \land (s_{0} = t_{0}) \land (s' \leq t').

Notice that if two sequences are prefixes of the same sequence, then one is the prefix of the other or viceversa: (su)(tu)(st)(ts)(s \leq u) \land (t \leq u) \implies (s \leq t) \lor (t \leq s).

The \leq operator may have an exponent, in which case SS is an n-prefix of TT if TT starts with SS and it has up to nn elements removed. For example: a,b2a,b,c,d\langle a, b \rangle \leq^{2} \langle a, b, c, d \rangle, a,b2a,b,c\langle a, b \rangle \leq^{2} \langle a, b, c \rangle, but a,b2a,b,c,d,e\langle a, b \rangle \lneq^{2} \langle a, b, c, d, e \rangle. This operator is defined as SnT=(ST#T#S+n)S \leq^{n} T = (S \leq T \land \# T \leq \# S + n). It follows that S0TS=TS \leq^{0} T \iff S = T and that STnSnTS \leq T \iff \exists n \bullet S \leq^{n} T. Also notice that SnTTmUSn+mUS \leq^{n} T \land T \leq^{m} U \implies S \leq^{n + m} U.


Since a sequence is a relation from natural numbers to the sequence elements, we can re-use the cardinality notation from sets. Thus, |a,b,b,c|=4\vert \langle a, b, b, c \rangle \vert = 4, or #a,b,b,c=4\#\langle a, b, b, c \rangle = 4.


A sequence containing other sequences might be flattened to a single sequence by using a ditributed version of the concatenation operator. Given $s = (a, b), (c, d), (e, f) $, then $/s = a, b, c, d, e, f $.


A sequence SS to the power of nn is equal to the sequence concatenated to itself nn times. For example: a,b3=a,b,a,b,a,b\langle a, b \rangle^{3} = \langle a, b, a, b, a, b \rangle.


Given a sequence S=a,b,c,d,eS = \langle a, b, c, d, e \rangle, its inverse is the same sequence from right to left: S¯=e,d,c,b,a\overline{S} = \langle e, d, c, b, a \rangle. Of course, ¯=\overline{\langle \rangle} = \langle \rangle, and x¯=x\overline{\langle x \rangle} = \langle x \rangle. Also, S¯¯=S\overline{\overline{S}} = S. The reverse of a concatenation is equal to the reverse concatenation of the inverse: st¯=t¯s¯\overline{s \frown t} = \overline{t} \frown \overline{s}.


The star sequence of a set AA is the infinite set of finite sequences ss made of elements from AA. More formally: A*={ssA=s}A^{*} = \{ s \mid s \restriction A = s \}. It follows that for any set AA, A*\langle \rangle \in A^{*}.

Membership on a set can be expressed in terms of membership to the star sequence of the set: xA*xA\langle x \rangle \in A^{*} \iff x \in A. Also, (st)A*(s \frown t) \in A^{*} means that both ss and tt are members of the star of AA.


Given a sequence SS, SxS \downarrow x represents the amount of time xx is inside the sequence SS. For example: a,b,b,cb=2\langle a, b, b, c \rangle \downarrow b = 2. Formally, SxS \downarrow x is defined as |S{x}|\vert S \restriction \{ x \} \vert.


The inin operation represents whether a sequence SS is contained within a sequence TT. For example: b,cina,b,c,d\langle b, c \rangle in \langle a, b, c, d \rangle. Notice that not b,dina,b,c,d\langle b, d \rangle in \langle a, b, c, d \rangle.


A sequence ss is an interleave of sequences tt and uu if ss can be constructed by arbitrarily extracting elements from tt and uu in order. For example 1,2,3,4interleaves(1,3,2,4)\langle 1, 2, 3, 4 \rangle interleaves (\langle 1, 3 \rangle, \langle 2, 4 \rangle), and 1,2,3,4interleaves(1,2,3,4)\langle 1, 2, 3, 4 \rangle interleaves (\langle 1, 2 \rangle, \langle 3, 4 \rangle). Of course, it holds that sinterleaves(t,u)=sinterleaves(u,t)s interleaves (t, u) = s interleaves (u, t).

This operation is defined like this:

interleaves(t,u)(t=u=)xsinterleaves(t,u)(thead(t)=xsinterleaves(tail(t),u))(uhead(u)=xsinterleaves(t,tail(u)))\begin{align} \langle \rangle interleaves (t, u) &\iff (t = \langle \rangle \land u = \langle \rangle) \\ \langle x \rangle \frown s interleaves (t, u) &\iff \\&(t \neq \langle \rangle \land head(t) = x \land s interleaves (tail(t), u)) \lor\\& (u \neq \langle \rangle \land head(u) = x \land s interleaves (t, tail(u)) ) \end{align}



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.