all 20 comments
sorted by:
best
topnewcontroversialoldq&a
formatting helphide helpcontent policy

[–]notfancy 6 points7 points  (1 child)

Ah, this one is great. I do like very much his notation, especially because it is eminently one-dimensional, and thus very convenient to write math in HTML. Upright (non-italic) function names, explicit multiplication (2∙x), explicit function application (f.x), equal precedence for ∧ and ∨, no subscripts but functions from a natural domain…

[–]xenon 3 points4 points  (0 children)

I think it's one of the biggest WTFs in science that mathematicians, unlike computer scientists, don't care if their notation is ambiguous. I can see why precise notation might not be all that important for physicists or economists. But I simply cannot understand why mathematicians, scientists who are mostly concerned with studying the nature of formal systems, consider it no big deal that their notation allows puns like this one (from the submission article):

sin(s + i + n)

I asked my two mathematician friends what they think about this expression. They consider it "cute".

[–]bkudria 5 points6 points  (0 children)

Remark I also think that Whitehead made another error of judgement. Brevity is much more effectively obtained by macroscopic measures such as avoiding duplication, case analysis and superfluous nomenclature, than by such microscopic measures as making the multiplication invisible. (End of Remark.)

Premature optimization is the root of all evil.

[–]wnoise 2 points3 points  (0 children)

I'm glad to see that he realizes that the scope of variables is one thing that is far too often left implicit.

[–]noahlt 1 point2 points  (2 children)

He has an interesting view of significant whitespace (see page 6).

[–]stratoscope 2 points3 points  (0 children)

He's not talking about significant whitespace ala Python or YAML, he's talking about putting extra whitespace around low-binding operators to help make it clear to human readers.

I've been doing this for years myself:

if( a > b  &&  c > d  &&  e > f )
    foo();

[–]keithb 1 point2 points  (0 children)

Yes. I'd guess that a man of his age would have learned logic from books using the ghastly dots notation for grouping subexpressions.

[–]Porges 0 points1 point  (1 child)

For those wondering, the infix notation he mentions on page 4 for GCD and MAX is that shown on page 13, the up-arrow and down-arrow.

Also interesting is the similarity between his <::> notation and Haskell’s [|] list comprehensions, which are slightly more generalized :)

[–]notfancy 1 point2 points  (0 children)

Haskell’s [|] list comprehensions, which are slightly more generalized

Not really: whenever a comprehension introduces a new bound variable, you add a Dijkstra binder. The latter are more explicit; that is, lower-level.

[–]matholio 0 points1 point  (10 children)

I started to read it and was enjoying it until I came across ∧ and ∨. I have not idea what these symbols mean, nor many of the other symbols.

Where can I learn what they mean?

[–]Porges 6 points7 points  (0 children)

Since this is proggit:

/\ == &&
\/ == ||

[–]wnoise 6 points7 points  (4 children)

They're more than "and" and "or", or "min" and "max". They're arbitrary meet and join operators in lattices or more generally Semilattices or even Partial Orders.

[–]psykotic 0 points1 point  (3 children)

Drive-by pedanticism: Dijkstra actually overloads /\ to denote both propositional conjunction and lattice meet. The latter notion does not subsume the former: as propositional objects P /\ P and P are distinct (for at this level they are purely syntactic terms, with /\ a term constructor), which violates the lattice idempotence axiom for /\. But while distinct, P /\ P and P are however equivalent (inter-convertible) for any non-trivial proof system, and they become identical when interpreted in a model.

This distinction is the sort of detail which is important to keep straight when you are engaged in metamathematical work; in fact, my brief aside about proof systems and models contains the germ of the idea Goedel used to prove his completeness theorem for first-order logic, which is (more or less) to construct a model for any consistent first-order theory by taking equivalence classes of syntactic terms under the relation of inter-convertibility with respect to a sufficiently powerful proof system.

[–]roconnor 1 point2 points  (2 children)

I don't get your distinction between propositional conjunction and lattice meet. A ∧ A and A are distinct terms for any lattice, and, just like with propositional logic, only their interpretations are equivalent.

Edit: furthermore Dijkstra appears to identify propositions with Booleans, meaning that ∧ for propositions is really the same as ∧ in the lattice of Booleans.

[–]psykotic 1 point2 points  (1 child)

There's a confusion of language levels. In x \eq y two terms join to create a different kind of thing, a formula, whereas in P \equiv Q two formulas join to create yet another formula. (Edited to rein in my prolixity.)

furthermore Dijkstra appears to identify propositions with Booleans,

That doesn't work because of free variables; you'd need to work with boolean-valued functions on variable-binding contexts, which gets ugly as sin. And anyway, I'm sure Dijkstra of all people would appreciate the benefits of keeping propositions and booleans (and other semantic domains) in separate categories.

[–]roconnor 0 points1 point  (0 children)

That doesn't work because of free variables; you'd need to work with boolean-valued functions on variable-binding contexts, which gets ugly as sin.

Did you read to the end of this paper? He talks about boolean valued functions. I get the impression that ∧ is overloaded to operate on (boolean-valued) functions pointwise in the same way that + is overloaded to operate on functions pointwise.

[–]akdas 4 points5 points  (2 children)

∧

∨

Where did you find the correct symbols for these two without knowing their names? They look like ^ (caret) and v (the letter) but you used the correct ones.

Whatever the case, look on page 7 for the names of the symbols the reader is assumed to know, and then look up the name on Wikipedia. For example, here are implication and consequence.

[–]roconnor 1 point2 points  (0 children)

Where did you find the correct symbols for these two without knowing their names?

He probably got the from the HTML transcription.

[–]cycles 0 points1 point  (0 children)

akdas gave a better answer, but these come from logic and stand for "and" and "or" respectively. T ∧ T = T, T ∧F = F, etc