]> Plaintext Denotations - Commentary

# Plaintext Denotations – Commentary

For a good over-view of the state of the art in putting mathematics on the web (in orthodox notation), see Jukka Korpela's page on the subject (my last visit: 2013/October).

## The Unavoidable Reversal

I'm going to take to heart the order of terms in g&on;f maps x to g(f(x)). Either g or f may be replaced by any text which denotes a mapping. Such texts have a natural split into things said about the inputs, things said about the outputs and things said about how the former are mapped to the latter; the beginning, the end and the middle. When we come to substitute texts for f and g, the result will read more clearly if the leftward end of f's text and the rightward end of g's texts are discussing the values which mediate &on; in g&on;f, namely f's outputs, in so far as they are g's inputs. This makes the leftward end of a mapping's text discuss the outputs, while the rightward end discusses the inputs. Then (W:g:V)&on;(V:f:U) = (W:g&on;f:U) will read more amicably than would (V:g:W)&on;(U:f:V) = (U:g&on;f:W), especially when the chains of composition get long.

There is an unavoidable conflict in order involved when g(f(x,y)) passes first x, then y to f, passing on the result to g; x was followed by y, but f was followed by g; one half reads left-to-right, the other right-to-left, because each, in effect, reads away from positions between a mapping and its first input. Having f(x,y) mean (f(x))(y) is so much more intuitive than having it mean (f(y))(x), just as (g&on;f)(x) means g(f(x)) rather than f(g(x)). So I can have either order of input or order of composition read left to right (like my English text), but the other has to read right to left (like Arabic). For the sake of g&on;f maps x to g(f(x)), I've chosen to endure right-to-left as the internal structure of texts denoting mappings, with left-to-right then arising as the convenient order for supply of inputs.

A mapping, f, from members of A to members of M must thus end up denotable as (M? f(a) % a !A) for some enclosure (…) and punctuators ?, % and ! so as to put the input truths, a in A, on the right and the output truths, f(a) in M, on the left, while separating the several sub-texts which may be substituted in place of M, f(a), a and A. This will mean that, at least when f's outputs are mappings f(a) = (Z? f(a,n) % n !N), f is denotable as (M? (Z? f(a,n) % n !N) % a !A) in which f(a,n) mentions a and n in the reverse of the order in which they subsequently appear. I can (and shall) chose different punctuators, but I can't avoid a reversal somewhere.

Now, all that applies to mappings, which are a particular flavour of relation; so I want denotations for mappings to be special cases of denotations for relations. The need for reversal arises, for mappings, out of the f maps x to f(x) form of denotation, only pertinent where we use the f(x) mode of denotation, which is only familiar in so far as it connects to mappings. None the less, I'll have relations of form (M? m % a !A) and it would be nice to be able to read this as a relation which relates m (in M) to a (in A). To do so will read a mapping, f, as relating f(x) to x, in the reverse order to that used when describing it in the language of mappings, where it maps x to f(x); this will make the verbs map and relate describe a given thing differently, but does not disturb the sense of what is happening.

## Ambiguity

I intend to counteract ambiguity with a systematic integration of equivalences into the restriction/end-relation denotations; a context doesn't care about ambiguity in so far as all the values a given denotation may stand for are equivalent, for that context's purposes. If a relation r = (B:r:A), with A and B equivalences, the appropriate replacement notion for mapping [recap.: (B:r:A) is a mapping if it maps each a in A to precisely one r(a) in B; so r relates a unique r(a) in B to each right value, a, of r] becomes; if r relates d to c and b to a, A relates a to c implies B relates b to d; the appropriate replacement for monic says the converse. So, to be a mapping from A to B, (B:r:A) must respect equivalence: (:B|)-equivalent values will only ever be related to (|A:)-equivalent values; if (:B|) can distinguish two of r's left values, (|A:) can distinguish the corresponding right values. To be monic from A to B, (B:r:A) must respect distinctness: if (|A:) can distinguish two right values, (:B|) can distinguish their corresponding left values; to (:B|)-equivalent values, (B:r:A) only ever relates (|A:)-equivalent values.

Indeed, one may construct collections of relevant equivalence classes, AA = {{x: A relates x to a}: a in (|A:)} and BB = {{y: B relates b to y}: b in (:B|)}, and construe r as monic or a mapping AA to BB if it's iso-monic or an iso-mapping, as appropriate. However, reducing to equivalence-classes induces artifacts into the discussion which I suspect the iso-map/iso-monic notions may help to assuage.

## Equality

Template: left [ = right …]

Note that the template allows there to be no right texts, just the left text; in which case the definition says it means exactly the same as the given text, as one would hope, given that it can't be distinguished from that text.

