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: 2013/October).
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 a 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 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.
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, to use the terminology 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|).
Written by Eddy.