Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

I recently discovered that I have a fondness for the work of Dijkstra. I am currently reading random EWDs, and stumbled across one with some notation that I couldn't quite grasp.

Dijkstra states that $[ x < y \implies f.x.y < f.y.x]$

OK, so. This isn't a list comprehension, right? Why the brackets?

Also, how could this be read aloud? What does $\implies$ mean?

And finally, what does $f.x.y$ and $f.y.x$ mean?

And how could this statement be written more conventionally? And does Dijkstra's notation derive from anything, or is it entirely his own invention?

share|improve this question

1 Answer 1

I think this would read as follows in modern notation (although field-local variations are possible):

$$\forall x y. x < y \Rightarrow f(x,y) < f(y,x).$$

Read aloud: for all x and y, x is less than y implies that f of x and y is less than f of y and x.

If you read the first sentence of the linked document, it says that square brackets represent universal quantification over $x$ and $y$. The second states that $f$ is a function. => is ASCII art for $\Rightarrow$ (logical implication).

The main problem here is missing context (and detective skills). This article refers to EWD878. Perhaps looking there would have helped. Indeed, looking at that article, you see notation slightly closer to what is used today (at least, by Haskell programmers: f.x.y becomes f\ x\ y).

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.