I have developed the plaintext denotations below with an eye on the following practical concerns:
Fortunately, this is a field which has been thoroughly explored: and designers of computer programming languages have provided me with ample examples of how plain text may be used expressively towards this end.
Specifically, I use the
emacs HTML mode (the friendly one, based on sgml-mode, whose
sole fault is that I have to type C-c C-t a lot, not the other
html-mode, or the so-called html-helper-mode). If I needed to
use vi or a dumb tablet
editor, I could do so: the use of plain
(ASCII) text as the foundation of HTML is a virtue because it is the most
portable data encoding available. Both the effort of typing markup and the
clutter
it adds to what my eyes see (my brain sees that along-side what my
internal web-browser
says it all means
) help me keep to my chosen discipline
of light markup
- leaving decisions about how to make this look good
to the
user agent which displays the page (and maybe some day I'll write some style
sheets to help it along).
I strive to make the
plaintext math-mode
material amenable to a dumb parser (if once you can
extract it - possibly in ugly ad hoc ways - from the ramblings in which
it is embedded). The following constitutes the spec for the language
to be
parsed. One of these days, when I have richer XML tools to hand, I may well
parse it all up into XML (though I might continue using parseable plaintext as
the form in which to maintain it). The goal of amenable to dumb parsing
is
closely allied to the kinds of simple/straightforward at which I also aim for
the sake of readers learning the denotations.
Just to confuse matters, this page describes old denotations, some of which I'm slowly replacing with new ones. Principally, the new forms reverse relation-denotation texts.
In this page I collect together the denotations I introduce in the
basement of mathematics (which lies mostly
above the foundations), along
with pointers to the discourses which give meaning to my explanations of what
each denotation means. All presume the implicit foundation I introduce under
the banner of naïve logic and the early
stages of my discussion of relations.
I'll use italicised [ square brackets ] to enclose optional parts of denotations; italicised words to denote any (denotation for a) value - using words chosen to describe or identify those values - and; bold words, and punctuators, to denote actual text belonging to the denotation being introduced. I'll use italicised [ square brackets ending in ...] to denote arbitrary repetition: formally, [ thing ...] means [ thing [ thing ...]] - that is, it's optional, if present it begins with thing and after that you can have anything the original could have stood for.
Contents, with illustrations of the most obvious denotations introduced:
This asserts that the two expressions, left and right, are equal: it denotes the value they both have. If evaluation of either expression fails, or if they are not equal, evaluation of this equation as an expression fails. By the nature of this, first [= next ...] = last is consequently well-defined, asserting that all the given expressions are equal.
If the expressions contain some unbound names, evaluation of an equation constrains the binding of these names to values: a binding of names to values is valid if evaluation of both expressions succeeds and yields equality.
This denotes the single member of ({last}: ... unite({next}: unite({first}: relation |) |) ... |), when last is the last in the comma-separated sequence which begins first, next. If the given collection has other than exactly one member, evaluation of this expression fails. Since the definition just given uses denotations I haven't yet defined, I now give the equivalent in terms of the little we already have.
Note that, when f(x) is a relation, ({x}:f|) is {f(x)}, so unite({x}:f|) yields f(x), provided it is a relation, but copes with the failure cases - it yields empty if x isn't in (|f:) and returns a single relation even when ({x}:f|) has many members. [If one used intersect({x}:f|) similarly it would clash with the multi-argument form.] Use of the f(x) denotation, to force failure if non-unique, can be used to limit the matching of names to values.
In which initial and final are expressions, which may introduce names - as may the constraint clause, if present. This last is (read as) a statement: it is included with any constraints, from context, on the values for which any names (whether introduced in the denotation or provided by context) may stand.
The relation denotated relates any given x to given y precisely if there is some match of x to initial which agrees with some match of y to final (agreeing in the sense that any name to which both matches give values is bound to the same value by the two matches).
This denotation for a relation is unashamedly a denotation (plundered from Ponder and Haskell) for a mapping, but without the restrictions needed to make it always denote a mapping. Eliding the restrictions leaves a nice clear definition which manifestly denotes a relation, which may happen to be a mapping if the expressions it uses have the right meanings.
The restrictions would inescapably entwine, in the reading of the denotation, (at least one of): a discussion of when a relation is a mapping, or; some tool for extracting a mapping from a relation. Each of these can equally be defined separately from the denotation, directly in terms of general relations and mappings, rather than in terms of any denotation - and this is generally a more illuminating way to introduce them, quite apart from rendering them applicable even to relations which have been introduced by some other means than the restricted denotation. Thus the restricted form of this definition is less expressive, less powerful and more complicated, while this general form lets us build any tool it could have built.
Since initial and final may stand for relations, and could be
denoted formulaicly themselves, we could, in principle, read x->y->z
at
least two ways: so I define that it is to be read as x->(y->z), which
relates x to the relation y->z. This reading naturally extends to a->
b-> ... y-> z, which is then read as a-> (b-> ... (y->z)...).
One can still write (x->y)->z, for the relation which relates the
relation x->y
to z, of course.
Eliding everything we may leaves {} which denotes the empty
relation - which is a sub-relation of every relation, including equality. [Reminder: a collection is a sub-relation of equality;
and a value x is said to be in
a relation A precisely if A relates x to x.]
More usually, however, one includes some expressions, matches to which may variously be constrained by type, filter and constraint: any value which matches any of the expressions, subject to any pertinent constraints, is a member of the denoted collection. Any constraint given is simply included with those imposed by context.
If filter is given, it must be a relation: only its fixed points are
considered for matching - the constraints effectively include x is in
filter
for each expression, x. If type is given, x is
[a] type
(must make sense and) is likewise effectively added to
the constraints, for each expression, x: a value will only be considered
for matching if it is [a] type
. Both filter and
type constraints can be migrated into constraint: however, the
denotation is a good deal more compact when certain relevant styles of
constraint are given terse denotations - I prefer {linear (V|:U)} over {f:
(V|f:U) =f is linear}.
Note that constraints
and types
are notions to which context is obliged
to give meaning if it is to deploy any in denotations. The given reading of a
type as a constraint, omitting the optional a
, e.g. he is quick
, reads a
type as an adjective. With the a
, e.g. n is a number
, we get a form which
seduces the following rendition of the special case in which only one
expression appears, it is a simple name and the only constraint is a
type: the name is superfluous.
I'll use the plural of a type in {} to mean {type name} without having to use a name: thus, {relations} means {relation s} but lets s be anonymous - in the case of relations, {relation (::)} would do, but I like the better readability of {relations}.
Notice that {0, 0, 0, 0} = {0}, that is, repetition in expressions
is ignored: this is most usually relevant in cases such as {a, b, c} where a, b,
c need not be distinct - consequently, do not assume that such a collection is
as big as
its list of expressions.
This and the previous, &unite;, denotation correspond to mappings, intersect and unite respectively, which can be used to combine an arbitrary collection of relations rather than just the two combined here.
This relates x to z precisely if there is some value, y, for which first relates x to y and last relates y to z. Notice that y need not be unique.
When both first and last are mappings, this is the usual
composition of mappings: formally (f&on;g)(x), is f(g(x)). [That's why
first is to the right of last, and why I'll number lists [last,
..., 1, 0] when I come to introduce them, with 0 in the rôle of first
.
Note, however, that the denotations below, like the formulaic relation above,
read from left to right, being modelled on text, without regard to this
reversal; so that (X|y:Z)&on;...&on;(A|b:C) is (A|y&on;...&on;b:Z), which takes
some getting used to - this is the price of reading function composition in the
opposite order to that used for ordinary text.]
As like as not, you see &union; and the others as an & followed by the
word union
and a semi-colon, ;
. In an ideal universe, it'd be easy enough
for me to arrange that &union; appears as the slightly reshaped U commonly used
to denote intersection; this is the symbol I would write if I had a black-board
and a piece of chalk as my medium of communication. Likewise for intersection
(an up-turned version of &union;, like an enlarged smoothed n
) and composition
(&on; appearing as a small circle, like an o
but raised slightly, so as to be
centred on the line along the top of an o
, or half-way up an f
). These are
the conventional symbols. For why I use forms styled on HTML's character
entities
, see elsewhere.
Constraints and exceptions: in the last case, at least one of the assertions must be present. The optional parts, when present, must be (denotations for) relations. (In all cases, if none of the optional parts is present the denotation is a bit pointless.) In cases with only a relation, of the optional parts, : may be elided where present. (This is boring when it says (:r:) = (r), unhelpful where it says I can write (r:) and (:r): but it lets me keep (r|) as a short-hand for (:r|) for backward compatibility with old texts ... such elision is deprecated and will be retired at a later date.)
If a | is present without an accompanying assert (on its side), the denotation stands for the collection of initial (if on the left) or final (if on the right) values of the relation it would denote if that | were replaced by a : (see below). Thus (:r|) means the collection of final values of r, {y: r relates some x to y}, and (|r:) is {x: r relates x to some y}.
Otherwise, the denotation stands for a restriction of the given relation: this relation composes cleanly after the filter or assertion on the left and before the one on the right.
In any case, where a | appears with an accompanying assertion, as well as denoting what the above says it denotes, the denotation also states that the assert's collection of final (if on the left) or initial (right) values is subsumed by the collection of initial or final (respectively) values of the relation which would be denoted if we replaced the | and its assert with a :. [i.e. (A:f|B) says that (A:f|) subsumes (|B:) - when A and B are collections, this says that every b in B is b = f(a) for some a in A.]
Where the relation is given as a name being introduced by the denotation, it will implicity be one for which any assertions or filters present are vacuous - that is, given A and B, introducing (A|r:B) not only asserts that (|r:B) subsumes (:A|) but also that r = (A:r:B), so that (:A|) subsumes (|r:), which makes (:A|) = (|r:), and (|B:) subsumes (:r|). Given B, introducing (|r:B), the collection of r's initial values, incidentally introduces r whose final values are all initial values of B: while introducing (|s|B) imposes that (:s|) = (|B:).
Thus introducing r, given A and B, with (A|r:B) says that (|B:) subsumes (:r|) and (|r) subsumes (:A|)
So, given collections A, B and a relation r (we could have relations a and b and use (a|) wherever A appears, (|b) wherever B appears), in the absence of any other constraints from context on what is being denoted,
but
note that context will often mess with this, eg a mapping (A::B)
is an
(anonymous) mapping whose initial values are all in A and whose final values are
all in B.
Call the relation this denotes g, for now. If the left filter is present, all initial values of g are final values of that filter, which must be a relation. If the right filter is present, g's final values are initial values of it. If the relation is given, then g relates x to y precisely if: any such filter conditions are met, and; the given relation relates x to y. Thus (a:f:w) denotes the relation which relates x to y precisely if x is a final value of a, y is an initial value of w and f relates x to y; while (:f:) is a synonym for f.
When no relation is given, g is an arbitrary relation satisfying constraints implied by context and the filters. Examples, given (for simplicity) collections A and B:
any mapping (A::B)is a mapping which accepts inputs only from A (though it need not accept all members of A) and each of whose outputs is a member of B (though, again, the members of B need not all be produced).
When the expression is of initial->final
form, it makes sense to allow the filters to depend on names introduced
in the expression: each match of a value to initial or
final is then individually constrained to satisfy its filter. For
example, given mappings f and g, we can introduce (: x->g(x) :{f(x)}) which
is the restriction of g (or, equally, of f) to those values on which f and g
agree: this is equivalent to g(x)=f(x); x->g(x)
or x-> g(x)=f(x)
.
Similarly, given a mapping f whose outputs are relations, and some mapping g, we
have (: x->g(x) :f(x)) as a mapping which takes x to g(x) provided g(x) is
initial for f(x), aka g(x) in f(x); x->g(x)
. When f and g have a smooth
manifold as their input domain, with f(p) being the space of tangents at p, g is
thus restricted to a mapping for which g(p) is a tangent at p - which is just
the formalism needed to define a vector field
or a section of the tangent
bundle
.
This denotes the collection of initial values of (: relation
:filter) - or of relation if filter
is absent. In this
last case, the :
is optional. (Spring 1998: it occurred to me to want
to include it, because that seemed natural, though superfluous; and, when the
relation is a complicated expression, the closing bracket is more
readily recognised if accompanied by its :.) [In principle, given some
collection B, {(|:B)} denotes the collection of collections from which there is
some mapping to B: but this is seldom of interest, since either B is empty (and
the only member of this collection is empty) or this is the collection of all
collections. Likewise, {(|:)} is the collection of all collections.
Consequently, I don't intend to use such minimal denotations with |
.]
This, likewise, stands for the collection of final values of the specified (filter: relation :). Notice that the definition of restriction, above, now means that: for any relation r, r = ((|r): r :(r|)) while; for any relations r, s, ((s|):r:) = (s:r:) and (:r:(|s)) = (:r:s), as only a filter's initial or final values matter, according as it is applied to r's final or initial values (respectively).
Examples, with A and B collections and f a relation:
Wherever the restriction denotation above allows a [filter]
,
with accompanying :
, it may be replaced by an assert
(which
must be a relation) with accompanying |
. This denotation stands for a
relation: indeed, the relation in question is the one obtained by replacing the
| with a :. However, in addition to denoting that relation, this
denotation asserts that its initial or final values are exactly the final or
initial values of assert. Thus, for example (with A, f, B general
relations - but note that when A is a collection, (|A) = A = (A|), and likewise
for B):
fromA to B.
any mapping (A|:B)is a mapping which accepts every final value of A and whose outputs are all initial values of B: if its name is not needed (as when I can refer to it as
it), the denotation is not obliged to name it.
Wherever the asserted denotations just given may have (:
or :)
, the
colon, :
, may be replaced with a |
to denote the initial or final values of
the relation (as if the assert's | were replaced by a
:), while at the same time making the given assertion about the
final or initial values of (:relation:) subsuming the initial or final
values of assert.
Leap-frog this aside to another.
I introduced &unite;, &intersect; and &on; as symbols. I would be pretty happy to replace &unite; with the U-shaped symbol usually used to denote the union operator. Sadly, that's not in the character set.
I could burden some ordinary character, such as U or a punctuator, with the rôle of &unite;. But this would have overloaded other characters, especially as that U isn't going to be the only symbol I want. I tried ;- for a while, but it looks no better (and is easier to fail to notice) than &unite; and the latter at least gives a hint at what it means.
I could produce (or find) a standard set of little image files which (when displayed using a web browser which supports in-lined images) appear as the symbols I want. I'd then be writing <IMG SRC="/img/math/union.png" ALT="union"> where, at present, I type &union;, though I could probably persuade emacs to let me produce these with only a few keystrokes. Font-changes wouldn't affect them, but they'd do the job reasonably well. However, the source file containing my HTML then gets ugly, and I dislike that.
On the other hand, &unite;, though not at all pretty, will do as well as any
other token for the purpose in hand: and is of the form required for HTML (or,
perhaps, a style sheet) to be able to specify that it be rendered as a suitable
U. I could as readily have introduced the word unite
with a special meaning,
it would be shorter, but &unite; gives me the opportunity to mark
the word as
one token
where it appears, in an expression, adjacent to a name.
Those folk using raw text, or old, browsers are going to be meeting ×
in a similar form wherever I use it, and I don't consider it an unreasonable
burden to intelligibility - it's the form in which I read them when using my
authoring tool
(emacs). Indeed, a reader seeing ×, once cued to
know that &...; is to be read as a single token, even gets to be reminded of
what that symbol means (in case it is unfamiliar to them). Anyway, that's as
much apology as you'll get from me for using such ugly denotations rather than,
say, just the word on
. I'll use &symbol; to denote a symbol, using
some (at least vaguely) appropriate word as the symbol where I so chose -
and maybe I'll one day have a way of telling your browser a nice
way to
present it.
Leapfrog this aside to denotations for lists.
I have used the standard denotation, f(x), for the output of a mapping, f, produces in response to an input, x, it has accepted: this leads naturally to defining composition as (f&on;g)(x) = f(g(x)). I have a problem with this, in that mappings, thus written, accept their input from the right: yet when we want to draw the behaviour of a mapping, those of us who read text from left to right generally want to draw the arrow pointing from input on the left to output on the right. Indeed, left-to-right denotations are in common use for functions, as when the input-set is written, then an arrow pointing rightwards to the output-set, to denote a function from the former to the latter: see, likewise, my formulaic denotation for relations (above).
Some mathematicians, I'm told, work consistently from left to right: so that f's output for input x is (x)f or just xf, perhaps. I can see the appeal of this. However, as readily as I can pass f's output, when given x as input, to some second mapping, g, I can equally notice that f's output was itself a mapping, and give it a second input, y. With one convention we get g(f(x)) and (f(x))(y), with the other we get ((x)f)g and (y)((x)f): f comes before g and x comes before y, so one way round forces us to read composition in right-to-left order, the other forces that order on successive presentation of arguments. Either way, we have to live with reading in each order in some places: and this inevitably leads to having to deal with some order-twisting - which I've tried to keep to a minimum and make plain wherever it arises.
Anyway, I want to be understood by physicists, so I'm going to use the f(x) form for function application, with its consequent order for composition. It's taken some work to keep this sweet with plain words (which here read from left to right) and various things which I'll introduce in the order suggested thereby. It is, however, possible: with some studiously judicious choices along the way - such as numbering the rightmost element of a list, when I introduce their denotation, as 0. This will create minor friction when representing a relation as a collection of pairs (lists of length 2), but resolves peacefully.
Notice that supplying a succession of arguments to a mapping (which you can
do so long as its output from the previous argument is a mapping) is written
f(x)(y)(z) when x is the argument f receives, y being then given to f(x) and z
to the resulting f(x)(y). Argument consumption, unlike the composition of
mappings, reads from left to right in formulae: so when I come to identify
mappings which accept several arguments with mappings which accept lists
(wrapping up the arguments to be handed to the mapping), I'll identify f with a mapping which maps [x, y, z] to f(x)(y)(z), so
that the first argument passed to a mapping with several arguments will be the
highest-numbered (or last
) in the list which packs up the arguments.
As discussed earlier, f(x)(y)(z), which really stands for ((f(x))(y))(z),
may also be written as f(x,y,z).
In this bit, you'll have to watch out for the font of [, ... and ] - when [ italic ... ] they're this page's meta-notation, enclosing or denoting something optional, when [ bold ... ] they're part of the denotation for lists. (When actually used, in the examples and real discourses, they'll be used in the ambient font of their context.)
The first of these denotes a list of definite length; the second denotes a list of indefinite length. In the latter, if there is a sequence of items to the left of the (leftmost) ellipsis, ..., this is known as the tail of the denotation; if there are items to the right (of the rightmost), they are known as the denotation's head.
The pattern for a list of definite length matches an arbitrary sequence of items separated by commas: if no items are present, we have only [], denoting the empty list; otherwise, let n be the number of commas present (n may be 0, and we ignore any commas which may be present inside items); the list denoted is then (1+n| :); it implicitly labels the right-most item 0 and, for each item with label i in n, gives label 1+i to the item to its left; the list maps each i in 1+n to the value of the (unique) item labelled i. (The left-most item gets the label n: indeed, the label of each item is the number of commas to its right.)
A denotation using ellipsis isn't as definite about the length of the list denoted: it can be used to say things about a list of any length, subject to a minimum. The simplest case, [...], stands for an entirely arbitrary list (but gives us no name for its length or for any of its entries, so I don't use it much). Otherwise, the list denoted is at least as long as the longest sequence of items separated by commas (ie not be ellipsis): that is the minimum, but it may be longer.
For any comma-separated sequence of items in an ellipsis denotation, we could enclose that sequence in [ ] to get a denotation for a list, s, of definite positive length: the presence of this sequence in our denotation states that the list denoted subsumes s&on;(:n+i -> i:) for some natural n - that is, the list maps n to s(0), 1+n to s(1) and so on: s appears as a sub-list of the list denoted. If the sequence is the head, n is zero: if the tail, then n+(|s) is the length of the list denoted (where (|s) is the length of s); the last (leftmost) item of s is then equally the last item of the list denoted.
Note that the sub-lists given in an ellipsis denotation may overlap, and I
make no assertion here about the order of sub-lists separated by ellipsis: [...,
r,q,p, ..., k,j,i, ...] has the same meaning as [..., k,j,i, ..., r,q,p, ...]
and either may indicate [r=k,q=j,p=i] or [..., k,r=j,q=i,p]. However, the
context specifying such a list may call for p to come after
(ie really
to the left of) k or no earlier than
it (ie possibly allowing [...,
r,q,p=k,j,i, ...], but otherwise with p after k) if that is appropriate.
Most commonly, lists with ellipsis will have no more sub-lists than head and tail, for which we do have a statement about ordering: the left-most item of the tail is the list's last item and the right-most item of the head is its first, so we know the head's right-most item is no later than that of the tail and the tail's left-most is no earlier than that of the head. Thus [z,y,...,c,b,a] may be [z,y=c,b,a] or [z=c,y=b,a]: but, otherwise, the head and tail given can't overlap. Indeed, similarly, [z,..., k,j,i, ..., a] is, at its extremes, [z=k,j,i, ..., a], [z, ..., k,j,i=a] or, even, [z=k,j,i=a]. As a final example, which will arise often, I'll write [z,...,a] for an arbitrary non-empty list: this may be [z=a] with one item, [z,a] with two, or some longer list starting in a and ending in z: for any natural n, a list (1+n|f:) is then [f(n),...,f(0)] without having to treat the case n=0, hence (1|f:), specially. I'll generally give [] special treatment, though - it tends to warrant it.
Lists suffice for a definition of the binary operator ×, denoting the Cartesian product: for relations r, s, we get s×r = Rene([s,r]) relating [u,v] to [x,y] precisely if s relates u to x and r relates v to y: when r and s are collections, this is the collection of pairs [u,v] with u in s and v in r. More generally, we have (| s×r :) = (|s)×(|r) and (: s×r |) = (s|)×(r|).
Of course, I should really write an XML description of that and an XSL program to convert it into the denotational forms given above.
Written by Eddy.