Sometimes formally correct statements are rather hard to read: rigour
sometimes comes at the cost of clarity. In such cases, I may include
a Slogan
that caricatures the statement in terms that I hope shall be
easier to comprehend (and hence remember), albeit this statement may not be
rigorously correct. In particular, where expressions may be ambiguous
(e.g. r(x) when r is a relation, see below), slogans may
use equality to indicate that there is at least one value that each of the
equated expressions may take in common; typically, the more rigorous statement
shall have one expression's collection of possible values subsume that of the
other, or some similar result that does collapse down to actual equality when
the expressions are unambiguous. In the language of standards, my slogans
are not normative
; they may be true in some (typically unambiguous)
cases, but are not in general rigorously correct. I include slogans in the hope
that they shall aid the reader in making sense of more rigorous texts.
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, despite the similarity of form, comparison works differently than binary operators; it makes assertions rather than denoting a value; and reads differently when more than two values appear.
in which left and
each right must be (texts denoting) values;
asserts that all those values are equal; and denotes that value. However, a
text is only read as matching this template if it would have been read, in its
context, as a comparison (not denoting a value),
were { =
; ≡ } a comparator. (This admitedly
oddly-phrased constraint causes equality
to bind less tightly than
all binary
operators.)
Where (for a specific choice of how to bind each name or
symbol used in them to a specific one of the meanings context permits it to
take) the expressions – left and
each right – are potentially ambiguous,
equality shall be understood as meaning that each value each expression can take
is a value each of the other expressions can take; i.e. the expressions have the
same ambiguity as one another. (Exception: in slogans, I may use equality to
indicate that the expressions have at least one value in common,
as discussed above.) I shall at times express this sense
of equality by saying the expressions agree
with one
another, typically when I want to emphasise that this holds even though the
expressions may be ambiguous.
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).
Note that an equation may appear as
a value in a comparison; when this arises, one
may equally read the text as if equality were 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
comparison asserts. We can thus regard equality (in either of the two forms
here) as a comparator for these purposes; the main distinction is that, when
the only comparators
used are equality tests, it has this more
specialised form and thus denotes a value, as well as making its
assertions. This does lead to one other distinction: a text of this form may
appear as a value in a text of the preceding
form, but not the other way round – unless parentheses enclose the
expression of the previous form and context gives meaning to assertions
as truth values
and gives meaning to assertions about the equality of
such truth values. An equation can likewise appear as a value in a text using
a binary operator, although it should be enclosed in
parentheses if so used, to avoid ambiguity.
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.
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 be either preceded by or
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 does involve names bound by
an inactive expression; 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 or reading
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, or what first comes to mind on reading it; the result need
not coincide with that of any positive f(u,v), g(u,v) or h(v,u) with
u<v
.
conditional value expression(a right-associative ternary operator, borrowed from python)
The literals if
and else serve as
enclosures, with if as opening
and else as closing. The text between a use
of if and its matching use
of else may thus exercise this template, subject to
the usual rules for nested enclosures. Each of the sub-expressions between a
use of if and its matching use
of else (i.e. first
and, when present, each next) must have the form
of an assertion; the other sub-expressions, outside
the if-else enclosures
(i.e. early, last
and, when present, each later), must have the form
of expressions denoting values. The greedy matching
of
the optional repeated element precludes
interpreting n if c else m if d else k
as (n if c else m) if d else
k
– which would give k when d is false, even if c is true – in
the absence of the parentheses in the latter.
If the first assertion is true, the whole use of this template stands for the value that early denotes. Otherwise, either the portion of the text following the first else is itself a match to this template, in which case it is evaluated in the same way, or it consists only of a final value expression, in which case the text matching this template stands for the value of that final value expression, last.
This process evaluates assertions until one is true, selecting the value expression preceding its use of if, or all assertions are found to be false, in which case the value expression after the final else is selected. The use of this template then stands for the selected value expression. Only the meanings of the selected value expression and the assertions that must be checked to determine that it is selected are relevant to the meaning of this expression. Provided each later text between an if and its matching else has the form of an assertion (so as to make it possible to parse the use of this template), it does not matter whether these later assertions can actually be given meaning, much less whether they are true. Likewise, provided the non-selected value texts have the required form, no assertions implicit in them are taken into account, nor are any names introduced and quantified over in them taken into account.
A use of this template is valid precisely when an initial sequence of its
assertions is valid, either this sequence is all of its assertions or the last
in it is a true assertion, and the value text thus selected is valid. When an
assertion introduces a name and the assertion is true, the name is retained in
the thus-selected value expression's context – e.g., given f, g and x from
context, g(t) if x = f(t) for some t else 0
introducing t in the
assertion and using it in the expression it selects. (If I ever find an example
where it may be relevant, I shall allow such name bindings in false assertions
to also remain part of the context of later assertions and of the
finally-selected value expression. However, I can think of no sane example for
now.) For example, the Collatz iteration can be written as (n if m = 2.n for
some natural n else 3.m + 1) ←m.
Written by Eddy.