This
corner of the web contains a collections of miscellaneous thoughts and
ponderings by yours truly.
You can also find some of my early KRML notes at
mathmeth.com.
This
corner of the web contains a collections of miscellaneous thoughts and
ponderings by yours truly.
You can also find some of my early KRML notes at
mathmeth.com.
Any technical writer who uses formulas or variables ought to consider the issues brought up in this short article. [PDF] K. Rustan M. Leino. Real estate of names. Information Processing Letters, 77(2-4):169-171, February 2001.
Many operators in programming languages have standard representations, like + and <. Logical implication (Þ), however, is an operator that different programming/specification languages have chosen to represent in different ways, particularly when the language uses ASCII characters. I wish to make a recommendation to such language designers: choose ==> over =>. Here's why:
If you think of the boolean type as an enumeration consisting of the values false and true, then many languages would let you compare these values with the ordering =. In ASCII, you would then write false <= true. Similarly, if you think of the booleans as forming a lattice, then common choice is to make false be the bottom element and true the top element, so then, too, does false <= true make sense. The ordering in the lattice in fact the implication ordering, so = is the same as Þ. In typeset mathematics, one is used to this, but in ASCII, it would be confusing that both false <= true and false => true would hold. So don't choose => as your implication symbol; choose something else, like ==>.
Also, if you have implication, chances are you would also want reverse implication, Ü ("follows from", or as Jan van de Snepscheut jokingly used to say, "explies"). If you had chosen => for implies, the natural choice for explies would then be <=. But this would be disastrous, because then you'd have both false <= true and true => false! So, don't choose => as your implication symbol; instead, consider ==> for implies and <== for explies.
Finally, although binding powers of operators are not always chosen the same way by different people, I like giving conjunction and disjunction higher binding power than implication. To make the visual appearance of expressions suggestive of the binding powers, you want to make lower-precedence operators occupy more horizontal space. A simple way to achieve that is to make operators longer. Using 3 characters for implication instead of 2 thus achieves this effect: your eyes would naturally read A && B ==> C && D as (A && B) ==> (C && D), not A && (B ==> C) && D. So, don't choose => as your implication operator, choose ==>.
If you have written papers that include variable declarations, you might have noticed that the type setting of "x : T" in TeX and LaTeX puts a lot of space on both sides of the colon. If so, you probably want to use "\colon" instead of ":". The idea behind "\colon" is to give an appropriate amount of space in exactly this situation. So write "x \colon T". Similarly, "\to" is defined to give the symbol and spacing to write function types, as in "f \colon A \to B".
If you're like me, you might also want some more space between such variable declarations. Unless I'm cramped for space, I write "x \colon T,~ y \colon U".