Meta-denotations: the language of templates

Each of my definitions of denotations comprises a template and accompanying explanative text. The template specifies a way of combining texts, some given verbatim, others indicated by tokens to which the explanative text refers, stating any constraints on the fragments which may be used in place of those tokens and specifying the meaning of the composite in terms of the meanings of the components. [I try to design templates that someone writing a parser would find useful.] Aside from any ambiguity the definition explicitly introduces or resolves, any ambiguity in the fragments combined (potentially) propagates to the composite: it means each of the meanings it could be given by replacing each ambiguous fragment with any of the meanings it could have consistently with the definition's constraints and any imposed (typically via the values, and relationships among the values, that particular names used in fragments may be understood to denote) by context.

In templates, and where explanative text refers back to a fragment using the following, I'll use text style to distinguish the rôle of sub-texts. Words & punctuators, in this style, (hopefully bold if I got my CSS right) are text to be included verbatim in any use of a template – folk (and programs) reading the text need to be able to recognise the denotation by the appearance of these verbatim fragments. Everything else in a template will be in this style (hopefully italic and dark green) and will describe the sub-texts that must appear in conjuction with the verbatim fragments:

Note that one is not expected to use these styles in texts which use the template: they serve in the template to say how to read texts of the givenform without this formatting. At least one browser I've used fails to display (plain) | distinct from (bold) |, others may have similar problems – sorry about that, but you can always read the source (the mark-up is only as fiddle-some as the meaning requires) if you can't work it out from what you browser does display.

The styling is important; a given sequence of words shall mean quite different things if differently styled. For example value is a type is one specific text (that happens to be true; see below) while value is a type uses the words value and type as tokens representing sub-texts in a template; each may be replaced by some arbitrary text satisfying whatever conditions the template's specification imposes; and that specification shall give meaning to the literal is a where used in accord with the template.

The diverse ways of being

The verb to be carries many meanings, some of which I aim to exercise somewhat carefully. It can be used to indicate equality – when x is 7, for example. It can also be used to assert existence of something – if there is a solution – or to assert that a thing has some property (or some properties) – the sentence is short or each pig is an animal.

A text asserting, or conditioning something on, the existence of some expression may use, as that expression, a denotation that instantiates templates that assert various conditions; in such a case, the conditions asserted by the templates are expressed by the given text's existence claim. Thus when there is an x −y is a way of conditioning on whether x and y meet the conditions imposed by the template that gives meaning to as a binary operator; this condition, as it happens, is that there is some z for which x = z +y.

Various properties that a thing may possess are commonly expressed by defining a word to package the assertion that some thing possesses the given property or some assemblage of properties. Thus any relation satisfying a certain condition is described as a mapping and said to map its inputs to its outputs; and mappings that satisfy certain conditions are described as linear.

mode is a type

this asserts that context gives some meaning – distinct from thing = mode and from any assertion of the existence of either mode or thing – to statements of form thing is [{ a; an }] mode; and that the given meaning is some form of condition on or statement about thing. (The choice between a and an, or whether to use either, 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 as well). The purpose of this template is precisely to be a way to make the type-claim without possibility of misreading as an equality.

In the present context, the first of these definitions does indeed give meaning to statements of form thing is [{ a; an }] mode, opting for is in the is [{ a; an }] choice and using the word type as mode; consequently, 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.


The templates defined here formalise particular uses of natural language; each is close to how the vernacular (to the extent that it uses the words involved at all) uses the words involved; consequently, it is often simpler to just read texts matching these templates as natural language in the usual way, rather than formally interpreting them via the templates given here. None the less, I do strive to use these natural language idioms in a consistent manner, that matches the templates and explanations given here; the following makes explicit what is likely obvious to anyone familiar with the language.

[{unary ; binary}] operator

A type. A function or other way of combining or transforming values can be described as an operator; in such a case it may be denoted in the usual manner for a function, but shall usually be denoted by a symbol used, in some manner specified by a template, in conjunction with the values to be combined. In the latter case, it is usual for the value denoted by a text instantiating the template to be kindred to the values being combined – e.g. of the same type, or of some related type – and amenable to further use of the same operator; more generally, a family of types and operators may be knitted together such that each of the values any of the operators may yield is at least amenable to being combined, by some operator in the family, with some values of types in the family.

In the template case, if the template uses precisely one value and one instance of the operator symbol, the operator is described as unary; if the template uses one more value than instances of the operator symbol it is described as binary; and the theory of binary operators is fairly extensive. An operator combining three values may be described as ternary; and kindred classically-derived adjectives, or simply n-ary (with n as the relevant number of values), may be used for larger numbers of values; however, I'm not inclined to use these (c.f. my preference for currying functions). It is entirely possible for a given symbol to be used both as a binary operator and as a unary operator, provided the templates have sufficiently different form that no ambiguity arises; this is usually apt when the two operators are closely related, as for example the usual use of for both subtraction and negation.

In the function case, there is usually some number of inputs (all of kindred type) to the function, after which the yield of the function is of the same type as the inputs, though there may be a family of functions and types in similar manner to the templated case; the operator shall then be construed as combining this number of values and described as unary if the number is one or binary if it is two.

[{ left ; right }] operand [ of operator ]

A textual reference, construable as a type. A text matching this template refers to a value in some context where an operator is used on the referenced value. If the operator is unary, this is the one value on which it acts; otherwise, it is one of the values combined (with another or with others) by the operator. If specified, operator must be either (a text denoting) some operator (which may be a function) or a text identifying a particular use, or some particular uses, of some operator in some text being referred to. (Here, some operator usually means an operator but the text may refer to several operators.) Otherwise, there must be some operator to which context is tacitly referring. Each value acted on (transformed or combined with others) by the operator (or by any of the operators, if several are referenced) is an operand. For a binary operator, in each text using the operator to combine two values, one of these values appears to the left of the other; this is called the left operand, and the other (on its right) is called the right operand, of the operator. (Note that the operator need not appear between them, so they need not necessarily be to its left and right, respectively – although this is the usual case.) In the case of a ternary operator, it would likewise be reasonable to refer to the left-most and right-most of the operands in like manner; and to the one in between as the middle operand.

Some programming languages construe =, ≡ and the comparisons (<, ∈, ⊂, etc.) as binary operators: however, in my specifications, they don't combine values so much as make assertions about relations among values, so I characterise these as comparators as distinct from operators. In these terms, (from above) isa isa comparator, not a binary operator. In particular, operators get to transform or combine values before comparators get to compare the results.

Valid CSSValid HTML 4.01 Written by Eddy.