This is somewhat disorganised but isn't high among my priorities. It is at least partially made redundant by my more recent work on notation, especially its parsing.
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).
(but not in that order – and my thoughts in this section remain exploratory)
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 quotes
–
i.e. “sub”
or ‘sub’
but implemented using HTML's Q element – 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, so as to suppress any matching of patterns by either some text
before sub and the leading part
of sub or some trailing part
of sub and the text
following sub. For example, (a+b).c is
distinguished from a+b.c = a+(b.c).
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.
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'd rather not switch to &mido;, ∪, ∩,
⊗, even if they existe and produce 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).
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 outputs (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:
denotes a value, v; and, when mode is
present it must be a type; it asserts 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 this text 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, and the
type name
with the some
form – 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
Written by Eddy.