3
$\begingroup$

Continuing https://tex.stackexchange.com/questions/435986/how-to-draw-the-box-of-dijkstras-guarded-command-language, what is the difference in the intended usage of ⫾ (Dijkstra choice, U+2AFE) and ⫿ (n-ary Dijkstra choice, U+2AFF) in the context of the Guarded Command Language (GCL) of Dijkstra? In other words, when do you use ⫾ and when ⫿ for typesetting GCL programs?

Related:

$\endgroup$
3
$\begingroup$

Non-deterministic guarded choice is an associative-commutative binary operator. My guess is that the character ⫾ U+2AFE is intended to be used as an infix binary operator and the character ⫿ U+2AFF, which is larger and described as “n-ary”, is intended to be used as a prefix operator which is typeset larger, in prefix position, and typically with a subscript and sometimes a superscript to indicate the range over which the operation is carried out.

$$⫿_{i=1}^n c_i \rightarrow a_i \qquad = \qquad \mathsf{if}\; c_1 \rightarrow a_1 ⫾ \cdots ⫾ c_n \rightarrow a_n \;\mathsf{fi}$$

Typeset with inline math: $⫿_{i=1}^n c_i \rightarrow a_i = \mathsf{if}\; c_1 \rightarrow a_1 ⫾ \cdots ⫾ c_n \rightarrow a_n \;\mathsf{fi}$

It's the same relationship as between $+$ (binary) and $\sum$ (n-ary), or between $\times$ (binary) and $\prod$ (n-ary) ($\prod$ is sometimes a different product such as $\cdot$). For binary operators other than the two classics addition and multiplication, the n-ary version is the same glyph, just bigger.

$\endgroup$
  • $\begingroup$ Got it; thx! Btw., I still remember you meta-post. Any alternative comp.sci. forums found so far? As for latex, I'm moving to latex.org/forum, as you see above :-). By the way, I removed the tick since you made a guess (which is excellent, but still a guess; I upvoted), whereas in the future some of the folks who suggested the addition of the characters to Unicode (or who agreed to this addition) might hypothetically stop by and answer the question with a full rationale. I hope you don't mind, and I apologize if you do. $\endgroup$ – user110815 Oct 18 at 21:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy