in which left and right are expressions – which may involve names – and each constraint, if any, is a constraint. [In older texts I have used a , where the first template mandates ; to make reading easier … 2001/May/27. I am now exploring putting the constraint after the template … 2002/Jan/7.] The whole denotes a relation, which relates each value left may take to whatever value right may take, subject to all pertinent constraints. The composite may quantify over names for which any of its sub-texts (left, right and any constraint) require context to provide values.
Thus, for instance, f(x) ← g(x) denotes the result of composing f
(which is f(x)←x) to the left of (i.e. after
, when f and g are
mappings) the reverse of g; the latter being x←g(x). Most usually,
however, right will be a simple
name; left will usually be some formula
involving that name; though not uncommonly both will be simple names, with
some constraint to specify the details. Almost
invariably, ← denotations will be enclosed in (:…:) if in nothing
else: for reasons which shall emerge below, this is fatuous, but the enclosure
is often an aid to reading.
in which (in so far as each is
given): expressions must
be an expression sequence
(in or form, generally implicitly, with optional
type qualifiers and filtering), and
each constraint must be a constraint. Each member
of the collection is a value of expressions
subject to any constraint. Note that everything
inside the { } is optional, so that { }
is a collection: there being no expressions, no
value is a member of this collection, so { } denotes the empty collection.
[I'll more usually write empty as {} without the space inside it; or call it by
its name, empty
.]
A formulaic collection implicitly quantifies over
all ambiguity in
the value of expressions. Note that use of
expression sequences provides for an implicit union
, i.e. {a, b: a in
A, b in B} stands for the union of (the collections of fixed points of) A and
B, even when B is empty – as noted when discussing expression sequences
– requiring enough slack to ignore a constraint which doesn't involve a,
even indirectly, while evaluating the expression a in the sequence.
This and the previous, &unite;, denotation are binary operators. They correspond to mappings, intersect and unite respectively, which can be used to combine arbitrarily many relations rather than just the two combined here.
This relates x to z precisely if there is some value, y, for which left relates x to y and right relates y to z. Notice that y need not be unique. This combines the relations left and right to produce a new relation; as such, &on; is a binary operator.
When both left and right are mappings, this is the usual composition of mappings: formally, (f&on;g)(z) is f(g(z)); f relates this to g(z), which g relates to z. Note that I require the enclosure here used around f&on;g to distinguish this from f&on;g(z), which I intend to be read as synonymous with f&on;(g(z)), which relates f(g(z,y)) to y – i.e. g(z) maps y to g(z,y), which f then maps to f(g(z,y)) – whereas (f&on;g)(z,y) is f(g(z),y), the result of passing y to the function (f&on;g)(z) = f(g(z)).
Note that I am here using character entities which are not a standard
part of the normal HTML repertoire, as
explained elsewhere. Frustratingly, my tablet and 'phone browsers lack
fonts supporting (at least) the composition operator; I should
work out how to provide a web-font via my style-sheets, that includes the needed
glyphs. Even on desktop, I've seen &on;
and
for &intersect;
displayed normally, rather
than bold, in the templates above.
in which left, right and relation, if present, are relations. A text matching this template denotes a relation. Let P = relation if present, else P is an arbitrary relation. If left is present, let L be its collection of right values; else let L be P's collection of left values. If right is present, let R be its collection of left values; else let R be P's collection of right values. The whole denotation then stands for L&on;P&on;R; as L and R are collections, their sole effect here is to restrict which left and right (respectively) values of P are retained.
In particular, the denoted relation's left values are all right values of left (when given) and its right values are all left values of right (when given); when these are collections, the result is simply to restrict relation by imposing these requirements on its left and right values. More generally, we can use these denotations, applied to the universal identity, to denote the sets of left and right valueas of a relation r as (:x←x:r) and (r:x←x:), respectively; I'll call those the end-collections of r.
When relation is absent (so that P is arbitrary) the whole denotation stands for an arbitrary relation between the right values of left and the left values of right, subject to any further constraints imposed by context. For example, {mapping (B::A)} means the same as {mapping f: f = (B:f:A)}.
From July 2004 to April 2012, I had restrictions also compose the restricted relation with end-relations from the restrictions; but I never found a good use for it, was in two minds about which end, if either, should use a reversed end-restriction and didn't like some of the complications implied, so reverted to the above, which is roughly what I had before.
I also need (2017…) to settle how this ties
into homomorphisms,
where left and right
may identify algebraic structures; they contribute their collection of values,
tacitly, as the restrictions above; but they also assert that the denoted
relation not only relates values but is also tagged
with those structures
at its two ends, for the purpose of morphing between structures. Perhaps, in
fact, have the above be the base case of the notation but allow contexts to
extend it by using things other than relations in the three positions.
Written by Eddy.