A list
is a mapping from (all of)
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 often more apt to use a pair (i.e. an atomic relation x←y for the specific values x and y to be paired), unless the context naturally generalises to many values, in which case it is better handled using lists (even in the special case where those lists are of length two).
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), …].
A mapping (: f :n) for some natural n, potentially with some i
in n that are not right values of f, is known as a partial
list. Likewise, when n is either a natural or {naturals}, f is called a partial
sequence. A partial list (or sequence) which has a right value m that has a
member i that is not a right value of the partial list is not a list (or
sequence), since there is thus no natural n for which it is (: |n), as that n
would need m as a member, hence would have i as a member, but it is not a right
value. (For the case of a sequence, n = {naturals} would still fail for the
same reason.)
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, 2 to d and 4 to e without mapping 1 or 3
to anything; these represent partial lists.
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:
(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 non-empty list (i.e. finite h) is cyclic
(and empty has no proper tails or suffixes). 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.