[math-fun] Dijkstra's square operator?
I'm trying to understand these slides about the fixed point fusion theorem, but the author is using some notation from Dijkstra I've never seen and don't have access to the book where it's defined. Can anyone parse this statement for me? I'm typesetting it a couple different ways, hoping one of them works for you. x∈S ⇒ b ≣ S ⊆ if b ➝∑* □ ¬b➝∑* - {x} fi x \in S \Rightarrow \equiv S \subseteq if b \to \Sigma^{*} \square \lnot b \to \Sigma^{*} - \{x\} fi Or can anyone point me at an explanation that uses a different notation? -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com
I found a site explaining his notation: http://www.cs.arizona.edu/icon/library/procs/dijkstra.htm On Tue, Dec 29, 2009 at 9:26 PM, Mike Stay <metaweta@gmail.com> wrote:
I'm trying to understand these slides about the fixed point fusion theorem, but the author is using some notation from Dijkstra I've never seen and don't have access to the book where it's defined.
Can anyone parse this statement for me? I'm typesetting it a couple different ways, hoping one of them works for you.
x∈S ⇒ b ≣ S ⊆ if b ➝∑* □ ¬b➝∑* - {x} fi
x \in S \Rightarrow \equiv S \subseteq if b \to \Sigma^{*} \square \lnot b \to \Sigma^{*} - \{x\} fi
Or can anyone point me at an explanation that uses a different notation? -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com
-- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com
I don't have Dijkstra's "A Discipline of Programming" on my shelf either --- though I do recall finding that his rather severe style makes it difficult to appreciate the considerable practical impact of his ideas. For a programmer, I'd recommend instead David Gries's "The Science of Programming" as a more approachable introduction to programming with guarded commands, invariants etc. This technology has been around now for decades --- yet still we are stuck with grotty old C syntax (C++, Java etc), defended as stoutly by its users today as Fortran and Cobol used to be in the 1960's. When are programmers going drag themselves into the second half of the twentieth century? WFL On 12/30/09, Mike Stay <metaweta@gmail.com> wrote:
I found a site explaining his notation: http://www.cs.arizona.edu/icon/library/procs/dijkstra.htm
On Tue, Dec 29, 2009 at 9:26 PM, Mike Stay <metaweta@gmail.com> wrote:
I'm trying to understand these slides about the fixed point fusion theorem, but the author is using some notation from Dijkstra I've never seen and don't have access to the book where it's defined.
Can anyone parse this statement for me? I'm typesetting it a couple different ways, hoping one of them works for you.
x∈S ⇒ b ≣ S ⊆ if b ➝∑* □ ¬b➝∑* - {x} fi
x \in S \Rightarrow \equiv S \subseteq if b \to \Sigma^{*} \square \lnot b \to \Sigma^{*} - \{x\} fi
Or can anyone point me at an explanation that uses a different notation? -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com
-- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
participants (2)
-
Fred lunnon -
Mike Stay