A list

is a mapping from
some natural number; its outputs (left values) are
known as the entries

or items

in the
list; its inputs (right values) are known as indices

into
the list; in a list f, each f(i) is the entry at index i in f. A given value
may appear at more than one index in the list; when none do so, the list is
monic. If every entry in the list is of some type T, then the list is said to
be of

Ts. The length

of a list (:|n) is the
natural n. A sequence

is a mapping (:|N) for which N is
either {naturals} or a natural. Thus every list is a sequence but some
sequences are infinite, hence not lists; the length of an infinite sequence is
infinite. The nomenclature for sequences is otherwise the same as for
lists.

Lists show up in lots of places in mathematics as a convenient container for a succession of values; most notably in the case of a bulk action, e.g. of a binary operator. When exactly two values are to be contained, it is usually more apt to use a pair (i.e. an atomic relation x←y for the specific values x and y to be paired); but any context which naturally generalises to many values is better handled using lists.

A list can be denoted by square brackets enclosing its entries separated by commas; for example, an (: f |3) can be written [f(0), f(1), f(2)] and, given values a, b, c, one can write the list [a, b, c] to denote that (: f |3) for which f(0) = a, f(1) = b, f(2) = c. More complex denotations use ellipsis as well as overt entries in such a list display. For any value v whatever, there is a list [v] = ({v}:|1) which maps 0 (the single member of {0} = 1) to v. A non-empty list (: f |1+n) can also be denoted [f(0), …, f(n)]; a list introduced as [a, …, z] is given to have at least one entry (it may have only one, in which case a = z); it is (: f |1+n) for some natural n with f(0) = a and f(n) = z.

The element at index n in a list or sequence f is known as the (1+n)-th element in f; this is by specification f(n); for particular n, the usual natural language forms for (1+n)-th are commonly used, e.g. f(0) is the first element, f(1) the second and so on. (The glaring off-by-one in the numbering here is a feature of natural language, arising from it evolving in a culture which started its counting at 1 instead of 0.) For a list of length 1+n, the (1+n)-th element f(n) is likewise referred to as the last element; earlier elements may be referred to using last-but-i terminology, so that f(n−i) is the last-but-i element, for each i in 1+n; as ever, natural language synonyms may also serve, so the penultimate element is f(n−1) and the antepenultimate element is f(n−2), although I do not promise to ever (elsewhere) use these terms ! A sequence f doesn't necessarily have (any last-but-i, or even) a last element but, if non-empty, can still be written [f(0), …].

Many programming languages include some sort of list data
type; while these usually have special notation distinguishing them from
functions (e.g. the entry at index `i`

in a list `L`

is `L[i]`

where `f(i)`

is the output that a
function `f`

gives for input `i`

) and are commonly mutable
(i.e. one can set the value of `L[i]`

given an extant
list `L`

), they are similar in spirit to the lists here. In some
cases (e.g. ECMAScript, a.k.a. JavaScript) they allow lists

with missing
entries, so [a,,,d,e] would map 0 to a, 3 to d and 4 to e without mapping 1 or 2
to anything; for my purposes, this is not a list, merely a mapping (: :5) or (:
|{0,3,4}).

The empty collection {} is also the natural 0; a mapping (:|0) has no right values, hence nothing to relate anything to, hence no left values, so is in fact empty; since it is a mapping from a natural it is a list, with no entries so denoted [] when considered as such. Each natural is a collection so synonymous with the identity on itself and hence a mapping from a natural; it is thus a list; 0 = {} = [], 1 = {0} = [0], 2 = [0, 1], 3 = [0, 1, 2] and so on. In contrast to collections, lists care about their order: while 2 = {1, 0} = {0, 1} as a collection, the list [1, 0] is not the same thing as [0, 1] = 2. When a list is iso (n| |n) for some natural n, choice of the order of entries gives us permutations (of naturals). One can compose any permutation of a natural n before any list (: |n) to get another list (: |n) with the same entries in a potentially different order.

Define a binary operator & on lists and
sequences, named concatenation

, by:

- (: (: f&g = f&unite;(: g(i) ←i+n :) ←g :{sequences}) ←(:f|n) :{lists})

