nLab sequence




A sequence is a function whose domain is a subset of the set \mathbb{N} of natural numbers (or more generally a subset of the set \mathbb{Z} of integers; cf. bi-infinite sequence and the further generalizations below). Often one means an infinite sequence, which is a sequence whose domain is infinite. Sequences (especially finite ones) are often called lists in computer science. (In constructive mathematics, the domain of a sequence must be a decidable subset of \mathbb{Z}.)

Sequences may also be indicated by functions ωX\omega \to X where ω\omega is the first countably infinite ordinal: the key piece of structure on \mathbb{N} relevant for the study of sequences, particularly in analysis, is the order structure.

Up to bijection, the only possible domains are those of the form

{i:|0i<n} \{i\colon \mathbb{Z} \;|\; 0 \leq i \lt n\}

for n=0,1,2,,n = 0, 1, 2, \ldots, \infty; other domains are used for notational convenience.

An alternative generalisation takes the domain to be a set of ordinal numbers, without loss of generality the set

{i:Ord|i<α} \{i\colon \Ord \;|\; i \lt \alpha\}

for α\alpha some specific ordinal number (or the proper class Ord\Ord of all ordinal numbers, if one wishes to allow for a proper class).

A subsequence of a sequence a=a n:Xa = a_n: \mathbb{N} \to X is a composition

iaX\mathbb{N} \stackrel{i}{\to} \mathbb{N} \stackrel{a}{\to} X

where ii is an order-preserving monomorphism. The salient point is that ii be cofinal as an embedding.


One normally writes the value of the sequence aa at the argument ii as a ia_i rather than a(i)a(i). Similarly, given a term a[i]a[i] with the free variable ii, one often defines a sequence whose values equal those terms as (a[i]) i<n(a[i])_{i \lt n}, {a[i]} i\{a[i]\}_i, or the like. In fact, one even often says literally ‘Let (a i)(a_i) be a sequence.’ even though ‘Let aa be a sequence.’ would be less of an abuse of notation. This is all because notation for sequences arose before functions were considered in their full generality, and one distinguished a ‘sequence’ (whose domain was a set of integers) from a ‘function’ (whose domain was an interval in the real line or a region in the complex plane). Early mathematicians also often conflated the sequence (the function itself) with its range (a subset of the function's target); hence the use of curly braces. All of this applies in greater generality to families with index sets other than \mathbb{N}.



Infinite sequences are often used in topology, but for topology in general, one needs to generalise to nets, also called Moore–Smith sequences. Here one replaces the domain \mathbb{N} by any arbitrary directed set.

Sequential nets

Recall that weak countable choice is a rather weak version of the axiom of choice that is accepted even in most schools of constructive mathematics; it follows separately from both excluded middle and countable choice. However, when it fails (as it does in the internal language of some widely studied toposes, such as the topos of sheaves over the real line), then some important results about sequences fail, including many standard results in topology. In this case, we may want a slight generalisation that we call sequential nets.

A sequential net is a multi-valued function from \mathbb{N} (or a decidable subset thereof) to XX, that is a span AX\mathbb{N} \leftarrow A \rightarrow X where the map AA \to \mathbb{N} is a surjection (or has a decidable range). Note that AA inherits the structure of a directed set via AA \to \mathbb{N}, so that AXA \to X is a net. As a net, every sequential net is equivalent (in the sense of corresponding to the same filter) to some sequence, if you assume WCC. Without WCC, however, this equivalence fails.

(Using a multi-valued function here is a special case of an alternative definition of net that uses only partially ordered directed sets; see net. In some foundations of mathematics, we can get the same result by defining a sequential net to be a presequence: a prefunction, which is like a function but need not preserve equality, from \mathbb{N} or a decidable subset thereof.)

Without WCC, many of the usual properties of metric spaces and other sequential spaces fail, but they continue to hold using sequential nets in the place of sequences. For example, every (located Dedekind) real number may be represented as a sequential Cauchy net, even when they might not all be represented as Cauchy sequences; see Cauchy real number.

Sequence types

In dependent type theory, a sequence type is simply the function type A\mathbb{N} \to A, and thus comes with the following rules:

Formation rules for sequence types:

ΓAtypeΓAtype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathbb{N} \to A \; \mathrm{type}}

Introduction rules for sequence types:

ΓAtypeΓ,n:a(n):AΓλ(n:).a(n):A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, n:\mathbb{N} \vdash a(n):A}{\Gamma \vdash \lambda(n:\mathbb{N}).a(n):\mathbb{N} \to A}

Elimination rules for sequence types:

ΓAtypeΓ,a:A,n:ev(a,n):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:\mathbb{N} \to A, n:\mathbb{N} \vdash \mathrm{ev}(a, n):A}

Computation rules for sequence types:

ΓAtypeΓ,n:a(n):AΓ,m:β Π(m):ev(λ(n:).a(n),m)= Aa(m)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, n:\mathbb{N} \vdash a(n):A}{\Gamma, m:\mathbb{N} \vdash \beta_\Pi(m):\mathrm{ev}(\lambda(n:\mathbb{N}).a(n), m) =_{A} a(m)}

Uniqueness rules for sequence types:

ΓAtypeΓ,a:Aη Π(a):a= Aλ(n:).a(n)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:\mathbb{N} \to A \vdash \eta_\Pi(a):a =_{\mathbb{N} \to A} \lambda(n:\mathbb{N}).a(n)}

Sequence types also have their own extensionality principle, called sequence extensionality. This states that given two sequences a:Aa:\mathbb{N} \to A and b:Ab:\mathbb{N} \to A there is an equivalence of types between the identity type a= Aba =_{\mathbb{N} \to A} b and the dependent sequence type (n:)(a(n)= Ab(n))(n:\mathbb{N}) \to (a(n) =_{A} b(n)):

ΓAtypeΓ,a:A,b:Aseqext(a,b):(a= Ab)(n:)(a(n)= Ab(n))\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:\mathbb{N} \to A, b:\mathbb{N} \to A \vdash \mathrm{seqext}(a, b):(a =_{\mathbb{N} \to A} b) \simeq (n:\mathbb{N}) \to (a(n) =_{A} b(n))}

Sequence types are used in strongly predicative mathematics, where one does not have function types, to construct the real numbers.

Sequence spaces

In functional analysis, one considers topological vector spaces of infinite sequences; these are the sequence spaces. (Actually, these generalise quite nicely to net spaces.)

Not all that related, but similar sounding:

Last revised on January 9, 2023 at 23:27:59. See the history of this page for a list of all contributions to it.