An arrow land, L, is a relation, referring to the members of (|L) and of (L|) as arrows and describing L as composability of pairs of arrows. I refer to the union of (|L) and (L|) as Arrow(L), and to {[y,x]: L relates x to y} as Composable(L).
Where L relates f to g, I'll describe: g as `composable before' f; and f as `composable after' g. If this seems strange (when f appears to the left of - which we normally think of as `before' - g in the pair), consider that a common notation for the application of functions writes f(g(x)) for the action of f on g's action on some x: g acts on x first, then f acts on the result. Thus f (on the left) comes after g (on the right).
Given two arrow lands, U and V, consider the Cartesian product U×V. By definition, this relates [u,v] to [x,y] iff U relates u to x, V relates v to y. We obtain (|U×V) = {[u,v]: u in (|U), v in (|V)} and (U×V|) = {[u,v]: u in (U|), v in (V|)}. These are equal when (|U)=(U|) and (|V)=(V|). Reading the Cartesian product as an arrow land, we find that [u,v] is composable before [x,y] precisely when u is composable before x in U and v is composable before y in V.
The arrow land is a sufficient context in which to introduce duality; it is also the foundation on which I build arrow worlds and all that flows therefrom. It is slightly more general than an arrow world in that it allows some arrows to have empty Post and Prior. Thus, when I define partial orders below in terms of them, I am allowed a maximal (or minimal) element in a strict partial order, which would be forbidden in an arrow world.
In a given arrow land, I'll describe a list of arrows as composable precisely if it is non-empty and every sub-list which is a pair is composable in the arrow land. This incidentally allows single-arrow lists to be composable and ensures that every non-empty sub-list of a composable list is composable. I'll describe a composable list as composable before something iff its last element is: and as composable after something iff its first element is. When the first element of one list, (m|f:), is composable after the last of another, (n|g:), this makes f composable after g: indeed, the list f+g is then composable. When a is composable before k and k is composable before w, I'll describe k as `composable between' a and w (in that order).
In an arrow land L, with each of a and w an arrow or a composable list, define:
aka ({a}:L|) possibly using a's last element (if a is a list) in place of a here.
aka (|L:{w}) with the same proviso. Notice that when h is an arrow, its Post and Prior coincide with those of [h], the list whose single member is h.
I shall, by contrast, describe two arrows or composable lists as simply `parallel' precisely if their Post and Prior are equal (so each is in Parallel(the other)).
Note that Hom(w,w) may be thought of as antiParallel(w). I'll describe two arrows or composable lists as `antiparallel' precisely if they are composable with each other in both orders: taken together, they form a cycle. I'll describe an arrow or composable list as `self-composable' precisely if it is antiparallel to itself - that is, f is self-composable in L ⇔ L relates f to f - that is, f is a fixed point of L.
I'll describe an arrow land, L, as
that is: every arrow or composable list a has Parallel(a) non-empty.
Notice that any self-composable g is in Hom(g,g) in any case: `monotonic' is converse to a tautology. I'll qualify this as `strictly monotonic' precisely if there are no self-composable arrows in L (and, consequently, every Hom(g,g) is empty).
I describe a partial ordering as strict if it is strictly monotonic. Partial orders are, sometimes, known as poSets.
Practicality may equivalently be defined for composable pairs: from that, the given form for (non-empty) composable lists may be deduced. [Proof: For singleton lists, we have the single arrow in the list parallel to the list; for pairs we have a parallel arrow by pair-practicality. Given any composable list and a (non-empty) sub-list of it parallel to some arrow, replace the sub-list with the arrow and you've got a composable list which is necessarily parallel to the original: if the sub-list was a pair or had a pair as a sub-list, the new list is also shorter (and non-empty). Applying this to pairs so long as the list has some pair as a sub-list reduces the list to a parallel singleton list, which is thus an arrow parallel to the original list and the proof is complete.]
For a general relation, r, practicallity says that whenever r relates x to z, there is some y for which: `r relates u to x' implies `r relates u to y'; and `r relates z to v' implies `r relates y to v'. A relation is monotonic precisely if `r relates x to y and y to x' implies `r relates x to x and y to y'.
For any pair of arrows f and g, write f>g whenever f is the last (left-most) and g is the first (right-most) arrow in some composable list which has a pair as a sub-list and has at least one non-self-composable member. It may be worth pronouncing `>' as `later than'. I now proceed to show that this never yields an f>f and that `f>g>h' &implies; `f>h' - the familiar features of a partial order !
If a composable pair, [f,h], is parallel to a self-composable g, thus having g in Hom(g,g), we have g in Post(g)=Post(f) and in Prior(g)=Prior(h), whence h in Post(g)=Post(f): with [f,h] composable, so h in Prior(f), this means h in Hom(f,f), whence f in Hom(h,h). In particular, Hom(f,f) and Hom(h,h) are non-empty: so (as > is monotonic), f is self-composable, as is h.
A composable list parallel to a self-composable arrow is self-composable: its first member is composable after its last. To examine an arbitrary member of a list, it suffices to express the list as t+[f]+h with f the member in question, h the part of the list before the chosen member and t the part following f. Our composable list is self-composable, consequently [f]+h+t is composable and self-composable: with h+t a composable sub-list. Practicality now gives us an arrow k parallel to h+t, making [f,k] a composable list and self-composable: consequently, as before, f is self-composable. This shows that every arrow in a self-composable list is self-composable.
Now, suppose some arrow f appears both first and last in a composable list. Omitting it from either the start or the end leaves us with a self-composable list, with f still present, either last or first. Every member of the list is consequently self-composable. Thus no composable list with first and last elements equal has any entry in the list non-self-composable. Consequently, we have no instances of f>f.
If we have f>g>h, then we have one composable list starting with h and ending in g and another starting in g and ending in f: we can combine these (omitting the repeated g in the natural way) to obtain a composable list starting with h and ending with f. Every arrow in either of the original lists appears in the combined list, so the presence of at least one non-self-composable member of each implies the same for the combined list, so f>h.
Given a partial order, for any collection, C, of arrows, an arrow, f, is described as: an `upper bound' for C if f>g for each g in C; and as a `lower bound' for C if g>f for each g in C. An upper bound, f, of a collection of arrows is a `least upper bound' precisely if there is no upper bound, g, (for C) satisfying f>g. A lower bound, f, of a collection of arrows is a `greatest lower bound' iff there is no lower bound, g, satisfying g>f. Such bounds aren't always guaranteed to exist or be unique.
I'll describe a partial order as a full order iff, for any arrows a and w, there is some composable list in which both a and w appear. If they are equal this is trivial: in any case, a composable list in which both appear yields a sub-list which begins with one of them and ends with the other. If all arrows in this sub-list are self-composable, I expect a and w to be self-composable and composable with one another; otherwise, we have either a<w or w<a. So, in a full order, any two arrows are either ordered, equal or mutually composable.
I'll describe a partial order as unique iff, for each arrow f, Parallel(f) = {f}. This makes `mutually composable' imply `equal': for a, w mutually composable, we have a in Hom(w,w) making w self-composable, so Hom(w,w) = Parallel(w) = {w}, and a in {w} implies a=w.
In the discussion above, I dealt with pairs of arrows. These lead naturally on to discussion of lists and binary trees. Formally, given some variety of item and treating these items as atomic, a binary tree of these items is a pair of which each member is either an item or a binary tree of these items. A list can be defined from scratch, declaring an empty list and a constructor which add items to the start or end of a list: however, any such definition is equivalent to one using ordinals (as follows). One can define a `flattening' operation on binary trees to yield lists: an item `flattens' to the list of length one with it as sole entry; any pair flattens to the list obtained by concatenating the lists obtained by flattening its two members.
For any collection, I, of items, a list of items in I is a function from some ordinal to I. A list is described as finite precisely if the ordinal in question is finite. [Reminder: a natural number, n, is a finite ordinal. As such, it is the set {n-1, ..., 0} of smaller ordinals.] For a list (n|k:), I shall refer to k(n-1) as the list's last element and k(0) as its first element: for reasons which will become clear when you read about the order of composability, below, I shall write the list as (k(n-1), ..., k(0)). In particular, for items f, g, the pair [f,g] is synonymous with the list (2| 0->g, 1->f :I). For any item, f, we have, likewise, the list [f]: I'll refer to such lists as singletons.
I define an asymmetric `addition' on lists: (n|h:I)+(m|k:I) is the union of k with h&on;(m+i->i). Thus [z,...,n] + [m,...,a] = [z,...n,m,...,a]. Note that, as for composition, the right-most list is thus deemed to `come first'.
Define (:I-flat:{lists (::I)}) as follows:
(Most of which can be inferred, given the following - only the special case I-flat([]) = [] is really needed.)
I shall generally write I-flat([...]) as I-flat[...]. Thus, for lists (n|h:I), (m:k:I) and items f, ..., g in I:
This is the concatenation of h and k, with k's elements coming before those of h.
This is the list obtained by appending f to k, as its new `last' element. Notice that I-flat[[f],k]=I-flat[f,k].
This is the list obtained by prepending g to h; I-flat[h,g] = I-flat[h,[g]].
Likewise, for lists or items f, g, h, I-flat[f,g,h] is I-flat[[f,g],h], which is I-flat[f,[g,h]], and similar for longer lists. This is, as for binary trees, a matter of flattening - that is, deleting all but the outermost pair of brackets from the denotation. I'll describe each of f, g, h, when it is a list, as a sub-list of I-flat[f,g,h]. I'll describe a sub-list of a list as empty if it is just [] and as trivial if it is one of: empty, a singleton or the entire list. I'll describe a sub-list of a list as `proper' ⇔ it is not trivial. Note that all sub-lists of a list are contiguous (omitting a member of a list other than its first or last does not give you a sub-list).
Written by Eddy.