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 – readers of 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 green) and will describe the sub-texts that must appear in conjuction with the verbatim fragments:
greedy matchingof repeated elements.
{this ; that }means
either this or that. I shalln't use the empty verbatim text; if I did, {any; stuff; } would mean the same as [{any; stuff}] – I find the latter makes it clearer that the whole is optional.
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
given form 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.
Likewise, when I define denotations using
verbatim [ ] to
enclose other texts, I rely on the styling to make clear that these are brackets
that shall appear in texts that exercise the template, rather than
brackets that delimit an optional part of the template.
Spacing in templates separates tokens to make clear that they are distinct for purposes of interpreting the template (and determining what texts match it and how to interpret them); however, texts to be interpreted in terms of a template need not include such spacing except where the usual conventions of text requires it. Thus words used as tokens in a text that matches the template typically need to be separated by spacing characters (and denotations that make exceptions from this shall do so explicitly) but enclosures and other punctuators matching verbatim texts of the template need not be separated by spacing from one another or adjacent words, althoug the author of a text may chose to do so, for example to make the text easier to read.
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
.
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.)
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.
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
(cf. my preference for currying functions), save
for one ternary operator. 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 output 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.
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.
Written by Eddy.