(It may help to pronounce & as and then

.) Thus (f&g)(i)
= f(i) for i in n and (f&g)(n+i) = g(i), so f&g = [f(0), …,
f(n−1), g(0), …] is indeed the result of concatenating (in the
usual sense of the world, in those technical fields that use the word) the list
f and sequence g. In the special case where g has just one entry, f&[v] is
the result of appending

the entry v to the list f. We can
always write any list [a, …, z] as a concatenation of single-element
lists, [a]&[…]&[z].

Note that f&g allows g to be a sequence but requires f to be a list; the length of f, n, is the offset to be added to g's indices; so n must be finite. The concatenation f&g is infinite precisely if g is; otherwise, it is a list, whose length is the sum of the lengths of f and g, which I shall now show, while also proving that f&g actually is a list or, when relevant, sequence.

Given a list (: f |n) and a sequence g, we have f&g = f&unite;(: g(i) ←i+n :). The ordering of naturals tells us that every natural p either is in n or subsumes n; since no natural is a member of itself, no natural in n subsumes n, so only one of these conditions holds. This order's interaction with addition tells us that any natural p that subsumes n is in fact n+i for some natural i; and that no n+i is in n. This last tells us that f and (: g(i) ←i+n :) have no common right values hence, since each is a mapping, so is their union. If g is (: g |{naturals}) then every natural not in n is n+i for some natural i and g has i as a right value so f&g has n+i as a right value; thus, along with f(i) for each i in n, f&g has every natural as a right value and is (: f&g |{naturals}); the concatenation of a list and an infinite sequence is necessarily an infinite sequence. Otherwise, g is (: g |m) for some natural m and every member of n+m is either in n or equal to n+i for some i in m, hence i is a right value of g and n+i is a right value of f&g; together with all members of n as right values from f, this makes f&g = (: f&g |n+m) and a concatenation of lists is a list, with the length of the concatenation being the sum of lengths of the lists concatenated.

Thus f&g is a list whenever f and g are lists; hence & is closed on lists; when g is a sequence, f&g is also a sequence, so & is as closed as one could hope for on sequences (given that only list&sequence is defined).

Suppose we have lists (: f |n), (: g |m) and a sequence (that might be a list) h; let's compare (f&g)&h with f&(g&h). We have (: f&g |m+n) from the preceding (exploiting commutativity of addition, n+m = m+n), so (f&g)&h = f&unite;(: g(i) ←i+n :)&unite;(: h(j) ← j+m+n :), directly from the specification; and this (exploiting associativity of addition) is just f&unite;(: (g&h)(i) ←i+n :) = f&(g&h), so, & is associative. Since concatenation is also unambiguous, its bulk action's restrictin to lists is a mapping ({lists}: :{lists ({lists}: :)}).

Thus & is closed and associative, thus a combiner, on lists and, aside from its restriction to only taking lists as left values, similar on sequences.

No list h has h&[0] = [1] or [0]&h = [1], since the latter's entry
at index 0 needs to be both 0 and 1 and the former would be some (: f |1+n), as
it's given to be non-empty, whose f(n) is both 0 and 1; neither of these is
possible as 0 and 1 are distinct; thus & is
not complete; it is neither left-complete nor
right-complete. If (:h|p) is a list and f, g are sequences with h&f =
h&g then, as f = (: (h&f)(p +i) ←i :) = (: (h&g)(p +i) ←i
:) = g, we have f = g; so **& is left-cancellable**. Given
lists (:f|n), (:g|m) and (:h|p) with f&h = g&h, this concatenation's
length is both n+p and m+p so these must be equal; as natural addition
is cancellable, this tells us n = m; and then f
= (: f&h |n) = (: g&h |m) = g so f = g, making & right-cancellable,
and hence **cancellable, on lists**.

