For the book
Computational Intractability: A Guide to Algorithmic Lower Bounds
by Demaine-Gasarch-Hajiaghayi
(See here for a link to a first draft.)
we had to make some choices about which notation to use. One of the least important ones was the following:
When defining NP, and in a few other places should we use:
(\exists y)(\forall y)[B(x,y)]
or
\exists x : \forall y : B(x,y)
or
something else.
We ended up doing it the second way. But I wondered, which, if either, is standard. So I looked in many math and theoretical CS books looking for places they used quantifiers. Here is what I found
a) Most papers and books really don't use quantifiers at all! This surprised me.
b) When quantifiers are used, they are used in definitions, not theorems.
c) One exception is in logic when they deal with formulas as objects onto themselves. For example, the inductive definition of a formula will have a step:
If f(x_1,...,x_n) is a formula then (\exists x_i)[f(x_1,...,x_n)] is a formula.
d) Here is a list of the few places I saw quantifiers used and if they used parenthesis or not. I say if it has parenthesis (abbreviated Parens) or not, and if the matrix of the formula is in square brackets, no brackets, or something ese.
Cook's classic paper . Page 154 Parens, no Brackets (1971)
Stockmeyer's paper where he defines PH. Page 6 Parens and Brackets (1976)
Computers and Intractability by Garey & Johnson. Page 164. Parens and Brackets (1979)
Morass-like construction of aleph_2 trees in L by Devlin. Page 2 Parens and matrix in Parens (1979)
Descriptive Complexity by Immerman. Page 38 Parens no Brackets (1999)
Bounded Queries in Recursion Theory by Gasarch and Martin. Parens and Brackets Throughout the book. (1999)
Complexity Theory from Godel to Feynman by Rudich. No Parens, No Brackets in Def of PH. (2003)
Parameterized Complexity Theory by Flum & Grohe. Page 81 no Parens and no Brackets.
Computational Complexity: A Modern Approach by Arora & Barak. Page 40. No Parens No Brackets.(2007)
Computational Complexity: A Conceptual Prospective by Goldreich. Page 114 no parents, no brackets (2008)
On Quantifer Rank Equivalence between linear orders by Siders. On page 417 they use quantifiers to state a theorem, which is unusual. Parens no brackets.
Presburger arithmetic, Rational Generating Functions, and quasi polynomials by Woods. Parens no Brackets. (2012)
Who witness's the Witness by Abel et al. On Page 69 (which the pointer takes you to) No Parens, no brackets. Colons between quantifiers (2018).
e) What to make of all this?
First off- the RARITY of the use of quantifiers really surprised me. The only place I saw them used a lot was my book, co-authored with Georgie Martin, Bounded Queries in Recursion Theory. Perhaps it would have sold better if I didn't use so many quantifiers. Oh well.
Second off- Later works don't use parens and brackets. This is most clear if you just look at Complexity Theory Books
Garey & Johnson - 1979- parens and brackets
Flun & Grohe- 1998- no parens and no brackts
Immerman- 1999 - parens but no brackets (this is the one exception)
Arora & Barack- 2007 no parens and no brackets
Goldreich-2008- no parens and no brackets
If you have a complexity theory book around that is not on this list, look up the definition of NP and the definition of the Poly Hierarchy and see (a) if they use parens around the quantifiers, and (b) if they use square brackets or no brackets of something else. Please leave a comment about it so I test the conjecture that parenthesis are just so 1979.
Good notation question!
ReplyDeleteAs for the "RARITY of the use of quantifiers"....
I thought there were some quantifiers in Papadimitriou's 1994 book (but not on pages defining NP).
Yet another classic "Randomized Algorithms" by Motwani (intriguingly, this book doesn't make it as reference in your book) ... has some quantifiers on page 20 when defining NP, yet served w/o parens.
I vote for always parenthesize/always bracket. But it's a programming thing (I've seen operator precedence biting people too often), not a theory thing.
ReplyDeleteI'd gues that in proofs (at least in the statement of the thing to be proved), the for alls and there exists appear in language, not notation, e.g. "Given any integers n and m > 0..." and the like.
At least that's what statements of theorems look like in the Discrete Math texts I'm looking at.
In a French computational complexity book:
ReplyDelete- NP is defined in plain French, so no quantifiers but "il existe" and "pour tout";
- PH is defined using oracles, so no quantifier;
- a characterization of PH using quantifiers is given, using this time quantifiers with no parens, no brackets.
Also, I find uncommon your solution with colons as a separator. It seems more common to either using no separator, or a simple comma.*
Finally, I completely agree with what you write: "parenthesis are just so 1979."
I have no idea about complexity theory books. I've read quite a few math and logic books (although most of my books are pretty old). I'd do
ReplyDelete\exists x \forall y B(x,y)
That is, no extra punctuation unless it was needed to make things clear.
The first paper I wrote, I used some quantifier symbols. A friend pointed out that symbols are sometimes harder to read than are words, so I replaced the quantifier symbols with words.
We all strive for clean, clear, consistent and minimalistic notation that might even be useful in a programmatic context ... so, it's an interesting observation and good question!
ReplyDeleteTwo obvious oracles that have given some deeper thought in this direction -- Don Knuth and Leslie Lamport (in particular, see TLA specs).
See, also Kolaitis and Vardi in "The Decision Problem for the Probabilities of Higher-Order Properties" on page 11 (no: parens, bracks)
[https://www.cs.rice.edu/~vardi/papers/stoc87rj.pdf]
This comment has been removed by a blog administrator.
ReplyDeleteI think the use of the word "such that" is underrated and that should be used instead of the :'s
ReplyDelete