Expressions with assertions

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.

value compare value [ compare value …]

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.

left [ { = ; } right …]

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.

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

early if first else [ later if next else …] last
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.

Valid CSSValid HTML 4.01 Written by Eddy.