There is a choice to be made when left = right is used with potentially ambiguous texts: clearly the denotation is then ambiguous, standing for any value for which there is a disambiguation of the two texts yielding that value for each text. The choice is: should the assertion be that every disambiguation produces such agreement, only that some must, or that for each on either side, there's agreement with at least one on the other side ?

## Composition and Evaluation

Notice the difference between:

• (f&on;(g(x)))(y) = f((g(x))(y)) = f(g(x,y)) and
• ((f&on;g)(x))(y) = (f(g(x)))(y) = f(g(x),y) = (f&on;g)(x,y)

and consider what f&on;g(x) should mean; clearly f&on;(g(x)) and (f&on;g)(x) = f(g(x)) are the two possible candidates; except in odd circumstances, they mean different things. Analogously, in f(w)&on;g(x) there is clearly no need to enclose (f(w)), making it natural to read f(w)&on;g(x) as the result of composing f(w) to the left of g(x), i.e. f(w)&on;g(x) wants to be read as (f(w))&on;(g(x)) (and all the more so when we look at f(w)&on;g(x)&on;h(y)&on;…). Given this, it makes sense equally to read f&on;g(x) as f&on;(g(x)) - after all, the alternative, (f&on;g)(x), already has the handy synonym f(g(x)). So I'll have evaluation bind more tightly than composition, to use the terminology of computer language designers.

## Restrictions and End-equivalences

It is possible to unify all the various denotations in these sections; I'm not convinced it's any clearer, but I like it anyway.

( [left] { : ; | } [relation] { : ; | } [right] )

in which left, right and relation, if present, are relations. In explaining what this means, I'll describe the left use of {:;|} as the left punctuator and refer to left (or its absence) as this punctuator's constraint; likewise, right is the constraint of the right punctuator. If both punctuators are |, at most one of left and right may be omitted.

Where a punctuator is | and its constraint is present, the denotation stands for the same value as it would if this | were replaced with a :, but makes an additional assertion (to which I'll return). If a punctuator is | and its constraint is absent, in which case either the other constraint is present or the other punctuator is : (or both), the denotation stands for a relation among relation's values on the side of the unconstrained |. Otherwise, the denotation stands for a restriction of the relation.

If both punctuators are :, the denotation makes no assertions: it just stands for the relation which relates x to y precisely if

• left is absent or relates some value to x
• relation is absent or relates x to y
• right is absent or relates y to some value

(If any of left, relation and right is present but not a relation, this implies that the denotation stands for the empty relation, since no x, y meet these requirements.) Note, in particular, that (::) is a valid use of this template; absent any constraints, it stands for the all-relation, which relates any x to any y unconditionally. For a given relation, r, its collection of left values may be written as (:x←x:r), its collection of right values as (r:x←x:).

When one punctuator is | and its constraint is absent; for the relation obtained by making both punctuators : write r; then

( |[relation]:[right])
stands for (: {y: r relates x to y} subsumes {y: r relates z to y}; x←z :r), with r = (:[relation]:[right]
([left]:[relation]|)
stands for (r: {y: r relates y to z} subsumes {y: r relates y to x}; x←z :), with r = ([left]:[relation]:)

These are relations among, respectively, the left and right values of r; intersecting each with its reverse yields an equivalence which says r doesn't distinguish the relevant values - it relates them (if left) to the same values or (if right) relates the same values to them.

Where a punctuator is | and has a constraint, the assertion it makes concerns the two equivalences on either side of it. One is a constraint, call it s; eliding s from the original denotation will leave the denotation for an end-relation of the rest of the original; if it's the left-relation, call it e, otherwise call its reverse e. Put a | on the same side of s as it appeared in the original, a : the other side, wrap in (); if that's s's left-equivalence, call the result c, otherwise call its reverse c (because it's the constraint). The assertion says that e conforms with c - which roughly says that: e's values include at least one member of each equivalence class of c, and; e respects the equivalence c, in the sense that if c deems two of e's values equivalent, so does e. Thus

(A|r:B)
asserts that e = (|r:B) conforms with c = reverse(:A|)

i.e. (e:c|) subsumes c and e subsumes (e:c:e).

(A:r|B)
asserts that reverse(A:r|) conforms with (|B:)
(A|r|B)
makes both of these assertions

and all three stand for (A:r:B), which relates x to y iff x in (:A|), y in (|B:) and r relates x to y.

The notion conforms with, used to define assertions in the above, is designed to ensure that composing the two relations separated by the | will have some helpful properties. Specifically, (:f|g) ensures that f&on;g has all the same right values as g; while (f|g:) ensures that f&on;g has all the same left values as f. In a similar vein, it makes sense to consider (B:r:A) as a map from A to B when (:B|) subsumes (|r|A); and as monic from A to B iff (|A:) subsumes (B|r|).  Written by Eddy.