For a good over-view of the state of the art in putting mathematics on the web (in orthodox notation), see Jukka Korpela's page on the subject (my last visit: 2004/March).
At the same time I'm going to take to heart the order of terms in g&on;f
maps x to g(f(x))
. Either g or f may be replaced by any text which denotes
a mapping. Such texts have a natural split into things said about the inputs,
things said about the outputs and things said about how the former are mapped to
the latter; the beginning, the end and the middle. When we come to substitute
texts for f and g, the result will read more clearly if the leftward end of f's
text and the rightward end of g's texts are discussing the values which mediate
&on; in g&on;f
, namely f's outputs, in so far as they are g's inputs.
This makes the leftward end of a mapping's text discuss the outputs, while the
rightward end discusses the inputs. Then (W:g:V)&on;(V:f:U) = (W:g&on;f:U) will
read more amicably than would (V:g:W)&on;(U:f:V) = (U:g&on;f:W), especially when
the chains of composition get long.
There is an unavoidable conflict in order involved when g(f(x,y)) passes
first x, then y to f, passing on the result to g; x was followed by y, but f was
followed by g; one half reads left-to-right, the other right-to-left, because
each, in effect, reads away from
positions between a mapping and its
first input. Having f(x,y) mean (f(x))(y) is so much more intuitive than having
it mean (f(y))(x), just as (g&on;f)(x) means g(f(x)) rather than f(g(x)). So I
can have either order of input or order of composition read left to right (like
my English text), but the other has to read right to left (like Arabic). For
the sake of g&on;f maps x to g(f(x))
, I've chosen to endure right-to-left
as the internal structure of texts denoting mappings, with left-to-right then
arising as the convenient order for supply of inputs.
A mapping, f, from members of A to members of M must thus end up denotable as (M? f(a) % a !A) for some enclosure (...) and punctuators ?, % and ! so as to put the input truths, a in A, on the right and the output truths, f(a) in M, on the left, while separating the several sub-texts which may be substituted in place of M, f(a), a and A. This will mean that, at least when f's outputs are mappings f(a) = (Z? f(a,n) % n !N), f is denotable as (M? (Z? f(a,n) % n !N) % a !A) in which f(a,n) mentions a and n in the reverse of the order in which they subsequently appear. I can (and shall) chose different punctuators, but I can't avoid a reversal somewhere.
Now, all that applies to mappings, which are a particular flavour of
relation; so I want denotations for mappings to be special cases of denotations
for relations. The need for reversal arises, for mappings, out of the f maps
x to f(x)
form of denotation, only pertinent where we use the f(x) mode of
denotation, which is only familiar in so far as it connects to mappings. None
the less, I'll have relations of form (M? m % a !A) and it would be nice to be
able to read this as a relation which relates m (in M) to a (in A). To do so
will read a mapping, f, as relating f(x) to x, in the reverse order to that used
when describing it in the language of mappings, where it maps x to f(x); this
will make the verbs map
and relate
describe a given thing
differently, but does not disturb the sense of what is happening.
I intend to counteract ambiguity with a systematic integration of
equivalences into the restriction/end-relation denotations; a context doesn't
care about ambiguity in so far as all the values a given denotation may stand
for are equivalent, for that context's purposes. If a relation r = (B:r:A),
with A and B equivalences, the appropriate replacement notion for mapping
[recap.: (B:r:A) is a mapping if it maps each a in A to precisely one r(a) in B;
so r relates a unique r(a) in B to each right value, a, of r] becomes; if r
relates d to c and b to a, A relates a to c
implies B relates b to
d
; the appropriate replacement for monic
says the converse. So, to
be an iso-mapping from A to B
, (B:r:A) must respect
equivalence:
(:B|)-equivalent values will only ever be related to (|A:)-equivalent values; if
(:B|) can distinguish two of r's left values, (|A:) can distinguish the
corresponding right values. To be iso-monic from A to B
, (B:r:A) must
respect distinctness: if (|A:) can distinguish two right values, (:B|) can
distinguish their corresponding left values; to (:B|)-equivalent values, (B:r:A)
only ever relates (|A:)-equivalent values.
[need to separate this iso- meaning from that of iso-clean, q.v.]
Indeed, one may construct collections of relevant equivalence classes, AA = {{x: A relates x to a}: a in (|A:)} and BB = {{y: B relates b to y}: b in (:B|)}, and construe r as monic or a mapping AA to BB if it's iso-monic or an iso-mapping, as appropriate. However, reducing to equivalence-classes induces artifacts into the discussion which I suspect the iso-map/iso-monic notions may help to assuage.
Template: left [ = right ...]
Note that the template allows there to be no right texts, just the left text; in which case the definition says it means exactly the same as the given text, as one would hope, given that it can't be distinguished from that text.
There is a choice to be made when left = right is used with potentially ambiguous texts:
clearly the denotation is then ambiguous, standing for any value for which there
is a disambiguation of the two texts yielding that value for each text. The
choice is: should the assertion be that every disambiguation produces such
agreement, only that some must, or that for each on either side, there's
agreement with at least one on the other side
?
Notice the difference between:
and consider what f&on;g(x) should mean; clearly f&on;(g(x)) and
(f&on;g)(x) = f(g(x)) are the two possible candidates; except in odd
circumstances, they mean different things. Analogously, in f(w)&on;g(x) there
is clearly no need to enclose (f(w)), making it natural to read f(w)&on;g(x) as
the result of composing f(w) to the left of g(x), i.e. f(w)&on;g(x) wants to
be read as
(f(w))&on;(g(x)) (and all the more so when we look at
f(w)&on;g(x)&on;h(y)&on;...). Given this, it makes sense equally to read
f&on;g(x) as f&on;(g(x)) - after all, the alternative, (f&on;g)(x), already has
the handy synonym f(g(x)). So I'll have evaluation bind more tightly
than
composition, in the language of computer language designers.
It is possible to unify all the various denotations in these sections; I'm not convinced it's any clearer, but I like it anyway.
in which left, right and relation, if
present, are relations. In explaining what this means, I'll describe the left
use of {:;|}
as the left punctuator
and refer to
left (or its absence) as this punctuator's
constraint; likewise, right is the constraint of
the right punctuator
. If both punctuators are |, at most one of left and
right may be omitted.
Where a punctuator is | and its constraint is present, the denotation stands for the same value as it would if this | were replaced with a :, but makes an additional assertion (to which I'll return). If a punctuator is | and its constraint is absent, in which case either the other constraint is present or the other punctuator is : (or both), the denotation stands for a relation among relation's values on the side of the unconstrained |. Otherwise, the denotation stands for a restriction of the relation.
If both punctuators are :, the denotation makes no assertions: it just stands for the relation which relates x to y precisely if
(If any of left, relation and right is
present but not a relation, this implies that the denotation stands for
the empty relation, since no x, y meet these requirements.) Note, in
particular, that (::)
is a valid use of this template; absent any
constraints, it stands for the all-relation, which relates any x to any y
unconditionally. For a given relation, r, its collection of left values may be
written as (:x←x:r), its collection of right values as (r:x←x:).
When one punctuator is | and its constraint is absent; for the relation obtained by making both punctuators : write r; then
These are relations among, respectively, the left and right values of r; intersecting each with its reverse yields an equivalence which says r doesn't distinguish the relevant values - it relates them (if left) to the same values or (if right) relates the same values to them.
Where a punctuator is | and has a constraint,
the assertion it makes concerns the two equivalences on either side of
it
. One is a constraint, call it s; eliding s from the original denotation
will leave the denotation for an end-relation of the rest
of the
original; if it's the left-relation, call it e, otherwise call its reverse e.
Put a | on the same side of s as it appeared in the
original, a : the other side, wrap in (...); if that's s's
left-equivalence, call the result c, otherwise call its reverse c (because it's
the constraint
). The assertion says that e conforms with
c -
which roughly says that: e's values include at least one member of each
equivalence class of c, and; e respects the equivalence c, in the sense that if
c deems two of e's values equivalent, so does e. Thus
i.e. (e:c|) subsumes c and e subsumes (e:c:e).
and all three stand for (A:r:B), which relates x to y iff x in (:A|), y in (|B:) and r relates x to y.
The notion conforms with
, used to define assertions in the above, is
designed to ensure that composing the two relations separated by the | will have
some helpful properties. Specifically, (:f|g) ensures that f&on;g has all the
same right values as g; while (f|g:) ensures that f&on;g has all the same left
values as f. In a similar vein, it makes sense to consider (B:r:A) as a map
from A to B
when (:B|) subsumes (|r|A); and as monic from A to B
iff
(|A:) subsumes (B|r|).