erm ... this is somewhat disorganised but isn't high among my priorities
Context comes in many forms. This text presumes that its reader inhabits a cultural context which provides for making sense of the English language. (It even presumes that it is read via some mechanism which provides for making sense of various protocols and languages designed by the assorted processes which make up the worl-wide-web consortium, the internet engineering task force and various other organisations.) Every nugget of information of which you have made sense contributes to the context in which you interpret your subsequent experiences, hence equally to such sense as you make of these. This document constitutes a context - in the form of a text - in which I seek to prepare my reader to be better able to make sense of the mathematical texts on my web site.
The boundary between natural
and formulaic
language includes
an overlap; certain stock turns of phrase (as they appear to natural language)
are sufficiently characterisable to allow me to describe them as if they were
formulaic. [So the following might reasonably be used as preamble to my plaintext denotations.] I'll set out various such,
below, along with the meanings I formally give them - and a little guidance on
how this relates to other familiar idioms (including natural language).
Context gives meaning to some texts, but not all; nor, indeed, to arbitrary chunks taken out of a text (even when context does give meaning to the given text, as a whole). In so far as context;
I'll describe each of the meaningful fragments thus combined as a sub-text of the composite and of any text of which the composite is a sub-text. Thus, in giving meaning to a text, context builds up a sub-text hierarchy. Each text in this hierarchy provides the context for its sub-texts.
In the following descriptions of formalised idioms, I'll employ the meta-denotations that I introduce to encode my formal denotations.
To aid the reader's decomposition of the text into this hierarchy, I use
(sub), {sub},
[sub] and even ‘sub’ as
enclosures; call the left-hand character of each its opening,
the right-hand character its closing (and allow that other contexts may
provide other enclosures); so, in (sub) the opening is
(, the closing is ), sub being an arbitrary sub-text; the
whole stands for exactly the same meaning as sub, but is separated
from
surrounding text enough to eliminate some ambiguity there might otherwise have
been.
Because each denotational template I provide: uses at most one (verbatim)
opening, always using (after it) the matched closing; and likewise uses at most
one closing, always as a match to an earlier opening; one can infer that any
text to which my defnitions give meaning has properly nested
enclosures.
This helps the reader scan (parse) the text: begin by identifying the hierarchy of openings and closings and use it as a framework around which to work out the meanings of the fragments into which the enclosures cut the text; the enclosures serve as a guide to working out what the text means.
One problem for a parser will be that I have (technically
ab-) used the `grave accent and
apostrophe' as ‘left and right single quotes’' which would make
it non-trivial to parse ‘x isn't in A’ and similar texts matching
`sub' when sub includes an apostrophe. Indeed, this
is why I've now started switching to using quote entities
(the HTML Q
element) and the proper ‘ and ’ character entities. The
change-over will, however, take a while.
I'll use (sub) in particular to separate the parsing of sub from that of the surrounding text; this typically serves to rule out some ambiguity, as between a*(b*c) and (a*b)*c when * isn't (known to be) associative. This effectively asserts that any sub-text which straddles either the ( or the ) also straddles the other: absent any other denotation giving meaning to the shortest such sub-text, (sub) means whatever sub means. Note, however, that restriction/end-relation denotations, along with some conventional denotations (e.g. f(x) for function invocation) also use this enclosure - their meanings take precedence !
Generally, a word or symbol has some (e.g. natural language) meaning to the
author's intended audience; but, when context has described some formal
structure (or property of one), the author may chose to declare a specific
meaning for some chosen word, typically so as to refer back to that (possibly
complex) structure tersely thereafter. Likewise, the author may chose to use
(some text having roughly the form of) a word as a name by which to refer to
some value, e.g. when it has only been partially specified or to save writing
out some convoluted formula which specifies it. It is conventional (and very
convenient) to use certain texts as symbols
, e.g. to denote binary
operators such as addition - writing plus(a,b) is nothing like as handy (or
familiar) as writing a+b, in which plus, a and b are names and + is a
symbol.
The main flow of text may sensibly exploit natural language idioms to announce such namings, whether of values, notions, types, operators or whatever. I'll rely on that main flow for introduction of symbols but intend to enable denotations to supplement this mechanism with ones suited to their meanings. To this end: in so far as a text is being used as a name, it stands for an arbitrary value subject to whatever constraints context imposes on it.
It remains to decide how denotational definitions should make clear which
uses of a name are to be understood as referring to the same value. This needs
enough locality to allow the uses of a
in the threee primary sub-texts of
(A: a←a :) = {a in A} = (: a←a :A)
to operate independently of
one another, yet must let the uses of A
be tied together, albeit allowing
even these to appear as dummy - e.g. in {relation A: (A:a←a:) = {a in A} =
(:a←a:A)}, the collection of reflexive relations. What are the sub-texts
within which we quantify over variation in
any given name ?
To formalise name-value binding
in terms of the parse-tree of
sub-texts which describes a text used as a formula is to determine, for each use
of a name in the formula, the sub-text which disambiguates
that use of
the name. Within this sub-text the name takes one value at a time
; the
sub-text may collect together
(in one sense or another) the values for
which all its assertions hold true, or it may make some overall assertion about
each value which meets the internal assertions of the sub-texts of which it is
composed.
In the parse-tree, each node (at each reading of that node) is provided
with values for
some names by its context - effectively the namespace
available to the node's parent in the tree - and quantifies over
some
(other) names used within the sub-text; these, collectively, form the namespace
from which our node provides (at least some of) its children with values for
names.
Can I distinguish between names used in a sub-text which must be provided by
context and those which may be imposed on by context ? The latter are
quantified over (by the node) if not provided by context. This would have
denotational forms distinguishing their sub-texts into those whose must be
provided
names it will quantify over and those the form's composite text
will demand, in like kind, of its parent node in the parse tree. Any name, as a
sub-text, imposes must provide
on its parent node; if its parent
propagates must provide
from the sub-text (in its denotational form) as
which the name was used, follow up the parent-links to a parent node which
doesn't propagate it; call this the first flexible ancestor of the node as which
the name appeared. Do this for each sub-text which is a name; wherever the
first flexible ancestor of one use of a name is a descendant of the first
flexible ancestor of another use of the same name, these two uses of that name
will participate in the same disambiguation: the latter's disambiguation will
provide a value to satisfy the former's requirement.
It would thus appear that I can resolve the problem of scopes and
name-binding by specifying, for each of the (non-verbatim) sub-texts combined by
each denotational template, whether the composite propagates must provide
or is prepared to resolve it. (The latter need not mean that the composite
does resolve it, only that it will for any names not resolved by its
context - i.e. by some ancestor node in the parse tree which resolves each given
name.) The enclosures (see above), when appearing simply as such (rather than
as part of some denotational template involving other punctuators), propagate
must provide
.
A context using the following tools is at liberty to use any manner of text
as a name
or symbol
, though it behoves each author to give some
though to enabling readers to be able to identify which texts are so used.
I'll use some ASCII punctuators, +=-\*/%@^~#
at a guess, as symbols,
along with some &blah;
tokens, some of which your user agent (try:
<·>×÷±&
on yours) might even render
roughly the way I have in mind; I have no good reason to expect any user agent
to know about some (e.g. &on;&unite;&intersect;&tensor;
) that I use, but
never know how lucky we might get and, in any case, chose words to go between
& and ; with an eye to their being intelligible to the reader
who doesn't see the symbol I had in mind (so I wouldn't switch to &mido;, ∪,
∩, ⊗, if they existed and produced the symbols they vaguely describe,
until user agent support seems ubiquitous; and I'd prefer the semantic names
over the display names if I got the choice - e.g. × for × is
better than &diagcross; or similar would be, even if it displayed the same).
As soon as I've got my home computer connected to the outside
world again, I'll be upgrading my browser to one which supports a better
solution to this (namely: full support for CSS 2); I'll then upgrade my web-site
to use HTML elements - such as <unite> in place of
&unite; - in conjunction with style sheets which map them to
suitable things. For you to be seeing this
paragraph, I must already have connected, but it may take a while after that
before the rest catches up; if
displays as an × inside a
circle, we must be part way there already ;^)
I'll also use ← as a left-wards pointing arrow; though, formally, it's
just the syntactic token I use, regardless of how it's displayed, between left
and right values in denotations for relations. It points left-wards because,
when the relation is a mapping, the denotations I introduce interpret right
values as inputs and left values as output (for the sake of reading g(f(x)) as
passing x as input to f and f's output as input to g). Functional programming
aficionados may wish to pronounce ← as adbmal
, since its meaning is
roughly a reversed lambda; though it is perhaps better to pronounce it as a
function of
.
I'll also use some &blah; tokens as names, notably π, usually for
conventional reasons; otherwise, the texts I'll use as names will consist of
digits, letters and maybe the occasional underscore, e.g. 0, th1ng2, a_Name. In
particular, the standard denotations for numbers will end up being specified as
digit-sequence names
with a particular formalised reading.
Thus far, all has been so general as to consist solely of formalisation of anglic idioms; to go further, I must introduce the type which takes centre stage in my expression of mathematics: relation.
I anticipate that texts using the denotations I offer shall introduce
various ways of denoting values
; I make few presumptions about the values
so
denoted
, so as to make the tools as widely applicable as possible. In order
to be able to build any tools; I presume that much of the semantics of such
texts concerns itself with truths
relation.
I presume context provides some notion of equality
among the
values
, and this notion is close enough to natural language idiom to
allow it to be encodable using what I'll describe (in due course, and consistently with the orthodoxy
which educated me) as an equivalence relation
.
The following formalises, in the spirit of the above, the language I use when discussing relations and their specialisations.
relation
In so far as context gives meaning to texts
of this form I shall presume it does so in terms of readings of left and
right as values; in such a case, I shall describe this as
a relation
; I'll also describe left as a
left value of this and right as a right
value of this.
I thus give meaning to relation
as a type. In my own texts, I deal
with relations as values; indeed the only involvement my mathematical texts have
with any other kind of value is to allow that they may be the things relations
relate to one another. Absent any further knowledge (aside from the
equal/distinct dichotomy) of the things related, I provide tools for describing
the relations among whatever values context may introduce; and build the tools
within a context which only provides relations as values.
At the same time, for any relation r, the above gives meaning, as types, to
left value of r
and right value of r
. The following gives
alternate names for those types, when r is a mapping.
in which input and output must denote values and
this must denote a relation; asserts that this relates v to
input
iff v=output
. This, in particular, says
output is the only value this relates to input. I shall
describe a relation, r, as a mapping
precisely if: r relates z to a
iff r maps a to z
. Thus is mapping
given meaning as a type.
in so far as each relation denotes a relation and member
denotes a value, a denotation of this form denotes member's value and -
for each place where in separates a value, v, on its left (whether
member or a relation part way down the sequence) from a relation,
r, on its right - asserts that r relates v to v. Thus a in C
tells us
that C relates a to a
and stands for a's value; I'll write the assertion
this makes as a is in C
, thereby giving meaning to in C
as a type
for every relation C. This can, conversely, be used to give each type meaning
as a relation which relates every value of that type to itself.
I can integrate my formalisation of types with natural language and orthodox formal usage by applying the following formal uses of words:
asserts mode is a type
and denotes a value, v, for which
v isa mode
. If expression is omitted, the value denoted is
otherwise arbitrary; this is taken to be the case unless context allows us to
give meaning, to the text following mode, as a value - possibly requiring
us to give values to some names used in it to achieve this - but in that case it
is understood as an expression whose value is asserted to be equal to our
arbitrary v; this may constrain v and any values given to names introduced in
the expression.
Note that this definition is circular: it depends on using the type
value
with the a
form of the definition itself - here I am obliged
to rely on the reader's understanding of this as text written in English. The
only reason for including it is to indicate that I intend to use this English
idiom with a modicum of formality - and to tie a wide variety of usages
together, to give someone trying to decrypt this text (because totally ignorant
of English) a slightly easier job.
Example: given some mapping f, any linear f(x)
is given meaning as a text
which: denotes a linear output of f (whose outputs need not all be linear, nor
need every linear be an output of f, nor need f be linear) and gives meaning to
x as an input to f for which f(x) is linear; the expression any linear f(x)
is
ambiguous in so far as f has several linear outputs; and, for each value allowed
to it, x is ambiguous in so far as f maps several inputs to that output.
Replacing f with a relation would add yet more (potential) ambiguity.
Asserts that mode is a type and denotes (or, arguably, is) a
type, namely that T for which: sub isa T
iff sub is a type and:
v isa sub implies v isa mode
.
Asserts that mode is a type and denotes (or, arguably, is) a
type, namely that T for which: form isa T
iff form is a type and:
v isa mode implies v isa form
.
Thus this isa specialisation of that
iff that is a generalisation of
this
. Later I'll have the option of identifing a type with the collection of
values of that type, which will make the meaning I'll give to sub-
turn
specialisation
into a synonym for sub-type
.
When [qualifier] mode is a specialisation of the type
relation
, with qualifier living up to its name if present (e.g. by
being an adjective), a text matching this template asserts that this isa
[qualifier] mode and denotes (arguably: is) a type. When proper
is omitted, the type, T, denoted is specified by that isa T
iff
this subsumes that and that isa [qualifier]
mode
; if proper is present, the type denoted is similar, with the
added constraint that context distinguishes between this and that
(i.e. that doesn't subsume this). Consequently, any [
qualifier ] sub-mode of this isa [ qualifier ] mode and
is subsumed by this
.
Note: a subsumes
b
iff b relates x to y implies a relates x to y