Note, however, that left-cancellation breaks down when the right operand is a periodic sequence; for example, the constant sequence h = ({0}: |{naturals}) has, for each natural n, (:h:n)&h = [0,…,0]&h = [0]&h = []&h, so we can't right-cancel h. A sequence h is periodic precisely if there is some positive natural n for which h(i +n) = h(i) for all indices i into h (in which case it is necessarily either empty (so there is no i to which to apply this) or infinite, since each input i implies n +i as an input also, so there is no greatest input). Suppose we have lists (:f|n), (:g|m) and a sequence h for which f&h = k = g&h: if n = m then f = (: k :n) = (: k :m) = g as before and f = g. Otherwise, suppose n < m (for the alternative, m < n, swap (:f|n) and (:g|m) throughout in what follows): then f = (: k :n) = (: g :n) and g = f&q with (:q|r) = (: g(i+n) ←i :), m = n +r and r positive; this gives us f&q&h = f&h which left cancellation turns into q&h = h; but, by specification, (q&h)(i +r) = h(i) for every natural i so we get h(i +r) = h(i) for every natural i, for some positive r; hence h is periodic. (Furthermore, q = (:h:r) is non-empty, so h is non-empty, so h is infinite). So we can right-cancel non-periodic sequences, but not periodic ones.

A list f is described as a prefix

and a sequence g as
a suffix

of f&g. In each case f or g is
a proper

prefix or suffix of f&g precisely if neither
empty nor equal to f&g; for f this just means f and g are non-empty while,
for g, it requires f to be non-empty but this doesn't suffice (see below). If a
list (: f |n) is (: h :n) for some sequence h, then we have h = f&(: h(i+n)
←i+n :) and f is a prefix of h; if a sequence g is (: h(i+n) ← i :)
for some natural n and sequence h, then h = (: h :n)&g so g is a suffix of
h.

For a sequence h, for each natural n, I'll describe the sequence (: h(n+i)
←i :) as a tail

of h and as
a proper tail

precisely if n > 0. Every tail of a
sequence is a suffix of it, ever suffix is a tail and every proper suffix is a
proper tail; but some proper tails might not be proper suffixes. For a proper
tail (: h(i+n) ←i :) to not be a proper suffix of h requires h = (: h(i+n)
←i :) which implies that h is infinite and periodic (a.k.a. cyclic), with
(: h :n)&h = h and h(i+k.n) = h(i) for all naturals i, k, as for the case
where cancellability breaks down. When h isn't cyclic, every proper tail of h
is a proper suffix. In particular, no list (i.e. finite h) is cyclic. Note
that, when n is greater than the length of a list h, (: h(i+n) ←i :) is
empty; so every list has empty as a tail and as a suffix.

When we have lists (: f |n), (: h |m) and sequences g, k for which f&g = h&k, the ordering on naturals ensures exactly one of: n < m, n = m, n > m. In the first case, f = (: f&g :n) = (: h&k :n) = (: h :n) and f is a prefix of h; as n < m, h isn't equal to f so f is a proper prefix of h; furthermore, there is some positive natural p for which m = n+p, leading to k = (: (h&k)(i+m) ←i :) = (: (f&g)(i+p+n) ←i :) = (: g(i+p) ←i :) whence k is a suffix of g and, as p > 0, k is a proper tail of g. Conversely, in the n > m case, h is a proper prefix of f and g is (a suffix and) a proper tail of k. The n = m case gives us f = (: f&g :n) = (: h&k :m) = h and g = (: (f&g)(i+n) ←i :) = (: (h&k)(i+m) ←i :) = k. In all cases, either f is a prefix of h and k a suffix of g or h is a prefix of f and g a suffix of k.

Computer scientists are particularly prone to decomposing any
non-empty list f as [f(0)]&(: f(i+1) ←i :) and referring to f(0)
as the head

of f, with (: f(i+1) ←i :) as the

tail of f; in
my terms, the latter is the shortest proper tail of f but by no means the only
tail of f (unless its length is 1, when this is the only *proper*
tail). In deference to this usage, I shall try to avoid using head

as a
synonym for prefix

; the entry f(0) is the head, in the computer science
usage, where the relevant prefix is the list [f(0)], not its single entry.

Finally, & serves as a universal model of all unambiguous associative binary operators, in the sense that any such binary operator * is an image of & under its own bulk action, b = bulk(*), in the sense b(f&g) = b(f)*b(g) for all non-empty lists f, g for which f&g is a right value of b. The bulk action of any unambiguous associative binary operator thus serves as a homomorphism representing that binary operator as an image of &. In the language of categories, & is something like (albeit not strictly, since it's restrictions of it that do the trick) an initial object of the category of unambiguous combiners under homomorphisms in the given sense (in contrast to the composition of relations, which is a final object of this category).

Written by Eddy.