This has necessitated a complete break from the historical line of development, but the break is an advantage through enabling the approach to the new ideas to be made as direct as possible.

P.A.M. Dirac, 1930/May/29.

Plaintext Denotations

Context I discuss elsewhere. The following will, in places, differ from what I have used outside the new tidy area; I've been more brutal about the order of terms in various texts, and I'm exploring the use of equivalences as infrastructure for manipulating ambiguity.

In widespread support of handling ambiguity and equivalences, I'm generalising in, which relates each member of any collection to that collection, to have any relation in place of the collection, primarily so as to allow that a value is in an equivalence precisely if it's in the equivalence's collection of admissible values. Like Humpty-Dumpty, I declare a meaning for in and presume that meaning for it thereafter: a in A means A relates a to a, a.k.a. a is a fixed point of A. Since I'll encode collections as relations which relate each member to itself, this will carry over its meaning for collections transparently. In many of the contexts where I have used collections in the past, I now support arbitrary transitive reflexive relations (most notably equivalences), indicating the collection of values thereof while asserting that the context respects (and is oblivious to) the relation in relevant senses. The end-collections denotations of relations have become end-relations (via a period as end-equivalences, now – since 2004/June – generalised via subsumes) and, in various contexts, I provide for an arbitrary relation to tacitly provide one of its end-relations as a transitive reflexive relation.

I've also settled on a choice of language: for the sake of composition in a context where a mapping, f, maps x to f(x), texts which denote mappings shall discuss their outputs on the left and their inputs on their right. If f's inputs are the members of some collection, A, and its outputs are all in some collection Z, f will be synonymous with (Z: f(x) ←x :A), which relates f(x) to x yet maps x to f(x). I've now sorted out this tidy zone's use of ← rather than -> or →, but shall leave writings elsewhere alone except in so far as either I'm changing them for other reasons or I have copious free time.

Contents

… with illustrations of the most prominent denotations introduced:

thing is [{ a; an }] mode, thing [ isa mode …]

Templates and meta-denotations, styled words and punctuators, types and isa.

{i in n} = {i in j: n subsumes j}

Reading the text; enclosing sub-texts; quantifying over names.

this = that, r < t in T ⊂ S, f(x), f(a,…,z)

Expressions with assertions.

left ← right, {quick x: x in C}, &unite;, &intersect;, &on;

Relations, fixed points, sub-… and some combinators.

(A:f:B), (:f:B), (A:f:)

(:f|), (|f:), (|f:B), (A:f|)

(A|f:B), (A:f|B), (A|f|B), (|f|B), (A|f|)

End-relations and restrictions of relations, optionally with assertions.

[], [x], [h,i,j,k], [a,…,z]

Lists

Related:

x+y.z, a×b − c·d, e\f ± g/h

Arithmetic and its binary (and unary) operators

Types

For the purposes of giving meaning to templates, it is convenient to package some of the assertions I must make about context giving meaning to some texts, possibly a priori to my definitions. To this end, I'll use the following denotations:

mode is a type

