I define composition among relations by
from which one may infer that: (a&on;b)&on;c relates w to z iff a
relates w to some x which b relates to some y which c relates to z iff
a&on;(b&on;c) relates w to z; whence that (a&on;b)&on;c = a&on;(b&on;c) -
composition is associative
. Thus we are able to write a&on;b&on;c
unambiguously and likewise for longer (finite) sequences of relations.
The natural mechanism for describing finite sequences is in terms of lists.
I describe a mapping (:|n) as a list precisely if n is a natural; n is its
length
and, when n = 1+i, (:f|1+i) is written [f(0),...,f(i)]; while the only
(:f|0) is [], given that the natural 0 is the relation {}, so (:f|0)
has no right values, hence is itself empty; so [] arises as a synonym for {},
empty and 0. For any type mode, I'll describe (:f:n) as a list of
modes
if i in (|f:) implies i isa mode
. Thus a list
of relations
is a mapping ({relations}:f|n) with n natural. Given a list
(:f|n), we can cut it at position m
, for any natural m which n subsumes,
into the lists (:f:m) and (: f(i+m) ←i :), the first m entries
and
the rest
; the latter is f&on;(n: i+m ←i :) and may as readily be
described as the last n-m entries
; for each m, this gives us a
partition
of f into two pieces.
We can define ({relations}: compose |{lists of relations}) by:
whence compose([a,...,z]) = a&on;...&on;z as one would hope; and
compose is a mapping. For an arbitrary binary operator, *, we can define its
bulk action
, bulk(*) by: bulk(*) relates a to (:f|n) iff
and when * has an identity one may use it consistently as bulk(*,[]). Note that bulk(*) is a relation - bulk(*,h) is ambiguous in so far as either: * itself is ambiguous, or; different partitions of h may yield different values for b*c when the second clause is applied. A binary operator is associative iff its bulk action is a mapping (i.e. unambiguous); in particular, though defined subtly differently, compose = bulk(&on;).
For any relation, r, we have
When r is f&on;g, how are these related to those of f and g ?
First, clearly, (:x←x:f) subsumes (:x←x:f&on;g) and (g:x←x:)
subsumes (f&on;g:x←x:); one can replace subsumes
in the former with
=
whenever (:x←x:g) subsumes (f:x←x:) and in the latter
whenever (f:x←x:) subsumes (:x←x:g).
As to the end-relations, their definitions are:
so we need to examine ({x}&on;f&on;g: y←y :) = {y: x in {f(g(y))}}, which is subsumed by (g: y←y :), and similar. Now,
i.e. the only relevance of {x} and f is in how they constrain g's left values: y is in the right-collection of {x}&on;f&on;g iff f relates x to some value which g relates to y. Now, if (|f:) relates z to x, we know that ({z}&on;f: t←t :) subsumes ({x}&on;f: t←t :); for either z or x to be in (: u←u :f&on;g), f must relate it to some left value of g; and f relates z to all the values it relates x to, hence f&on;g must do likewise. However, (|f:) might distinguish x and z by virtue of one right value each to which it relates only one, while otherwise relating x and z to the same things; in such a case, if those right values of f aren't left values of g (|f&on;g:) will relate x and z to one another, even though (|f:) doesn't. Equally, (|f:) may have values which (|f:g) lacks. The analysis for (:|) proceeds similarly. Consequently,
i.e. the left-relation of a composite subsumes (while having the same
collection of values as) the restriction, to the composite's left values, of the
left-relation of the left component; likewise with right
in place of
left
; and likewise for the end-equivalences.
What are the criteria for subsumes
to be replaced by equals
?
This requires comparison of (:f|) and (|g:). If (:f|) subsumes (|g:), (f:g:) is
just g, so (: (:g|) |(f:g|)) is just (:g|) and (:f&on;g|) subsumes (:g|) while
having the same collection of values as it.
We can use the relationship between end-relations of composites and those of
components to (at least partially) characterise whether a given relation may be
expressed as a composite, for given candidates as left-most and right-most
component: if r is to be factorised as compose([f,...,g]), (|r:) and (:r|) must
subsume ((:x←x:r)| (|f:) :) and (: (:g|) |(r:x←x:)), respectively.
[The left |
seen in ((:x←x:r)| (|f:) :) asserts that every left
value of r is a left value of f, while the whole denotation stands for the
restriction of (|f:) to r's left values.]
If we allow any components between f and g - the ... in [f,...,g] - we can reliably replace them all by their composite - i.e. replace [f,...,g] with [f, compose([...]), g] - so the only cases to consider are whether f&on;g or f&on;q&on;g can be r. For given f we can ask whether there's some g for which f&on;g is r; we can trivially pose this as a request for some q for which f&on;q&on;(:r|) is r; then g is q&on;(:r|). Likewise, for given g, asking for an f for which f&on;g is r can be posed as a request for q with (|r:)&on;q&on;g is r; f is then (|r:)&on;q. So, in all cases, questions about the ability to factorise r via given left and/or right components are, without loss of generality of form: given r, f and g is there a q for which f&on;q&on;g = r ? Clearly, the above gives necessary conditions; are they sufficient ?
Now, if we're given r, f and g for which (|r:) subsumes ((:x←x:r)| (|f:) :) and (:r|) subsumes (: (:g|) |(r:x←x:)), can we find a q for which r is f&on;q&on;g ? Note that, given arbitrary relations f, g and r, we can use (|f:)&on;r&on;(:g|) to obtain a replacement for r which does meet the given conditions; albeit the replacement may quite readily be empty. Note that if either (|r:) or (:r|) is empty then so is the other and so is r; if either f or g is empty and r satisfies the constraints given, then r is also empty. Indeed, when r is empty, q = empty will always give f&on;q&on;g = empty, regardless of f and g: empty is factorisable via anything and only empty is factorisable via empty.
For any relation ({relations}: f :) we can define a binary operator on f's right values by
This may well be ambiguous - there may be several right values to which f relates f(a)&on;f(b) and, as f is a relation, f(a) is an arbitrary left value that f relates to a, so f(a) and f(b) may also contribute ambiguity. Furthermore, we have no guarantee that a composite of f's left values is always a left value of f and the binary operator will only combine a*b if f relates some x to a and y to b for which x&on;y is a left value of f. None the less, associativity of &on; will make * associative if it is unambiguous.
The bulk action of such a binary operator, derived from a relation ({relations}: f :), is then:
When f is a mapping this is just reverse(f)&on;(: compose(f&on;h) ←h :).
Before considering the properties of such a binary operator, pause to consider those of (:x←x:f), f's collection of left values (outputs, if f is a mapping) - which is a collection of relations.
We'll also need to understand the relationship between (| f&on;g :) and (|f:), likewise between (: f&on;g |) and (:g|). If g is a collection, f&on;g is just (:f:g), so (|f&on;g:) = (|f:g).
I'll describe a collection, C, of relations as:
compose(C:f|n) = compose(C:h:n) and f(i) = h(i) for all but one i in nimplies
f = h, i.e. f(i) = h(i) for all i in n.
Written by Eddy.