Formalising Text

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.

Formalised Anglic Idioms

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).

Basics: (scopes,) names, symbols and bracketing

(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 !

Names and symbols

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.

Scopes and Namespaces

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;, &cup;, &cap;, &otimes;, 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. &times; 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.

Relating values to one another

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

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 semantics of relations

The following formalises, in the spirit of the above, the language I use when discussing relations and their specialisations.

this relates left to right
the type 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.

this maps input to output

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.

member [ in relation …]

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.

Specialisation and Generalisation

I can integrate my formalisation of types with natural language and orthodox formal usage by applying the following formal uses of words:

{ any ; a ; an ; some } mode [ expression ]
{ any ; a ; an ; some } mode [ , expression , ]
{ any ; a ; an ; some } [ mode ] expression

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.

specialisation of mode

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.

generalisation of 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.

[ proper ] [ qualifier ] sub[-]mode of this

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

Valid CSSValid HTML 4.01 Written by Eddy.