Allow that context may give meaning to this is that as a synonym for this = that: mode is a type asserts that context gives some other meaning (which I'll generally presume to conform at least reasonably well to orthodox and colloquial notions of type) to statements of form thing is [{ a; an }] mode. (The choice between a and an is a cultural issue, not covered here, dependant on the natural language known as English.)

this isa that

Asserts that that is a type and denotes the statement of form this is [{ a; an }] that by which context gives that meaning as a type. In particular, this isa that emphatically does not assert this = that (though it does not preclude the possibility that this = that).

Note that, in the present context, type is a type (so type isa type and type = type); furthermore, the way I formalise use of any leads to: for any type t, any t isa t; in particular, any type is a type.

Primitive Parsing

Generally, I take it as given that the reader reads text according to the usual manner for text in the natural language I write (here, English). I augment the natural language by specifying meanings for various forms of text that would not otherwise be meaningful in it and I refine it by giving specialised meaning to some of its words.

See also my discussion of formalised natural language, of which this section is a reworking.

Words and symbols

When I introduce a specialised meaning for a word, that meaning supersedes any meaning that word normally has. I may specify, when defining it to take the specialised meaning, that it only does so for the purposes of the present formula, paragraph, section or page; otherwise, it tacitly takes that meaning throughout my writings. In so far as I am disciplined, other pages relying on such a specialised meaning shall link to the definition, at least when first they do so. When a definition binds such a specialised meaning to a word, to the extent that natural language derives other forms of the word for use in diverse contexts of the language's grammar, I tacitly extend the specialised meaning also to these derived forms.

For example, when defining a relation is less than on some kind of number, I tacitly use the same relation to give meaning to the least of several such numbers. In primitive discussions I may take the trouble to introduce is greater than separately (typically to something that shall prove to be the reverse of is less than); but, otherwise, I may tacitly use the reverse in this rôle. In a context with both defined, I'll use standard idioms such as at least, at most, more than, maxiumum, minimum; along with the parallel use of higher for greater and lower for less. Thus an upper bound on some numbers is a number which is greater than or equal to each of the given numbers; and a least upper bound is an upper bound which is less than or equal to every other upper bound. In this particular case, I should also note that I don't use bigger and smaller as simple synonyms for greater and less; instead, these compare the magnitudes or absolute values of things – all negative values are less than all positive ones, while a low positive value is small, as is its negation, and a high positive value is large, as is its negation; thus a big negative value is less than a small positive one, yet bigger than it.

As well as refining the meanings of existing words, I give meaning to texts that would not otherwise be meaningful, at least in the vernacular – although English (like many other languages) has now been in use for several centures by cultures in which at least a fairly basic level of mathematical education has been ubiquitous, with the result that there is at best a fuzzy boundary between refining existing meaning and giving meaning to texts that would otherwise have no meaning. Such texts use symbols and punctuators in specialised ways and commonly associate values, for the duration of the text, with words or texts having form loosely similar to that of words.

For the purposes of giving specialized meaning to one, a word is here just a text, each character of which is a word character, not immediately preceded or followed by word characters. The word characters are, for these purposes, the letters of the alphabet, the decimal digits and the hyphen character, -, as used in such compound words as mid-point. (Note that this is a quite different character from — the em-dash, the en-dash – or − the minus sign.) To illustrate all of the word-characters valid in English text, the text between quotes in abcdefghijklmnopqrstuvwxyz-0123456789 uses every word character. (Translations to another language might sensibly, however, use quite other characters as well as these or instead of them.) In particular, the space character which appears between words is not a word character, nor are the usual punctuation characters used normally in non-specialised English. Thus a sequence of letters between spaces is a word, for my purposes, even if there is no dictionary of English that recognises it as such and no opponent in a game of Scrabble® who would allow it into play it.

In contrast to words, a symbol is a single rendered (i.e. in visual media it is made visible, in audio it is voiced; it is not simply the gap between other things) character, other than the word characters, to which context has given meaning as such. Some of these are letters from other alphabets; while a Greek translation of my pages might use αλφα as a word, in English I shall not, but shall make use of individual letters of the (ancient) Greek alphabet as symbols. Other symbols are specialised symbols provided in Unicode (and related standards) to match common mathematical usage; for example, × may look somewhat like x or &on; may look somewhat like o but, in each case, the first is a symbol that looks somewhat like an alphabetic letter.

One of the common ways I give a word meaning is as a name by which to refer to some value; I use some symbols the same way, most obviously the letters from other alphabets. In particular, I follow orthodoxy in having π stand for the ratio of diameter to circumference of a circle. This last is an example of a meaning used everywhere (I doubt I ever use π to mean anything else), but other namings of values are commonly quite localised, typically to one instantiation of a template; see the next section.

Where symbols are used other than as names for values or relations (which some contexts might not regard as values), they are commonly used as binary operators or as the literal elements of templates. In any case, it is context's responsibility to establish their meanings; so responsible authors should link to something that explains those meanings when first they make use of a symbol.

Enclosing sub-texts

When reading a text, the reader is tacitly expected to decompose it into a hierarchy of sub-texts – paragraphs made up of sentences made up of words; derivations made up of equality assertions made up of expressions (to assert equal); proofs made up of assertions and inferences. The templates I define here serve to augment that hierarchy; they specify how, on recognising some parts of the text as matching the components of a template, arranged in the manner prescribed by the template, to read these components collectively as a use of the template. In making sense of a sub-text, the surrounding text contributes to its context; for example it may give meaning to some words and symbols, e.g. as names and operators. The reader conceptually replaces each sub-text with an atom of meaning that encapsulates the meaning of the sub-text; the enclosing text's meaning is arrived at by using this atom in place of the sub-text.

However, that can get complicated. We might have a sequence of ten tokens (words, symbols, etc.) in a text and find that the first seven of them match some template which gives them meaning, collectively, as a value; and that this, taken with the remaining three, matches another template that gives the whole meaning. So far, so good: but what if we also find that the last six tokens match some template, that gives them meaning as a value and that this, taken with the preceding four, matches a further template that gives the whole meaning ? Of course, if the two meanings of the whole coincide, all is well; but we have no guarantee that this shall always be the case. Such a text would be ambiguous: while I'm keen to be able to support ambiguity where it's intended, it's important to also enable authors to eliminate it where it isn't.

To this end, I define various enclosures of text (matching entirely orthodox rules of parsing); these are bounded by matched start and end delimiters and constrain the decomposition of text into sub-texts. The basic rule is that every sub-text that contains the start of an enclosure must contain the matching end enclosure, and vice versa. For that to be well-defined, I must specify what matching means, in this context. I'll describe a text as balanced precisely if: either it includes no use of { ( ; { ; [ ; ] ; } ; ) }; or it is of one of the following forms:

( text )

{ text }

[ text ]

[ text …]

with each text being balanced. I refer to the { ( ; { ; [ } in which a text of one of the first three types begins as opening an enclosure and the { ] ; } ; ) } in which it ends as closing that enclosure; I describe each as matching the other. Notice that text may include some opening and closing parentheses, braces or brackets, just so long as they appear in appropriately matched pairs; such enclosures are said to be nested within the primary enclosure of a particular match to one of these templates. Even when they use a character, at start or end, identical to the opening or closing of the template, the template's uses of the opening and closing match only each other, not any of those of nested enclosures.

For the purposes of my meta-denotations for templates, each literal text is treated as if it were balanced (so that { … } or [ … ] can enclose it and be balanced) even if (as actually exercised in the specification above) the literal in question is in fact one of the openings or closings. Each template as a whole shall use literal openings and closings in such ways that any text matching the template (as a whole) is indeed balanced. Every text denoted by a word in any template is constrained to be balanced.

I also use quotes and other standard features of the grammar of natural language (such as punctuation and phrasing) to delimit sub-texts; these operate just the same as a template's delimiting of its parts with literals, splitting the text into sub-texts. It is only necessary to use a formal enclosure, as just described, where such natural grammar would leave ambiguity – although it may, sometimes, be clearer to include some enclosures even when not needed.

Quantifying over names

Each use of a name in a formulaic text requires its context to give that name meaning, typically as a denotation for a value; by default, each denotational template propagates this requirement, from the sub-texts it combines, to whatever text is using the compound as a sub-text matched by the template. However, a denotational template may specify that each component sub-text it describes may quantify over or quantifies over names used in some of its components, in so far as context has not given them meaning.

For each use of each name, we can identify the smallest text around that use, in the hierarchy of sub-texts discussed above, for which that use appears within one of the may quantify components of the denotational template describing the given text (i.e. the first step back up the parse-tree at which the name can be quantified); call this sub-text a value-provider for that use of that name; if this is a sub-text of the value-provider for some other use of that name, call it a forwarding value-provider of that name; each use of each name then appears in a unique non-forwarding value-provider for that name; which quantifies over that name. Only {…} denotatons for collections, …←… denotations for relations and [for] {a;an;any;some} … texts do quantify over any names.

All quantification over names is, in any reading of the text, subject to assertions imposed by sub-texts exercising that name in the given reading. Note, however (e.g. in an expression sequence, below) that some constraints may be ignored. A text which quantifies over any names has meaning for each choice of meaning, for each such name, under which the text satisfies all constraints imposed by context and its sub-texts. The particular template which allows or imposes the quantification indicates how it combines the diverse meanings this gives it, typically collecting them together in some way.

Expressions with assertions

left [ { = ; ≡ } right …]

Equality

in which left and each right must be (texts denoting) values; this denotation asserts that all those values are equal; and denotes that value.

Note that context is presumed to be providing the notion of equality – it is entirely at liberty to be using some equivalence, Q, and writing modulo Q, x=y to express Q relates x to y: when all comparisons in some context are to be made in terms of Q, the whole text may provide equality is understood modulo Q and thereafter use x=y in place of Q relates x to y; this is particularly handy if Q is not expressed by a nice terse name but by some more convoluted text, such as one would sooner mention once than repeatedly. Although x=y may then be ambiguous, the ambiguity is invisible to Q – the values it can denote are all related to one another by Q – and, presumably, a context using such a convention doesn't care about differences invisible to Q.

Where context mediates equality via some such equivalence, it is sometimes necessary to indicate that some values are the same, even without that equivalence. The notion of sameness here shall ultimately relate to an equivalence implied by some broader context; this shall usually be equality as relations provided by my general formulation of mathematics; when it is anything else, I shall (endeavour to remember to) specify what. When such sameness needs to be denoted, I shall use ≡ in place of = to indicate the distinction. In a chain of equality assertions, if any of the links uses = then the chain, as a whole, denotes the value only modulo any relevant equivalence, such as Q above; but if all links use ≡ then the chain as a whole denotes its value only modulo the implicit equivalence from external context (i.e. it denotes the value more specifically).

value compare value [ compare value …]

Comparison

in which each value must be a (text denoting) a value; and each compare is a symbol or word (e.g. <, ∈, ⊂, in, subsumes or isa) to which context has given meaning as a relation to be denoted using this form; such a symbol or word is described as a comparator. A text of this form asserts that each compare relates the value on its left to the value on its right; it does not denote a value.

Note that some individual value may be a text of the preceding form, asserting the equality of some expressions and denoting their value; when this arises, one may equally read the text as using equality as a comparator; doing so should (provided context's comparators are all blind to differences ignored by the equivalence context uses as equality) make no difference to what the text asserts. We can thus regard equality as a comparator for these purposes; the main distinction is that, when a denotation of the present form only uses equality comparators, it has the preceding form and thus denotes a value, as well as making its assertions. This does lead to one other distinction: a text of the preceding form may appear as a value in a text of the present form, but not the other way round – unless parentheses enclose the expression of the present form and context gives meaning to assertions as truth values and gives meaning to assertions about the equality of such truth values.

relation ( [ early , …] last )

function invocation, generalised suitably.

Each early, if any, and last must be expressions denoting values; relation must be an expression denoting a relation.

If [ early, …] is omitted, this simply denotes an arbitrary value which relation relates to last and asserts that there are some such values (i.e. that last is a right value of relation).

Otherwise the text used in place of [ early, …] is of form first, …, late, – including the trailing comma – and our given relation([ early, …] last) stands for any value related to last by any relation denoted by relation(first, …, late) and asserts, as before, that there is some such value, i.e. that some such relation (exists and) does have last as a right value. Note that this specification is recursive.

Orthodoxy uses such denotations where there's only one such value – i.e. the denotation is unambiguous. For f(x), such uniqueness is exactly what f is a mapping guarantees us; and mappings describe their right values as inputs, left values as outputs, so the value to which a mapping f maps an input x is indeed the output f(x). Further, when f(x) is a mapping and accepts y as input, f(x,y) is the resulting output; which, if it is a mapping and accepts z as input, yields f(x,y,z) as output; and so on. However, I don't require uniqueness as a pre-requisite for using such denotations: nor does unambiguity of f(x,y) necessarily prevent f(x) from being ambiguous – provided there's only one value to which any value for f(x) does relate y. In particular, (: r(x) ←x :) = r shall be fatuously true for every relation, r – not just for the mappings.

[type] [ [ expression , …] expression { , | or | and } ] expression [ compare value ]

type-plural [ compare value ]

expression sequence

The second form is syntactic sugar; type-plural must be the plural noun (as provided by natural language) for values of some type; replace it with that type as type and a single expression comprising a name not used anywhere else; the second form is thus transformed into a special case of the first.

In the first form, each expression must be either the literal token … or an expression denoting a value. A use of … must either be preceded by or be followed by a value-denoting expression; it stands for further expressions whose form should be clear from context and the value-denoting expressions adjacent to the … (i.e. those immediately before and after it, in so far as there are any such); for example, where recent context has enumerated an expression sequence, a subsequent expression sequence may transform the first (few) and last (few) and replace the rest with … to save overtly stating what the same transformation does to the others; or an expression sequence whose entries are all of a common form, with some regular variation among them, may be expressed by a few of those values and a … indicating the rest, to be inferred by continuing the regular variation as often as may be (indicated by context or) appropriate.

Each expression denoting a value may quantify over any names used in it. In so far as an expression (either overtly given or implied by a use of …) takes a value or quantifies over any names: any constraints, implied by using the given expression in place of e in the following, are imposed. If supplied, type must be a type; its presence asserts e isa type for each expression e. If compare value is supplied; any text of form value compare value must match the comparison template above; and it asserts, for each expression, e, that e compare value.

If the final separator between expressions is and, the expression sequence introduces a context, in which all expressions are constrained to denote values. If the final separator is or, the expression sequence denotes any value which any given expression may take; and introduces a context in which the names used in that expression have the meanings that lead it to take this value. Otherwise, unless context indicates the former reading (e.g. by wording such as all of before the expression sequence sub-text, or by using the names introduced by the expression sequence in some manner that requires that they all be defined), the latter is implied. The context introduced may further constrain the names used in expressions, thereby further limiting the values the expressions may take.

In the or case, describe (for the purposes of this paragraph) any expression we are using (in a given reading of the text) as active; describe the others as inactive. In so far as the expression sequence gives meaning to some name, to which enclosing context does not, so as to cause an expression to denote a value, describe that name as bound by the given expression. The context, introduced by this expression sequence, ignores any constraint (that it would otherwise impose) which: involves any name only bound by inactive expressions; and involves no name bound by an active expression. (Thus any positive s, t or 1 with s+t = 1 may take the value 1 even when natural or integer is implicit in positive, causing s+t = 1, a constraint in the context introduced by the expression sequence, to be unsatisfiable. When 1 is the active entry in the expression list, provided its meaning is supplied by surrounding context, it binds no names. Thus s+t=1 involves no name bound by the active expression and involves names bound by the inactive expressions; so it is ignored.) The corresponding condition for the and case is fatuous, as all expressions are active.

Note that this may require care when writing constraints: any positive f(x,y), g(y,z) or h(z,x) with x<y<z can only exploit its h(z,x) in so far as there is a y strictly between x and z for which at least one of f(x,y) and g(y,z) is defined and positive; if f, its outputs and g accept integer inputs, this requires x+1 < z, which might not be what was intended; the result need not coincide with that of any positive f(u,v), g(u,v) or h(v,u) with u<v.

Relations

[[ constraint , …] constraint ; ] left ← right

left ← right [ ; constraint [ , constraint …]]

arrow formulae

in which left and right are expressions – which may involve names – and each constraint, if any, is a constraint. [In older texts I have used a , where the first template mandates ; to make reading easier … 2001/May/27. I am now exploring putting the constraint after the template … 2002/Jan/7.] The whole denotes a relation, which relates each value left may take to whatever value right may take, subject to all pertinent constraints. The composite may quantify over names for which any of its sub-texts (left, right and any constraint) require context to provide values.

Thus, for instance, f(x) ← g(x) denotes the result of composing f (which is f(x)←x) to the left of (i.e. after, when f and g are mappings) the reverse of g; the latter being x←g(x). Most usually, however, right will be a simple name; left will usually be some formula involving that name; though not uncommonly both will be simple names, with some constraint to specify the details. Almost invariably, ← denotations will be enclosed in (:…:) if in nothing else: for reasons which shall emerge below, this is fatuous, but the enclosure is often an aid to reading.

{ [ expressions [ : constraint [ , constraint …] ]] }

formulaic collection

in which (in so far as each is given): expressions must be an expression sequence, as above (in or form, generally implicitly, with optional type qualifiers and filtering) and each constraint must be a constraint. Each member of the collection is a value of expressions subject to any constraint. Note that everything inside the { } is optional, so that { } is a collection: there being no expressions, no value is a member of this collection, so { } denotes the empty collection. [I'll more usually write empty as {} without the space inside it; or call it by its name, empty.]

A formulaic collection implicitly quantifies over all ambiguity in the value of expressions. Note that use of expression sequences provides for an implicit union, i.e. {a, b: a in A, b in B} stands for the union of (the collections of fixed points of) A and B, even when B is empty – as noted when discussing expression sequences – requiring enough slack to ignore a constraint which doesn't involve a, even indirectly, while evaluating the expression a in the sequence.

relation &unite; relation

relates x to y precisely if either relation does.

relation &intersect; relation

relates x to y precisely if both relations do.

This and the previous, &unite;, denotation are binary operators. They correspond to mappings, intersect and unite respectively, which can be used to combine arbitrarily many relations rather than just the two combined here.

left &on; right

Composition (the &on; should be a bold (i.e. literal) &on; but I seem to lack the right fonts for the bold and plain forms to be distinct; readers who experience the same should read it as a literal element, all the same).

This relates x to z precisely if there is some value, y, for which left relates x to y and right relates y to z. Notice that y need not be unique. This combines the relations left and right to produce a new relation; as such, &on; is a binary operator.

When both left and right are mappings, this is the usual composition of mappings: formally, (f&on;g)(z) is f(g(z)); f relates this to g(z), which g relates to z. Note that I require the enclosure here used around f&on;g to distinguish this from f&on;g(z), which I intend to be read as synonymous with f&on;(g(z)), which relates f(g(z,y)) to y – i.e. g(z) maps y to g(z,y), which f then maps to f(g(z,y)) – whereas (f&on;g)(z,y) is f(g(z),y), the result of passing y to the function (f&on;g)(z).

Note that I am here using character entities which are not a standard part of the normal HTML repertoire: see above for the story behind that.

Restrictions

( [ left ] : [ relation ] : [ right ] )

in which left, right and relation, if present, are relations. A text matching this template denotes a relation. Let P = relation if present, else P is an arbitrary relation. If left is present, let L be its collection of right values; else let L be P's collection of left values. If right is present, let R be its collection of left values; else let R be P's collection of right values. The whole denotation then stands for L&on;P&on;reverse(R).

In particular, the denoted relation's left values are all right values of left and its right values are all left values of right; when these are collections, the result is simply to restrict relation by imposing these requirements on its left and right values. More generally, we can use these denotations, applied to the universal identity, to denote the sets of left and right valueas of a relation r as (:x←x:r) and (r:x←x:), respectively; I'll call those the end-collections of r.

When relation is absent (so that P is arbitrary) the whole denotation stands for an arbitrary relation between the right values of left and the left values of right, subject to any further constraints imposed by context. For example, {mapping (B::A)} means the same as {mapping f: f = (B:f:A)}.

From July 2004 to April 2012, I had restrictions also compose the restricted relation with end-relations from the restrictions; but I never found a good use for it, was in two minds about which end, if either, should use a reversed end-restriction and didn't like some of the complications implied, so reverted to the above, which is roughly what I had before.

End-relations

( | relation : [ right ] )

Let r = (: relation : [ right ] ). The denoted relation relates a to c precisely if {i: r relates a to i} subsumes {i: r relates c to i} and neither is empty. The final condition makes this a relation among the left values of r; I call it the left-relation of the given (: relation : [ right ] ).

( [ left ] : relation | )

Let r = ( [ left ] : relation :). The denotation relation relates a to c precisely if {i: r relates i to a} subsumes {i: r relates i to c} and neither is empty. The final condition makes this a relation among the right values of r; I call it the right-relation of the given ( [ left ] : relation :).

I'll extend these, below, to allow | in place of the : when left or right (as appropriate) is given; these variants shall add assertions relating relation to the restriction.

Collectively, I describe each of these as an end-relation. Because subsume is transitive and reflexive, so are end-relations. Consequently, intersecting one with its reverse necessarily yields an equivalence; I'll refer to these as end-equivalences, variously the left-equivalence and right-equivalence. When e is an end-relation, I'll refer to values as e-equivalent if e relates each to the other. Since an end-relation is reflexive, its values are fixed points, hence in the end-relation; thus, for given relation r, {right values of r} = {x in (:r|)} = (r:x←x:) and {left values of r} = {x in (|r:)} = (:x←x:r).

Prior to 2004/June, I defined these two denotational forms to denote the end-equivalences, rather than end-relations themselves (and a whole lot earlier than that, I used the same forms to denote the end-collections); and defined the conformance notion below in terms of those – there may yet be ghosts of that in texts here. I also transiently had the right-end relation defined reversed during July 2004 – hopefully I've fixed that, though.

Restrictions and end-relations with assertions

I now introduce variations on the restriction denotations above in which a : between two relations may be replaced with a | to assert (without changing the relation denoted) a relationship between the end-relations facing one another across the |. The asserted relationship is expressed, for transitive reflexive relations e and c, as e conforms to c iff (e:c|) subsumes c and e subsumes (e:c:e). Note that neither e nor c necessarily subsumes the other, all the same. Crucially, any reflexive transitive c conforms to itself and to {x in c}; and any collection, e, conforms to c if (e:c|) subsumes c.

( [ left ] : [ relation ] | right )

( left | [ relation ] : [ right ] )

( left | [ relation ] | right )

All three denote the same relation as ([left]:[relation]:[right]), but each adds assertions wherever that uses a : in place of a | in this template.

In the first form, the assertion is that ([left]: [relation] |) conforms to (|right:); in the second form, the assertion is that (| [relation] :[right]) conforms to (:left|); the final form makes both of the given assertions. Likewise …

( left | relation | )

Denotes (left:relation|) and asserts that (|relation:) conforms to (:left|).

( | relation | right )

Denotes (|relation:right) and asserts that (:relation|) conforms to (|right:).

Note that no provision is made for denotations of form (|r|) with an unconstrained | at each end.

Examples:

• The conventional idiom of mappings from U to V when U and V are collections says that the mapping must accept all members of U, while all its outputs must lie in V; which is tersely expressed by f = (V:f|U), given that U and V are collections, and the collection of such mappings is simply {mapping (V:|U)}.
• Finiteness, at least for a collection N, can be expressed by the equation {mapping (N|:N)} = {monic (N:|N)}, known as the pigeon-hole principle. A mapping (N|:N) is given to have only members of N as inputs (right values), and to have all members of N as outputs (left values). When N is finite such a mapping, with only one output per input, can only yield enough outputs if it in fact accepts all members of N as inputs and doesn't map any two to the same output; which is just to say that it is a monic (N:|N). Note that, in general, the reverse of a monic (N:|N) is a mapping (N|:N).

Lists (and sequences)

With my apologies for any confusion between [ meta-denotation …] and [ literal … ] square brackets and ellipsis. (Note that the latter leaves a space between … and ], while the former does not.) The difference does matter – see above under meta-denotations and templates. Note that the presence of commas in these denotations distinguishes them from further uses of square brackets which may arise in the tensor notation and elsewhere.

[ [ item [ , item …] ] ]

[ [ item , …] [ … , item , [ item , …] …] … [ , item …] ]

in which each item must denote a value; the whole denotes a mapping (:h|N), for which N is either {naturals} or a natural, and the items are h's outputs. When N is 1+n for some natural n, (:h|1+n) is synonymous with [h(0), …, h(n)], just as 1+n is synonymous with {0,…,n} and, indeed, with [0,…,n].

A text matching either template is a sequence of sub-texts, separated by commas and enclosed in [ square brackets ], in which each sub-text either is an ellipsis, as … is known, or is intelligible to context as a denotation for a value; if none of the sub-texts is … the denotation is of the first form, otherwise the second. Where a sequence of value-denotations, i.e. of items, uninterrupted by … appears in a denotation of either form, describe it for the present as a chunk; the first form, when it contains any items at all, has a single chunk; the second form may contain arbitrarily many chunks. Taking any chunk and enclosing it in [ square brackets ] yields a text matching the first template; so, first, I'll give the meanings for these, then I'll use these to express what the second form means.

Each chunk has a definite number of items in it, and no ellipsis; a list in the first form, having N items in its text, is that mapping (:h|N) for which the value of each item in the text is h's output when given, as input, the number of items to the left of the given one. Thus [a,b,c] is the mapping (:|3) which maps 0 to a, 1 to b and 2 to c; and [] is the mapping (:|0), there being only one such since 0 is empty = {} and a mapping (:|{}) has no right values, hence is empty, so indeed [] = {}.

Given this reading of the first form, any chunk is best described by the list one obtains by enclosing it in [ square brackets ]. In a use of the second template, denoting (:h|N), the presence of a chunk described by a list (:g|n) asserts that

• there is some m in N for which g = (: h(m+i) ←i :n) whence, in particular,
• N is at least n+m which is at least n
• if the chunk appears before the leftmost use of …, the denotation asserts that m is 0; if after the rightmost use of … that n+m is N; i.e. a chunk which starts or ends the denotation tells you the first or last few values in the list denoted, as you might expect. In particular, a chunk after the last ellipsis says that N is n+m for some naturals n, m – hence that N is a natural, not {naturals} itself.

Note that, aside from chunks which abut a [ square bracket ], nothing is asserted about the relative order of chunks – the lists [0, 1, 2, 3, 4, 5] and [1, 2, 3, 4] are both valid values for the denotation […, 2, 3, 4, … 1, 2, 3, …], for instance; as, indeed, is {naturals}.

A denotation of the second form may end in ellipsis, in which case the value it denotes may be an infinite sequence, (:h|{naturals}). One could probably do quite well extending the given notation to describing ordinal sequences; then n would be an integer while m might not (though it'll still be an ordinal); ending in ellipsis would then allow (but not constrain) N to be a limit ordinal.

Borrowing an idiom from ECMAScript, I could allow list-like denotations in which two commas appear with no value between them; this would naturally denote a mapping (:h:N) as above, but allowing some members of N to not be right values of h. However, for now (up to 2012/Spring), I haven't feld a strong need to do this.

Written by Eddy.