Dijkstra notation in physics or statistics

[bjbr...@gmail.com]

Hello All,

In the privacy of my own scribbling I am comfortable using Dijkstra's bracket notation and other conventions of the Calculus of Boolean Structures, but I haven't used it or seen it used in published work in physical science or applied statistics. But I just put a manuscript on Arxiv that uses the conventions extensively.

Estimating the Missing Mass, Partition Function or Evidence for a Case of Sampling from a Discrete Set

https://arxiv.org/abs/2603.13207

See the Section on Notation and the Appendix with Remarks on Notation, and of course all the manuscript for its application. The work needs some further development before it goes to a journal, and I have no idea how much the notation will be an issue.

Comments will be appreciated, and I will certainly appreciate to know of precedent for Dijkstra's notation in physics or statistics literature.

Bas Braams

[Diethard Michaelis]

Hi Bas,

My comments (sorry for being so late ...):

(0) "Dijkstra’s bracket notation"
is usually known as
"Eindhoven quantifier notation".
It might be useful to have a look in the books/writings of others using
Eindhoven notation [and calculational proof (Feijen proof format)].
I'd suggest Roland Backhouse for a very first try.

(1) For "bracket" see e.g. https://en.wikipedia.org/wiki/Bracket.
"bracket" is used for "square bracket", not "angle bracket".
But I'm not a native English speaker.

(2) The everywhere operator [P] might be best described by

[P] := (P = true), i.e. "P equals true".

This way [] is defined for any Boolean algebra.
Describing it as universal quantification over some obscure state space
is just a special case of (= true).

(3) The = symbol is indeed best used for "complete equality".
Even Dijkstra had some doubts with his "lifted" = ,
see the end of EWD 1300.

(4) EWD1300: "The Notational Conventions I Adopted, and Why"
https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1300.html
is more up to date on notation than the Dijkstra/Scholten book.
It is published in
Formal Aspects of Computing, Vol. 14, No. 2
https://doi.org/10.1007/s001650200030

(5) Boolean "structure"
for "element of a Boolean algebra"
seems to be quite uncommon outside Dijkstra's writings.
It somehow conflicts with the standard use of "structure"
and so it does in your paper.
I think there is even a comment by Dijkstra on it
suggesting a different terminology,
but I don't remember where nor what he suggested ...

Cheers,
Happy Easter Days,
Diethard.

[Kevin]

Hi.

(5) Boolean "structure"
for "element of a Boolean algebra"
seems to be quite uncommon outside Dijkstra's writings.
It somehow conflicts with the standard use of "structure"
and so it does in your paper.
I think there is even a comment by Dijkstra on it
suggesting a different terminology,
but I don't remember where nor what he suggested ...

At the bottom of EWD1086-2, he suggests the name "profiles".

Best regards

Kevin

[Diethard Michaelis]

Thanks!

I (must have) read EWD1086
https://www.cs.utexas.edu/~EWD/ewd10xx/EWD1086.PDF
from the Edsger W. Dijkstra Archive about 20 years ago
as it is on my list of
EWDs complementing the Dijkstra Scholten book
https://www.cs.utexas.edu/~EWD/AnnotationsEtc/Michaelis.html

Dijkstra's remark on "structures" therein sounds quite familiar ...

>> For lack of a better name, we called them
boolean and integer "structures" respectively.
(Had I have to name them now, I might have
chosen "profiles".) <<

... but I definitely forgot both the location and the term "profiles".

Further I remember "preds" as name for
"boolean structures" / elements of a boolean algebra.
(Perhaps in some paper or note by Rutger M. Dijkstra?)

Cheers
Diethard.

[bjbr...@gmail.com]

I understand why Dijkstra may have regretted to use "structure", but what would be wrong with "function"? (Viewing vectors, matrices and tensors as functions of their indices.) Let me leave it unresolved here and call them spf's for structure, profile or function, and spf's are compatible if they share the domain. For compatible boolean spf's we have \equiv for punctual equality and we have = for total equality. I would never want to use = for punctual equality, it creates no end of trouble. If an operator is wanted for punctual equality for other than boolean structures then one can just overload \equiv. (I mention it in my Arxiv manuscript above, but that is not the place to develop it further.)

[Kevin]

Further I remember "preds" as name for

"boolean structures" / elements of a boolean algebra.

(Perhaps in some paper or note by Rutger M. Dijkstra?)

I don't recall "preds" but RMD uses the term "specks" in "A Mathematical Approach to Logic" (rutger20)

Best regards,

Kevin

[Diethard Michaelis]

Hi Bas,

> I understand why Dijkstra may have regretted to use "structure", but what
> would be wrong with "function"? (Viewing vectors, matrices and tensors as
> functions of their indices.) Let me leave it unresolved here and call them
> spf's for structure, profile or function, and spf's are compatible if they
> share the domain. For compatible boolean spf's we have \equiv for punctual
> equality and we have = for total equality. I would never want to use = for
> punctual equality, it creates no end of trouble. If an operator is wanted
> for punctual equality for other than boolean structures then one can just
> overload \equiv. (I mention it in my Arxiv manuscript above, but that is
> not the place to develop it further.)

Had another look into your manuscript:
My comment (5) on the (Dijkstra's) use of "structure"
seems not that important / appropriate here.
Your use of "structure" is quite OK within the manuscript.
It even can't be replaced by "profile" (or even "function")
without heavily rewriting the affected sentences.
And "profile" might unnecessarily confuse the reader.
Sorry.

As for using = for total equality I completely agree, see my (3).
Then everywhere [] is a special case of total equality, see my (2),
[p] := (p = true) .
Nice, general, and simple.
(See also the (rutger20) paper mentioned by Kevin -- thanks!.)
For function f this becomes
[f] = <∀s::f(s) = true>
as total equality for functions f,g is defined this way
f = g := <∀s::f(s) = g(s)>.

Diethard.