- [[ constraint , …] constraint ; ] left ← right
- left ← right [ ; constraint [ , constraint …]]
- arrow formulae
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. - { [ expressions [ : constraint [ , constraint …] ]] }
- formulaic collection
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 animplicit 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. - relation &unite; relation
- relates x to y precisely if
either relation does.
- relation &intersect; relation
- relates x to y precisely if both relations
do.
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.

- left &on; right
- Composition.
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.

- ( [ left ] : [ relation ] : [ right ] )
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.