How to write a negative review for a conference paper?

I think this is too much of a duplicate of the other question, but my comment got too long.

Firstly, the review process is blind, so you simply have to do the best that you can. Be objective, be polite, give good reasons – see other question.
There is probably no such thing has having technical comments/improvements that are too long for the standard review, unless you will end up rewriting the paper. Authors tend to appreciate comments, even if they mean more work. If the paper is borderline and is worth improving, then give as many comments as you have time for.
If you have additional comments that you want to send to the authors, consult with the chair/editor before contacting the authors. Perhaps your comments can be sent anonymously via the chair/editor.
Papers get rejected, we learn to live with it. The best you can do is provide good comments to help the authors improve the paper for next time round. Authors may get mad, but they don't get even.
If the paper is terrible, just save your time and don't bother with all the comments. Write a sufficiently convincing review giving reasons why the paper should be rejected, point out that there are many typos and other mistakes, but don't enumerate them all.
On the other hand, if you are presenting and proving an alternative axiomatisation of their results to the degree that you are not only rewriting their paper, but lifting their results to a whole new level, then you should consult the chair/editor to see what to do. Maybe you should get credit for your contribution. You certainly should never write up your results independently, not until the paper has appeared in print.


Where do most REGEX implementations fall on the complexity scale?

I don't think that the real problem is the question of what unbounded means; this is no worse than any other situation in parsing.

The trouble lies with characterizing backreferences, which are both very powerful and very limited: they allow description of some non-context-free languages, without allowing some context-free languages. For example, the regex (a*)b\1b\1 matches strings of the form $a^n \cdot b \cdot a^n \cdot b \cdot a^n$, and you can use the pumping lemma to show this is not a context-free language. However, on the other hand, regexes with backreferences don't seem to be sufficient to match the balanced parenthesis language, which is the prototypical context-free language.

It's easy enough to give a denotational semantics saying what strings are in a language to regexes, but giving a good automata-theoretic characterization seems much more challenging. It's something like a register machine, into whose registers you can copy substrings of your input, and which you can use to test your current string against, but for which you lack the ability to modify these registers.

People doing finite model theory have a bunch of funky machine models, and it would be interesting to know if this corresponds to any of their models.


This is a well known problem. It's known to be impossible to solve exactly, but either approximable in the sense you describe or solvable exactly if you relax the conditions under which it recognizes a majority: see http://en.wikipedia.org/wiki/Majority_problem_(cellular_automaton)


In what fields does a knowledge of formal semantics prove useful?

Formal semantics is useful primarily when you want to reason about programs.

In the past this was mainly done in programming language development (and to a lesser degree in compiler construction). Increasingly formal semantics is also used in automatic and interactive program verification, which is beginning to see industrial use. Since you are interested in compiler design, verified and certifying compilation is a hot research topic now that is based heavily on formal semantics. Check out the following systems.

X. Leroy's CompCert. This was the first verified compiler: a realistic, moderately-optimizing compiler for a large subset of the C language down to PowerPC and ARM assembly code.
The MPI's Pilsner, the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Most prior work (such as CompCert) has focused on verifying whole-program compilers.
CakeML. A compiler for an ML dialect. The focus of CakeML is on minimising the trusted computing base, not on optimisation or on breadth of source language features.
Cogent. A certified compiler from a simple functional language with linear types (useful for reasoning about memory management) to C.

Progress on such compilers has been much swifter than many (including myself) anticipated, and I expect to see more and more of this work to seep into industrial compilers.

The problem with formal semantics is rarely to write down the semantics of a language. That's usually simple.  The real issue is how efficiently to prove theorems about programs in a language using the semantics.


I guess there is no consensus among researchers and academics on the security of Bitcoin protocol. Thanks to Stack Exchange Network, The following links should help you to answer some of your questions:

1- Bitcoin research at Cryptography StackExchange

2- How secure is the Bitcoin protocol? at Cryptography StackExchange

3- Are there any fundamental security vulnerabilities in Bitcoin? at Bitcoin Stackexchange

Here is a comprehensive list of research publications at Bitcoin wiki that include research and analysis of Bitcoin.


Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy.

The reason it is not widely used is because impredicative quantification is incompatible with classical logic. If you have it, you cannot give a model of type theory where types are interpreted as sets in the naive way --- see John Reynolds's famous paper Polymorphism is Not Set-theoretic.

Since many people want to use type theory as a way to machine-check ordinary mathematical proofs, they are generally unenthusiastic about type-theoretic features which are incompatible with the usual foundations. In fact, Coq  originally supported impredicativity, but they have steadily abandoned it.


Can programming help one understand constructive mathematics?

Agda is a dependently typed programming language and/or proof assistant for Martin-Löf type theory. Programming in Agda feels very much like programming in Haskell. For example, inductive proofs are written as recursive functions with multiple equations that pattern match on the function arguments. So programming and/or proving in Agda is a good way to learn about constructive mathematics coming from a (functional) programming background.


Relation between variance and mutual information

I think you can show it as follows, and even get a better constant in the end. Forewarning, there's enough cleverness here that I'm kind of suspect that everything is right. But the basic idea is simple enough: reduce to the case where $X$ and $Y$ take values in $\{0,1\}$, where we can exploit a nice relationship between covariance and total variation distance for such variables. From there, the rest of your proof idea works out.

First, introduce $\tau_X$ and $\tau_Y$ as uniform, independent draws from
$[0,1]$.
Define $\hat{X} = 1$ if $X \ge \tau_X$ and $\hat{X}=0$ otherwise, and define
$\hat{Y}$ similarly. Then we have the following relationships:

$\mathrm{Cov}[\hat{X},\hat{Y}]=\mathrm{Cov}[X,Y]$.
$|\mathrm{Cov}[\hat{X},\hat{Y}]| = \frac{1}{2}\hat{\delta}$ where $\hat{\delta}$ is the TVD of the joint distribution of $\hat{X},\hat{Y}$ from the product of the marginals (analogous to your $\mu$ and $\eta$).
$I[\hat{X} : \hat{Y}] \le I[X : Y]$

These can be combined with Pinsker's inequality to prove your claim (even halving the constant).

(1) follows easily by computing $\mathbb{E}[\hat{X}|X]=\mathbb{P}[\tau_X \le X|X] = X$, and similar for $Y$ and $XY$.

(2) can be worked out as follows. Let $a,b,c,d$ be the probabilities that $(\hat{X},\hat{Y})$ takes the values $(0,0), (0,1), (1,0), (1,1)$, respectively. We can write $|\mathrm{Cov}[\hat{X},\hat{Y}]| = |d - (c+d)(b+d)|$. But covariance is invariant under shifts of the variables, and flips sign when a variable is negated. All together, we have
$$|\mathrm{Cov}[\hat{X},\hat{Y}]| = \left\{
\begin{array}{ccl}
|\mathrm{Cov}[\hat{X},\hat{Y}]| &=& |d - (b+d)(c+d)| \\
|\mathrm{Cov}[\hat{X},1-\hat{Y}]| &=& |c - (a+c)(c+d)| \\
|\mathrm{Cov}[1-\hat{X},\hat{Y}]| &=& |b - (a+b)(b+d)| \\
|\mathrm{Cov}[1-\hat{X},1-\hat{Y}]| &=& |a - (a+c)(a+b)|
\end{array}\right.$$
If you write out the quantity $|| \hat{\mu} - \hat{\eta} ||_1$, where $\hat{\mu}$ is the joint distribution of $(\hat{X},\hat{Y})$, and $\hat{\eta}$ is the product of the marginals, then it's the sum of the above four quantities, hence four times the covariance. Dividing through by 4 and writing $||\hat{\mu} - \hat{\eta}||_1$ as $2\hat{\delta} (= 2\delta(\hat{\mu},\hat{\eta}))$ gives (2).

(3) follows from the data processing inequality. Note that once $X$ is fixed, $\hat{X}$ depends only on $\tau_X$, which is independent of everything else (even conditioned on $X$), and similarly with all the $X$'s replaced by $Y$'s. Thus the DPI can be applied twice to give (3), as follows:
$$\begin{align*}
I[X : Y] &\ge I[\hat{X} : Y] \\
&\ge I[\hat{X} : \hat{Y}]
\end{align*}$$


Reinforcement Learning and Optimistic Decisions

The main idea of following upper confidence bounds is minimizing regret, that is, the difference between the received reward and the maximum. The paper to read on this is: "Finite-time analysis of the multiarmed bandit problem" by Peter Auer, Nicoló Cesa-Bianchi, and Peter Fischer.

If we interpret life as a Markov Decision Process, then most reinforcement learning theories apply quite well. I.e. we want to keep an open mind, but we want to do what we think is best exponentially more often than exploratory actions.

Of course, interpreting life as an MDP is a bit of a stretch — foresight, for example, has to be interpreted as simulated experience, but I believe one can find quite a lot of wisdom in reinforcement learning and artificial intelligence in general.


This is an open problem: It is open whether $\mathrm{DTISP}(O(n \log n),O(n)) = \mathrm{DSPACE}(O(n))$ (or even $\mathrm{NSPACE}(O(n))$). We only know that $\mathrm{DTIME}(O(n))⊆\mathrm{DSPACE}(O(n/\log n))$.

However, under plausible computational complexity conjectures, there is a proper hierarchy.  For example, if for every $ε>0$, CIRCUIT-SAT ∉ i.o.-$O(2^{n-ε})$, then
$\mathrm{DTISP}(O(f),O(s(n))) ⊊ \mathrm{DTISP}(O(f^{1+ε}),O(s(n)))$
where $f(n)≥n$, $f(n)$ is $2^{o(\min(n,s(n)))}$, and $f$ is time-space constructible.

In particular (under the hypothesis), existence of a satisfying assignment for circuits with $⌊\mathrm{lg}(f^{1+ε/2})⌋$ inputs and size $(\log f)^{O(1)}$ serves as a counterexample to the equality of the classes.

Notes:

CIRCUIT-SAT is at least as hard as $k$-SAT (which is used in the strong exponential time hypothesis).
Per convention, in CIRCUIT-SAT, $n$ is the number of input wires; circuit size is $n^{O(1)}$.
If the assumption used CIRCUIT-SAT for quasilinear circuit sizes, then the bound on $f(n)$ can be relaxed to $O((2-ε)^{\min(n,s(n))})$.  Also, weaker/stronger assumptions on hardness of CIRCUIT-SAT give weaker/stronger hierarchies (that we can currently prove).
i.o. means infinitely often, and can be dropped for $f$ that are in a certain sense continuous (including $f(n)=n^a$).
It appears likely that the DTISP hierarchy is sharp enough to distinguish $O(f)$ from $o(f/\log f)$ (and perhaps $o(f)$) (when $f$ is not too large relative to the permitted space).
To distinguish $n^a$ from $2^n$, we only need the weaker assumption P≠PSPACE.


The problem as described is not convex, due to the nonconvexity of the constraint set. However, if you were to permit a relaxation, we could write your problem as
$\begin{array}{ll}
\max & \sum_{p\in P} t_p\\
\text{subject to }& t_p \geq \langle x, \|p\| p \rangle\\
& t_p \geq -\langle x, \|p\| p\rangle ,\\
&  \|x\|_2 \leq 1.
\end{array}$
This is a second-order cone program, which can be solved by standard methods.
It is probably not trivial to recover a solution to your original problem from this relaxation (for instance, Goemans-Williamson wrote a breakthrough paper describing the rounding algorithm for a similar relaxation). But maybe this is helpful in some way.
edit -- As pointed out by Neal Young, there is an error in the above answer. The question in the original post is a maximization of absolute value function, which isn't a convex objective; so, my reduction is incorrect. I am leaving the incorrect answer here in case someone finds any information in it useful, but please see Neal Young's comments below for more comprehensive (and correct) observations about the problem.


Reference for context-free grammar for Martin-Löf type theory

Generally, there will be one context-free grammar for both types and terms, and judgements will be used to identify those expressions which are types and which expressions are terms of a particular type.
This has been written down many, many times. For a pretty typical example, you could look at Abel, Coquand and Dybjer's LICS 2007 paper, Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements.


Where can you find job postings for faculty positions in CS theory?

The CRA jobs site is still the best place, although it's not theory-centric. Given the proliferation of postdocs in theoryCS, I think it would be nice to have a dedicated place for theory job postings.


What algorithms do you know for beltway reconstruction?

Paul Lemke Steven S. Skiena Warren D. Smith, Reconstructing Sets From Interpoint Distances, gave backtracking algorithm that runs in time $O(n^n \log n)$ for the beltway reconstruction problem. As far as I know, this is the best known. The exact complexity of the problem is not known. It is not known to be in $P$ and neither known to be $NP$-complete.


What math courses should I take to prepare for a CS masters or PhD?

A generally high degree of mathematical maturity makes a lot of the formal aspects of (not necessarily theoretical) computer science much easier to understand. So doing a minor in mathematics along with your major in computer science would do more good than harm.


Is it possible to convert a Max heap to a Min heap in place?

You can just ignore that you have a max heap and build your min heap from it. O(n) time
complexity. No need for additional array.


Searching for name of equivalence property in hamiltonian paths

The 2-OPT heuristic for finding TSP tours is fairly close to what you're asking about. It's a local improvement algorithm which looks for sections of a TSP tour which, when reversed, will yield a shorter tour. The 3-OPT and the Lin-Kernighan heuristics work along the same lines, but use more complicated moves.

Looking for the optimal rearrangement of some subpath of a TSP tour is going to be inefficient unless it only involves a short section of this tour, and then I imagine it will be inferior to more global rearrangement algorithms such as 2-OPT (which can reverse a large subpath of a tour).

As far as I know, the concept that you're asking about has no name.


Automata Theory / Formal Language Thesis Topic

I think David Eppstein is too dismissive of the area of automata theory and formal languages.  The claim that "getting it published in top-level conferences and convincing someone to hire you once you graduate may be problematic" seems to be what Haldane called Aunt Jobiska’s Theorem: "It’s a fact the whole world knows."

In fact, there are good conferences (such as STACS and ICALP) that routinely publish results in automata theory and formal languages; there are well-attended conferences (such as DLT) that focus on the area; it is a very active area in Germany, France, and Italy; there are great open problems in the area; and I know many students that have had no problem getting jobs.


Does there exist an extension of regular expressions that captures the context free languages?

Yes, there is. Define a context-free expression to be a term generated
by the following grammar:

$$
\begin{array}{lcll}
g & ::= & \epsilon & \mbox{Empty string}\\
  &  |  & c        & \mbox{Character $c$ in alphabet $\Sigma$} \\
  &  |  & g \cdot g & \mbox{Concatenation} \\
  &  |  & \bot      & \mbox{Failing pattern} \\
  &  |  & g \vee g  & \mbox{Disjunction}\\
  &  |  & \mu \alpha.\; g & \mbox{Recursive grammar expression} \\
  &  |  & \alpha    & \mbox{Variable expression}
\end{array}
$$

This is all of the constructors for regular languages except Kleene
star, which is replaced by a general fixed-point operator $\mu
\alpha.\;g$, and a variable reference mechanism. (The Kleene star is
not needed, since it can be defined as $g\ast \triangleq \mu
\alpha.\;\epsilon \vee g\cdot\alpha$.)

The interpretation of a context-free expression requires accounting
for the interpretation of free variables. So define an environment
$\rho$ to be a map from variables to languages (i.e., subsets of
$\Sigma^*$), and let $[\rho|\alpha:L]$ be the function that behaves
like $\rho$ on all inputs except $\alpha$, and which returns the
language $L$ for $\alpha$.

Now, define the interpretation of a context-free expression as follows:

$$
\newcommand{\interp}[2]{[\![{#1}]\!]\;{#2}}
\newcommand{\setof}[1]{\left\{#1\right\}}
\newcommand{\comprehend}[2]{\setof{{#1}\;\mid|\;{#2}}}
\begin{array}{lcl}
\interp{\epsilon}{\rho} & = & \setof{\epsilon} \\
\interp{c}{\rho}        & = & \setof{c} \\
\interp{g_1\cdot g_2}{\rho} & = & \comprehend{w_1 \cdot w_2}{w_1 \in \interp{g_1}{\rho} \land w_2 \in \interp{g_2}{\rho}} \\
\interp{\bot}{\rho} & = & \emptyset \\
\interp{g_1 \vee g_2}{\rho} & = & \interp{g_1}{\rho} \cup \interp{g_2}{\rho} \\
\interp{\alpha}{\rho} & = & \rho(\alpha) \\
\interp{\mu \alpha.\; g}{\rho} & = & \bigcup_{n \in \mathbb{N}} L_n \\
\mbox{where} & & \\
L_0 & = & \emptyset \\
L_{n+1} & = & L_n \cup \interp{g}{[\rho|\alpha:L_n]}
\end{array}
$$

Using the Knaster-Tarski theorem, it's easy to see that the
interpretation of $\mu \alpha.g$ is the least fixed of the expression.

It's straightforward (albeit not entirely trivial) to show that you
can give a context-free expression deriving the same language as any
context-free grammar, and vice-versa. The non-triviality arises from
the fact that context-free expressions have nested fixed points, and
context-free grammars give you a single fixed point over a tuple. This
requires the use of Bekic's lemma, which says precisely that a nested
fixed points can be converted to a single fixed point over a product (and
vice-versa). But that's the only subtlety.

EDIT: No, I don't know a standard reference for this: I worked it out
for my own interest. However, it's an obvious enough construction that
I'm confident it's been invented before. Some casual Googling reveals
Joost Winter, Marcello Bonsangue and Jan Rutten's recent paper
Context-Free Languages, Coalgebraically, where they give a variant
of this definition (requiring all fixed points to be guarded) which
they also call context-free expressions.


What are some applications of computational geometry towards computer vision?

Probably the most useful application of computational geometry within computer vision is in the realm of shape analysis/matching and image registration. There's a lot to google here, but you can start with Kendall's book on shape space, and also look at problems of measuring the distance between shapes.


Can a random oracle change which TFNP problems are strongly hard-on-average?

No to my title, and Yes to my question's body.  This in fact generalizes immediately

  to every polynomial-length game that does not use the adversaries' code.

Note that I will be using $C$ for the adversaries, rather than $A$,

so as to match up with Theorem 2's notation.

Assume that for almost all oracles $\mathcal{O}$, there exists a P/poly

oracle-algorithm $C$ such that $\operatorname{Pr}_x\hspace{-0.06 in}\left[\hspace{.02 in}R\hspace{-0.04 in}\left(x,\hspace{-0.04 in}C^{\mathcal{O}\hspace{-0.02 in}}(x)\hspace{-0.03 in}\right)\hspace{-0.02 in}\right]$ is non-negligible.

For almost all oracles $\mathcal{O}$, there exists a positive integer d such that

there exists a sequence of circuits of size at most d+nd such that

$\operatorname{Pr}_{x\in \{0,1\}^n}\hspace{-0.06 in}\left[\hspace{.02 in}R\hspace{-0.04 in}\left(x,\hspace{-0.04 in}C^{\mathcal{O}\hspace{-0.02 in}}(x)\hspace{-0.03 in}\right)\hspace{-0.02 in}\right]$ is infinitely-often greater than $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^d\hspace{-0.02 in}\right)$.

By countable additivity, there exists a positive integer d such that for a non-null set of oracles $\mathcal{O}$, there exists a sequence of circuits of size at most d+nd such that

$\operatorname{Pr}_{x\in \{0,1\}^n}\hspace{-0.06 in}\left[\hspace{.02 in}R\hspace{-0.04 in}\left(x,\hspace{-0.04 in}C^{\mathcal{O}\hspace{-0.02 in}}(x)\hspace{-0.03 in}\right)\hspace{-0.02 in}\right]$ is infinitely-often greater than $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^d\hspace{-0.02 in}\right)$.

Let j be such a d, and let z be the (not-necessarily-efficient) oracle-algorithm which

takes n as input and outputs the lexicographically least oracle-circuit of size at most j+n$^{\hspace{.03 in}j}$

that maximizes $\operatorname{Pr}_{x\in \{0,1\}^n}\hspace{-0.06 in}\left[\hspace{.02 in}R\hspace{-0.04 in}\left(x,\hspace{-0.04 in}C^{\mathcal{O}\hspace{-0.02 in}}(x)\hspace{-0.03 in}\right)\hspace{-0.02 in}\right]$.    By the contrapositive of Borel-Cantelli, $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^2\hspace{-0.02 in}\right) \: < \: \operatorname{Prob}_{\mathcal{O}}\hspace{-0.05 in}\bigg[\hspace{-0.02 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.03 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right) < \operatorname{Pr}_{x\in \{0,1\}^n}\hspace{-0.06 in}\left[\hspace{.02 in}R\hspace{-0.04 in}\left(\hspace{-0.04 in}x,\hspace{-0.04 in}\left(z^{\mathcal{O}}\right)^{\hspace{-0.04 in}\mathcal{O}\hspace{-0.02 in}}(x)\hspace{-0.05 in}\right)\hspace{-0.02 in}\right]\hspace{-0.06 in}\bigg] \;\;\;$ for infinitely many n.

For such n,

$1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right) \; = \; 1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.04 in}\left(\hspace{-0.02 in}n^2\hspace{-0.02 in}\right)\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right)\hspace{-0.04 in}\right) \; = \; \left(\hspace{-0.02 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^2\hspace{-0.02 in}\right)\hspace{-0.03 in}\right) \cdot \left(\hspace{-0.02 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right)\hspace{-0.03 in}\right) \; < \; \operatorname{Prob}_{\mathcal{O}\hspace{.02 in},\hspace{.04 in}x\in \{0,1\}^n}\hspace{-0.06 in}\left[R\hspace{-0.04 in}\left(\hspace{-0.04 in}x,\hspace{-0.04 in}\left(z^{\mathcal{O}}\right)^{\hspace{-0.04 in}\mathcal{O}\hspace{-0.02 in}}(x)\hspace{-0.05 in}\right)\hspace{-0.02 in}\right]$

.
Let $A$ be the oracle-algorithm that takes 2 inputs, one of which is $n$, and does as follows:

Choose a random n-bit string $x$.  Attempt to

[parse the other input as an oracle-circuit and run that oracle-circuit on the n-bit string].

If that succeeds and the oracle-circuit's output $y$ satisfies R(x,y), then output 1, else output 0.

(Note that $A$ is not just the adversary.)

For infinitely many n, $\;\;\; 1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right) \; < \; \operatorname{Prob}_{\mathcal{O}}\left[A^{\mathcal{O}}(n,z^{\mathcal{O}}(n))\right] \:\:\:\:$.

Let p be as in Theorem 2, and set $\;\;\; f \: = \: 2\hspace{-0.04 in}\cdot \hspace{-0.04 in}p\hspace{-0.04 in}\cdot \hspace{-0.04 in}\left(\hspace{.02 in}j\hspace{-0.04 in}+\hspace{-0.04 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right)\hspace{-0.04 in}\cdot \hspace{-0.04 in}n^{(2+j)\cdot 2} \:\:\:\:$.

By Theorem 2, there exists an oracle-function $\mathcal{S}$ such that with $\mathcal{P}$ as in that theorem,

if $\;\;\; 1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right) \; < \; \operatorname{Prob}_{\mathcal{O}}\left[A^{\mathcal{O}}(n,z^{\mathcal{O}}(n))\right] \;\;\;$ then

$1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{2+j}\right)\hspace{-0.04 in}\right) \; = \; \left(\hspace{-0.02 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right)\hspace{-0.03 in}\right)-\left(\hspace{-0.04 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{2+j}\right)\hspace{-0.04 in}\right)\hspace{-0.04 in}\right) \; = \; \left(\hspace{-0.02 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right)\hspace{-0.03 in}\right)\hspace{-0.04 in}-\hspace{-0.04 in}\sqrt{1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{(2+j)\cdot 2}\right)\hspace{-0.04 in}\right)}$

$= \; \left(\hspace{-0.02 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right)\hspace{-0.03 in}\right)\hspace{-0.04 in}-\hspace{-0.04 in}\sqrt{\left(p\hspace{-0.04 in}\cdot \hspace{-0.06 in}\left(\hspace{.02 in}j\hspace{-0.04 in}+\hspace{-0.04 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right)\hspace{-0.04 in}\right)\hspace{-0.06 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}2\hspace{-0.06 in}\cdot \hspace{-0.04 in}p\hspace{-0.04 in}\cdot \hspace{-0.06 in}\left(\hspace{.02 in}j\hspace{-0.04 in}+\hspace{-0.04 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right)\hspace{-0.06 in} \cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{(2+j)\cdot 2}\right)\hspace{-0.04 in}\right)} \; = \; \left(\hspace{-0.02 in}1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right)\hspace{-0.03 in}\right)\hspace{-0.04 in}-\hspace{-0.04 in}\sqrt{\left(p\hspace{-0.04 in}\cdot \hspace{-0.06 in}\left(\hspace{.02 in}j\hspace{-0.04 in}+\hspace{-0.04 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right)\hspace{-0.04 in}\right)\hspace{-0.06 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.04 in}f\right)}$

$< \; \operatorname{Prob}_{\mathcal{O}}\left[A^{\mathcal{O}}(n,z^{\mathcal{O}}(n))\right]-\hspace{-0.04 in}\sqrt{\left(p\hspace{-0.04 in}\cdot \hspace{-0.06 in}\left(\hspace{.02 in}j\hspace{-0.04 in}+\hspace{-0.04 in}n^{\hspace{.04 in}j}\hspace{-0.02 in}\right)\hspace{-0.04 in}\right)\hspace{-0.06 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.04 in}f\right)} \; \leq \; \operatorname{Prob}_{\mathcal{O}}\left[A^{\mathcal{P}}(n,z^{\mathcal{O}}(n))\right] \;\;\;$.

For n such that $\;\;\; 1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right) \; < \; \operatorname{Prob}_{\mathcal{O}}\left[A^{\mathcal{O}}(n,z^{\mathcal{O}}(n))\right] \;\;\;$:

In particular, there exists $\big[$an oracle-circuit $C$ of size at most j+n$^{\hspace{.03 in}j}\big]$ and

$\big[$an assignment of length at most f$\big]$ such that with that input and presampling,

$A$'s probability of outputting $1$ is greater than $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{2+j}\right)\hspace{-0.04 in}\right)$.

Oracle-circuits of size at most j+n$^{\hspace{.03 in}j}$ can be represented with poly(n) bits, so for p is bounded

above by a polynomial in n, which means f is also bounded above by a polynomial in n.

By construction of $A$, that means there are oracle-circuits of size at most j+n$^{\hspace{.03 in}j}$ and a

polynomial-length assignment such that when run with that presampling, the circuits' probability of finding a solution is greater than $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{2+j}\right)\hspace{-0.04 in}\right)$.  Since such circuits cannot make queries longer than j+n$^{\hspace{.03 in}j}$ bits, presampled inputs longer than that can be ignored, so such presampling can be efficiently-and-perfectly simulated with a random oracle and poly(n) hard-coded bits.  That means there are polynomial-size oracle circuits such that with a standard random oracle, the circuits' probability of finding a solution is greater than $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{2+j}\right)\hspace{-0.04 in}\right)$.  Such a random oracle can in turn be efficiently-and-perfectly simulated with just ordinary random bits, so there are polynomial-size probabilistic non-oracle circuits whose probability of finding a solution is greater than $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{2+j}\right)\hspace{-0.04 in}\right)$.  In turn, by hard-coding optical randomness, there are polynomial-size deterministic (non-oracle) circuits whose probability (over the choice of x) of finding a solution is greater than $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(2\hspace{-0.06 in}\cdot \hspace{-0.06 in}\left(\hspace{-0.02 in}n^{2+j}\right)\hspace{-0.04 in}\right)$.

As shown earlier in this answer, there are infinitely many n such that $1\hspace{-0.04 in}\big/\hspace{-0.07 in}\left(\hspace{-0.02 in}n^{2+j}\hspace{-0.02 in}\right) \; < \; \operatorname{Prob}_{\mathcal{O}}\left[A^{\mathcal{O}}(n,z^{\mathcal{O}}(n))\right] \;\;\;$, $\;\;\;$ so there is a polynomial such that

the sequence whose n-th entry is the lexicographically least

[circuit C of size bounded above by that polynomial] which maximizes $\operatorname{Pr}_{x\in \{0,1\}^n}\hspace{-0.04 in}\left[\hspace{.02 in}R\hspace{-0.04 in}\left(x,\hspace{-0.04 in}C(x)\hspace{-0.03 in}\right)\hspace{-0.02 in}\right]$

is a P/poly algorithm whose probability (over the choice of x) of finding a solution is non-negligible.

Therefore the implication's in my question's body always hold.

To get the same implication for other polynomial-length games, just

change this proof's $A$ to make it have the input oracle-circuits play the game.


Check the paper Wilfried, Imrich; Iztok, Peterin, Recognizing Cartesian products in linear time. Discrete Math., 307, 3-5, Page(s): 472--483, 2007. I think that Imrich has more papers for other products.


Is there a version of MIP=NEXP with relatively efficient provers?

Yes.    This paper constructs "a one-round succinct MIP of knowledge, where each prover runs in time $t\cdot \operatorname{polylog}(t)$ and space $s\cdot \operatorname{polylog}(t)$ and the verifier runs in time"  $\operatorname{length}(m) \cdot \operatorname{polylog}(t)$ .


Can we count in depth $\frac{\lg n}{\lg \lg n}$?

Consider a fanin 2 circuit of $C$ depth $O(\log n)$. Divide the layers of $C$ into $O(\log n/\log\log n)$ blocks each of $\log\log n$ consecutive layers. We now wish to replace each block by a depth 2 circuit. Namely, each gate in the last layer of a block depends on at most $2^{\log\log n} = \log n$ gates of the last layer in the block below. We can thus replace each gate in the last layer by a DNF of polynomial size with inputs being the gates in the last layer of the block below. Doing this for all gates in the last layers for all blocks and connecting these should yield the desired circuit.

Let me note this is essentially the best one can obtain: the switching lemma allows for lower bounds all the way to depth $\log n/ \log\log n$.


What is the Relationship between QMA and AM?

No relationship is known to hold between QMA and AM, and it is reasonable to conjecture they are incomparable.

If QMA were proved to be contained in AM, it would be an absolutely enormous result in quantum complexity.  Of course it would imply that BQP is in PH, which itself would be huge, but it would go beyond that -- it would surely require major revelations about the structure of quantum algorithms and quantum certificates.

Having said that, the evidence against is not very convincing.  An oracle relative to which QMA is not contained in AM would help, and it seems like such a result may not be far off -- but we don't even have this yet.

A proof of the reverse containment, AM in QMA, would also be huge.  At least here we have an oracle relative to which AM is not contained in QMA (and in fact is not even contained in PP).


Generating hard satisfiability problems with given constraint graph

It sounds like what you want are universal factor graphs. Such graphs exist for every NP-hard boolean CSP and in many cases are optimally inapproximable.


VC dimension of intersection of half-spaces

It has been recently shown by Csikos, Kupavskii, Mustafa
in "Optimal Bounds on the VC-dimension" that the VC dimension of $k$-fold unions (or intersections or XORs) of half-spaces in $R^d$ behaves as
$$ \Theta(dk\log k).$$


For your second question, the number of bits is $O(n^2 \log n)$ (i.e. $O(n\log n)$ per coefficient) and there are examples where it is $\Omega(n^2\log n)$, i.e. the bound is tight. See Corollary 26 here.

The ideas are standard, and anyone who has seen an analysis of the ellipsoid algorithm will be familiar with this. Say you have a facet in the hyperplane spanned by vertices $v_1, \ldots v_{n-1}$. If the hyperplane is through the origin, it is defined by $a^T x = 0$ for the vector $a$ satisfying $V^Ta = 0$ where $V$ is the matrix containing $v_1, \ldots, v_{n-1}$ as columns. Using the fact that $V$ is a 0-1 matrix, you can bound the coefficients of $a$ using Cramer's rule and the Hadamard bound. If the hyperplane is not through the origin the argument is the same but the defining  equality is $a^T x = 1$ and the system of equalities you need to solve is $V^Ta = e$ where $e$ is the all-ones vector.

The lower bound is based on observing that everything above is tight and constructing a matrix $V$ such that removing any row from $V$ gives a matrix with a huge determinant. This construction is the one thing about your question which is research level, see the book or this paper by Alon and Vu


Using Kolmogorov complexity to establish proof complexity lower bounds?

Arvind, Köbler, Mundhenk, and Torán introduced the notion of time-bounded nondeterministic instance complexity. Based on a quick reading, It seems they use Kolmogorov complexity measure that depends on the size of shortest nondeterministic TM. They were able to prove the existence of hard to prove Tautologies under a notion of hardness based on nondeterministic instance complexity.

Vikraman Arvind, Johannes Köbler, Martin Mundhenk, Jacobo Torán,
Nondeterministic Instance Complexity and Hard-to-Prove Tautologies,


Chomsky normal form method: CYK parser performance implications?

While the obvious answer is that the fundamental complexity can't change, there may be better or worse algorithms for parsing the strings you're actually going to encounter. However, it seems like the issue is less the relative frequency of individual grammar productions (the A's, B's, and C's in the question) and more an issue of the unused, dead end parses that one binarization versus another may produce.

With a bit of searching I found Better Binarization for the CKY Parsing (Song, Ding, and Lin, EMNLP 2008), which seems to definitively conclude that you can pick a "better" or "worse" binarization relative to the strings you actually expect to have to parse. Their name for the "dead end parses" that one would hope to minimize in practice seems to be incomplete constituents, and there is a good example on the first page.


Introductory resources on Computational Learning Theory

Kearns and Vazirani is maybe a bit old, but good introduction.


Is it necessary to call matrix multiplication $n$ times to find a claw

I think that we can do slightly better than $O(n^{1+\omega})$ for dense graphs, by using rectangular matrix multiplication. A similar idea was used by Eisenbrand and Grandoni ("On the complexity of fixed parameter clique and dominating set",
Theoretical Computer Science Volume 326(2004) 57–67) for 4-clique detection.

Let $G=(V,E)$ be the graph in which we want to detect the existence of a claw.
Let $A$ be the set of (ordered) pairs of vertices in $V$. Consider the following Boolean matrix $M$ of size $|V|\times |A|$: each row is indexed by some
$u\in V$, each column is indexed by some $(v,w)\in A$, and the corresponding entry
is one if and only if $\{u,v\}\in E$, $\{v,w\}\in E$ and $\{u,w\}\notin E$.
Consider the Boolean matrix product of $M$ and its transpose $M^T$. The graph $G$ has a claw if and only if there exists $\{u,v\}\notin E$
such that the entry of $MM^T$ in the row indexed by $u$ and the column indexed by $v$ is one.

The complexity of this algorithm is essentially the complexity of computing the Boolean product of an $n\times n^2$ matrix by a $n^2\times n$ matrix, where $n$ denotes the number of vertices in the graph.
It is known that such a matrix product can be computed in time $O(n^{3.3})$, which is better than $O(n^{1+\omega})$ for the best known upper bound on $\omega$.
Of course,  if $\omega=2$ (as conjectured) then the two approaches give the same complexity $O(n^3)$.


Hitting set of pairwise intersecting families

The answer is yes - the problem is still NP-Complete. for every set $S_i$ create a fake elements $e_i', e_i''$ and create a new sets $S_i' = S_i \cup \{ e_i'\}$ and $S_i'' = S_i \cup \{e_i''\}$. It is easy to verify that  any hitting set of the old system is a hitting set of the new system. Furthermore, except for the fake elements, every element now hit at least three sets.

Next, for every pair of sets in the new system (lets call them $T_i$ and $T_j$ to avoid confusion), create a fake element $x_{ij}$ and add it to both $T_i$ and $T_j$. Clearly, in the resulting set system all sets pairwise intersect, but the original optimal hitting set is still the optimal hitting set for this newest system.

Without any further restrictions the problem looks as hard as the original problem.

BTW, proving that indeed the optimal solution would not use any of the fake elements is not trivial. First, we can assume that a given hitting set for the new system does not include any $e_i'$ or $e_i''$, since otherwise we can move the elements to the original elements of the sets, and get a hitting set of similar size. It is slightly more subtle to see why the elements $x_{ij}$ are not in the optimal hitting set. Since it is tedious I would just leave a hint: build a graph connecting two sets $S_i$ and $S_j$ in the original system if $x_{ij}$ connects two sets that are derived from these sets. Argue that this graph in the minimal hitting set must be $3$ regular, and as such the number of edges in it strictly exceeds the number of sets present as vertices. As such, one can find a smaller hitting set for these sets.


Lower Bounds on Running time of Graph Algorithms

In the PRAM model without bit operations, fairly strong lower bounds are known. For example, in this model, one cannot solve min-cut in $O(\sqrt{n})$ time on $2^{O(\sqrt{n})}$ processors [1].

Despite being a restricted model, it is strong enough to compute the determinant efficiently, and includes most standard algorithms for poly-time combinatorial optimization problems. See here, here, or the original paper for more details.

[1] Mulmuley, K. Lower Bounds in a Parallel Model without Bit Operations. SIAM J. Comput., 28(4), 1460–1509, 1999. (from author's webpage without paywall)


Is it possible to test if a computable number is rational or integer?

It is easy to get confused about what it means to "represent" or "implement" a real number. In fact, we are witnessing a discussion in the comments where the representation is contentious. So let me address this first.

How do we know that an implementation is correct?

The theory which explains how to represent things in a computer is realizability. The basic idea is that, given a set $X$, we pick a datatype $\tau$ and to every $x \in X$ a set of values of type $\tau$ which realize it. We write $v \vdash x \in X$ when $v$ is a value that realizes $x$. For example (I shall use Haskell for no good reason), a sensible implementation of $\mathbb{N}$ might be the datatype Integer where $v \vdash k \in \mathbb{N}$ when $v$ evaluates to the numeral $\overline{k}$ (thus in particular -42 does not represent a natural number, and neither does a diverging program). But some joker could walk by and suggest that we use Bool to represent natural numbers with $\mathtt{True} \vdash 42 \in \mathbb{N}$ and $\mathtt{False} \vdash n \in \mathbb{N}$ for $n \neq 42$. Why is this incorrect? We need a criterion.

In the case of "joker numbers" the easy observation is that addition cannot be implemented. Suppose I tell you I have two numbers, both represented by $\mathtt{False}$. Can you give a realizer for their sum? Well, that depends on whether the sum is 42, but you cannot tell. Since addition is an "essential part of what natural numbers are", this is unacceptable. In other words, implementation is not about sets, but about structures, i.e., we have to represent sets in such a way that it is possible to also implement the relevant structure. Let me stress this:

  We implement structures, not bare sets. Therefore, we have to be able to implement the entire structure, together with operations and all the axioms, in order for the implementation to be correct.

If you do not abide by this principle, then you have to suggest an alternative mathematical criterion of correctness. I do not know of one.

Example: representation of natural numbers

For natural numbers the relevant structure is described by Peano axioms, and the crucial axiom that has to be implemented is induction (but also $0$, successor, $+$ and $\times$). We can compute, using realizability, what the implementation of induction does. It turns out to be a map (where nat is the yet unknown datatype which represents natural numbers)

  induction : 'a -> (nat -> 'a -> 'a) -> 'nat -> 'a

satisfying induction x f zero = x and induction x f (succ n) = f n (induction x f n). All this comes out of realizability. We have a criterion: an implementation of natural numbers is correct when it allows an implementation of Peano axioms. A similar result would be obtained if we used the characterization of numbers as the initial algebra for the functor $X \mapsto 1 + X$.

Correct implementation of real numbers

Let us turn attention to the real numbers and the question at hand. The first question to ask is "what is the relevant structure of the real numbers?" The answer is: Archimedean Cauchy complete ordered field. This is the established meaning of "real numbers". You do not get to change it, it has been fixed by others for you (in our case the alternative Dedekind reals turn out to be isomorphic to the Cauchy reals, which we are considering here.) You cannot take away any part of it, you are not allowed to say "I do not care about implementing addition", or "I do not care about the order". If you do that, you must not call it "real numbers", but something like "real numbers where we forget the linear order".

I am not going to go into all the details, but let me just explain how the various parts of the structure give various operations on reals:

the Archimedean axiom is about computing rational approximations of reals
the field structure gives the usual arithmetical operations
the linear order gives us a semidecidable procedure for testing $x < y$
the Cauchy completeness gives us a function lim : (nat -> real) -> real which takes a (representation of) rapid Cauchy sequence and returns its limit. (A sequence $(x_n)_n$ is rapid if $|x_n - x_m| \leq 2^{\min(n,m)}$ for all $m, n$.)

What we do not get is a test function for equality. There is nothing in the axioms for reals which asks that $=$ be decidable. (In contrast, the Peano axioms imply that the natural numbers are decidable, and you can prove that by implementing eq : nat -> nat -> Bool using only induction as a fun exercise).

It is a fact that the usual decimal representation of reals that humanity uses is bad because with it we cannot even implement addition. Floating point with infinite mantissa fails as well (exercise: why?). What works, however is signed digit representation, i.e., one in which we allow negative digits as well as positive ones. Or we could use sequences of rationals which satisfy the rapid Cauchy test, as stated above.

The Tsuyoshi representation also implements something, but not $\mathbb{R}$

Let us consider the following representation of reals: a real $x$ is represented by a pair $(q,b)$ where $(q_n)_n$ is a rapid Cauchy sequence converging to $x$ and $b$ is a Boolean indicating whether $x$ is an integer. For this to be a representation of the reals, we would have to implement addition, but as it turns out we cannot compute the Boolean flags. So this is not a representation of the reals. But it still does represent something, namely the subset of the reals $\mathbb{Z} \cup (\mathbb{R} \setminus \mathbb{Z})$. Indeed, according to the realizability interpretation a union is implemented with a flag indicating which part of the union we are in. By the way, $\mathbb{Z} \cup (\mathbb{R} \setminus \mathbb{Z})$ is a not equal to $\mathbb{R}$, unless you believe in excluded middle, which cannot be implemented and is therefore quite irrelevant for this discussion. We are of forced by computers to do things intuitionistically.

We cannot test whether a real is an integer

Finally, let me answer the question that was asked. We now know that an acceptable representation of the reals is one by rapid Cauchy sequences of rationals. (An important theorem states that any two representations of reals which are acceptable are actually computably isomorphic.)

Theorem: Testing whether a real is an integer is not decidable.

Proof. Suppose we could test whether a real is an integer (of course, the real is realized by a rapid Cauchy sequence). The idea, which will allow you to prove a much more general theorem if you want, is to construct a rapid Cauchy sequence $(x_n)_n$ of non-integers which converges to an integer. This is easy, just take $x_n = 2^{-n}$. Next, solve the Halting problem as follows. Given a Turing machine $T$, define a new sequence $(y_n)_n$ by
$$y_n = \begin{cases}
x_n & \text{if $T$ has not stopped within $n$ steps}\\
x_m & \text{if $T$ stopped in step $m$ and $m \leq n$}
\end{cases}$$
That is, the new sequence looks like the sequence $(x_n)_n$ as long as $T$ runs, but then it gets "stuck" at $x_m$ if $T$ halts in step $m$. Very importantly, the new sequence is also a rapid Cauchy sequence (and we can prove this without knowing whether $T$ halts). Therefore, we can compute its limit $z = \lim_n y_n$, because our representation of reals is correct. Test whether $z$ is an integer. If it is, then it must be $0$ and this only happens if $T$ runs forever. Otherwise, $z$ is not an integer, so $T$ must have stopped. QED.

Exercise: adapt the above proof to show that we cannot test for rational numbers. Then adapt it to show we cannot test for anything non-trivial (this is a bit harder).

Sometimes people get confused about all this testing business. They think we have proved that we can never test whether a real is an integer. But surely, 42 is a real and we can tell whether it is an integer. In fact, any particular real we come up with, $\sin 11$, $88 \ln 89$, $e^{\pi \sqrt{163}}$, etc., we can perfectly well tell whether they are integers. Precisely, we can tell because we have extra information: these reals are not given to us as sequences, but rather as symbolic expressions from which we can compute the Tsuyoshi bit. As soon as the only information we have about the real is a sequence of rational approximations converging to it (and I do not mean a symbolic expression describing the sequence, but a black box which outputs the $n$-th term on input $n$) then we will be just as helpless as machines.

The moral of the story

It makes no sense to talk about implementation of a set unless we know what sort of operations we want to perform on it.


I think (2) is called the uniform sparsest cut. The term non-uniform is used for the version where each pair ij of vertices has a separate demand d(ij) and the cut sparsity is E(S,V-S)/d(S,V-S) where d(S,V-S) is the demand between S and V-S.


Has this online problem been studied before ?

While I'm still not entirely sure what you're looking for, you might try reading Avrim Blum's talk on Online Learning and Prediction, and that might help you focus on areas of interest.


Automated theorem proving via unsupervised approaches

Clarification on terminology

The theorem proving community does not use the terms supervised and unsupervised. They use the terms interactive theorem proving or automated theorem proving. If you give a conjecture to the prover and it always comes back with a yes or no answer, such a prover is a decision procedure for a logical theory or simply called a decision procedure.

Proving statements of an infinite nature

The intuition that a theorem that involves an infinite number of cases will be difficult for a machine is misleading. Consider the statement below.

  The sum of two even numbers is an even number.

If you were do prove this by enumerating even numbers, there are infinitely many cases to consider. This statement is expressible in Presburger arithmetic. Presburger arithmetic is the first-order theory of the Natural numbers with the constants zero, one, addition, and equality.  Presburger in his 1929 Masters thesis showed this theory to be decidable. There are other facts of an 'infinite' nature that can be expressed in Presburger arithmetic and proved algorithmically.

Fully Automatic Theorem Proving

In asking for a machine that works with no assistance, you are asking for a decision procedure. It does not make much mathematical sense to ask for a decision procedure for one conjecture. If the conjecture is either true or false, there is a a trivial decision procedure. What we do in practice is try to find a logic that can express a conjecture we care about and try to prove the logic is decidable.

There are many many logical theories that are known to be decidable. Presburger arithmetic is a standard example. Another famous example is the first-order theory of real closed fields. The axiomatization provided by Tarski and his collaborators is sufficient to express statements of Euclidean geometry without measurement of angles or trignometric functions. This theory is decidable though the complexity is non-elementary.

Observe again that the intuition that complexity of proving a statement depends on the cardinality of the underlying domain is quite misleading. The intuition that the complexity of automatically proving a statement corresponds with how late in our education we meet that idea is also misleading.

The theory of the natural numbers with addition and multiplication is undecidable. The first order theory of real-closed fields is decidable but the proof is quite complex. The first-order theory of algebraically closed fields, which includes facts about complex numbers is also decidable. The proof for algebraically closed fields takes one or two pages in logic textbooks.

To summarise, you are asking about decision procedures for logical theories. There are many of them.

Interest

Success of a tool and interest of the theorems are highly subjective. The value of a theorem changes over time. Theorems proved at a certain time are forgotten and rediscovered a few decades later when they are celebrated by the community. It is easy to claim a theorem significant in retrospect and put it in a textbook, but it is not easy to recognise the significance of a theorem when it is proved. There is also the matter of relevance. There is much in a model theory text book I find boring and much in an automated deduction book that a model theorist would find boring, even though we both work in the field of logic.

There are decision procedures that can prove statements in textbooks. Tarski's decision procedure can prove the statements in Euclid's Elements. There are some statements in elementary number theory and linear algebra that decision procedures can prove.

The company TheoryMine sells theorems. (Yes, you can now proudly go to a medieval market and barter two theorems about list reversal for a kilo of unwashed potatoes.) The techniques they use to identify interesting theorems may answer your question.

Success

There are many ways to define success of a theorem prover. If you're asking whether a fully automatic theorem prover has ever, entirely by itself, proved a statement that mathematicians wanted to prove, I believe there might be stray examples, but they are not considered major successes.

Asking if a piece of technology can achieve the same things a human being finds interesting misses the point. It's interesting for a human being to hike up a mountain but trivial for a helicopter.

The major success of automated theorem provers is proving theorems about machines. Reasoning about the correctness of a cache coherence protocol, a floating point multiplication algorithm, a device driver are all highly non-trivial problems of a scale and intricacy that our limited monkey brains cannot deal with.

There is a theorem prover in the production flow of an Intel chip. There is a theorem prover shipping with Windows 7 and Windows 8 device driver kits. These theorem provers and the theorems they prove save more money and affect the daily lives of more people than most of our manually derived proofs ever will. That reeks of success to me.

On The Capabilities of Theorem Provers

This is in response to a question about whether there is an automatically generated proof of the infinitude of the primes (automatic, not computer assisted).

I am not aware of such a proof. However, one should ask what the consequences of such a proof are. If a human being can prove this statement, I think we can conclude they know something about numbers and about proofs. The consequences of an automatic proof would be very significant. The automatic procedure would also be able to solve open problems in mathematics. The problem is that difficulty and capability are very different for human beings and for machines.

To summarise, we have absolutely no illusions about what can be proved completely automatically. The goal of the field is not to replace or compete with human mathematicians. It is not surprising that a machine cannot prove what a human being can prove. It is insightful to understand that the consequences of a human being proving something are quite different from a machine automatically proving something.


Is there any problem in $\mathsf{\Sigma^P_2}$ which is solvable in bounded tree width graphs?

I think 2-clique-coloring [GT19 in Schaefer and Umans] is an example. The question is whether the given graph can be (improperly) 2-colored in such a way that none of its maximal cliques are monochromatic. For graphs of bounded treewidth, each maximal clique should occur within a single bag of the tree decomposition, so it should work to use the standard dynamic programming approach in which the states of the dynamic program are 2-colorings of the bag that correctly color all maximal cliques within the bag and are consistent with good states of the child bags.


Does Standard ML validate (CBV) eta equivalence?

@xuq01's guess is (extremely surprisingly!) wrong. The CBV eta rule described in the question is sound in Standard ML: the value v is contextually equivalent to fn x => v x.

There are two caveats to this.

First, in specific implementations this equivalence might not be sound: in SML/NJ, you could use Unsafe.cast to detect physical equality of function values. However, unsafe features are not part of the standard.
Second, eta with functions and sums interacts in a slightly subtle way, due to clausal definitions and incomplete pattern matching. In particular, the definitions:

fun f (SOME x) (SOME y) = x + y

and

val g = fn (SOME x) => (fn (SOME y) => x + y)

are not contextually equivalent. This is because the call f NONE will return a function, and g NONE will raise an error.

- f NONE;
val it = fn : int option -> int

- g NONE;
uncaught exception Match [nonexhaustive match failure]
raised at: stdIn:2.32

The reason this happens is operationally obvious, and of course a call-by-push-value/polarization setup makes this choice explicable. But if you really want to seriously understand clausal definitions, you are led to the idea that clausal definitions should be primary, and the usual term formers should be derived notions. See Abel, Pientka, Thibodeau and Setzer's Copatterns: programming infinite structures by observations for an example of a polarized calculus in this style. (See also Paul Levy's Jumbo Lambda-Calculus, for another calculus based on this observation.)


What are some techniques for "balancing" a tree beside heavy-light and centroid decomposition?

The paper "Algorithmic Meta Theorems for Circuit Classes of Constant and Logarithmic Depth" (Elberfeld, Jacobi, Tantau) gives a nice balanced tree decomposition based on tree contraction in $TC^0$:

https://eccc.weizmann.ac.il/report/2011/128/

Another nice $TC^0$-decomposition is based on so-called TSLPs in the paper "A Universal Tree Balancing Theorem" (Ganardi, Lohrey):

https://arxiv.org/pdf/1704.08705.pdf


What can we prove with infinite graphs that we cannot prove without them?

Here's an example from distributed computing:

1 Background

1.1 Asynchronous Shared Memory Model

Let's consider a collection of distributed nodes that communicate using
shared memory variables. There is an adversary that controls when a node take steps
and when to deliver messages. The computation is asynchronous, i.e., the
adversary can delay the steps of nodes for any (finite) amount of time.
You can think of a step of a node as a state transition of its local
automaton (according to the algorithm) where the next state is determined
by the current state and the observations of the node since the last step.

1.2 Safety and Liveness

When formally reasoning about the properties of an asynchronous algorithm,
we distinguish between safety and liveness properties. Informally, a
safety property can be interpreted as a guarantee that something "bad"
never happens. (E.g., for mutual exclusion, a safety property would be
that no two nodes enter the critical section  simultaneously.) Liveness,
on the other hand, can be interpreted as "something good will eventually
happen", e.g.: every node eventually terminates.

To formalize safety, we consider the infinite set ${M}$ of all possible
executions of all possible algorithms, taking into account all possible
choices of the adversary. An execution is an infinite sequence of steps.  We can define a metric on $M$ by taking the distance between two distinct
runs $\alpha,\beta \in M$ to be $2^{-n}$ where $n$ is the first index where $\alpha$ and $\beta$ differ.

A safety property $S$ corresponds to some nonempty set $P\subseteq M$ that
is closed in the sense that the limit of an infinite
sequence of runs in $P$ cannot be in $M\setminus P$. So once we know that some property is a safety property, it is sufficient to show that this property holds on finite prefixes.

Applying Koenig's Infinity Lemma

It's not always straightforward to see whether a specific property is a
safety property: Consider the implementation of read/write atomic objects
on top of basic shared memory variables. Such an implementation should handle requests and their responses in a way that makes them look as if they happen at some instant in time and don't violate their order of invocation. (Due to the asynchronous operation, the actual duration between request and response might be nonzero.) Atomicity is also known as Linearizability. Section 13.1 of [A] gives a proof that Atomicity is a safety property. The proof uses Koenig's lemma to show that the limit of any infinite sequence of executions (each of which satisfies Atomicity) also satisfies Atomicity.

[A] N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.


How do you go from insights to formal solutions?

Transforming intuition into formal argument is difficult, and the degree to which it is viewed as necessary is sociological, and varies by community. In general, arguments tend to be less formal in AI conferences, reasonably formal in the "Theory A" community, and extremely formal (i.e. machine verifiable) in parts of the programming languages "Theory B" community.

Probably the best way to develop this skill is to take rigorous courses that require formal argument on problem sets. You can also just read papers in the community that you would like to publish in, but you have to make sure to actually read the arguments carefully for this to be helpful. i.e. it is easy to read a paper and feel that you understand it, but be unable to reproduce key parts of the argument. A good way to do this is to plan to actually present the paper to a group of friends. If you actually have to present the arguments on a board and answer questions, you will be able to force yourself to really understand.

Do this a few times and you should be able to construct formal arguments of your own.


About switching from a computer scientist to a mathematician

Theoretical computer scientists are already mathematicians.  So you don't need to do anything!

Your later comment suggests that you're really asking about changing from one area of mathematics (like complexity theory) to another (like functional analysis).  The only way to do it is to just do it.  You want to be an analyst?  Great!  Just start doing analysis!  Read analysis books and papers, solve analysis problems, talk to lots of analyst faculty and students, attend analysis seminars, go to analysis conferences, ask analysis questions on MathOverflow, and so on.  Act like an analyst long enough (and well enough) and you'll become one.

In that respect, becoming a functional analyst is not so different from becoming anything else.  Want to be a programmer?  Program!  Want to be a writer?  Write!  Want to be a painter?  Paint!  Want to be a functional analyst?  Analyze functions!  (Meanwhile, don't forget to earn enough money to eat, and do not blow off the stupid administrative hurdles.)

And yes, lots of people successfully change fields/careers.  For example, Joan Birman started her academic career in physics, worked for several years as a systems analyst in the aircraft industry, spent several more years at home raising kids, went back to grad school in mathematics in her 40s, and became one of the most influential researchers in modern low-dimensional topology and geometric group theory.  For other examples, see these questions on MathOverflow.

One last suggestion: You might find the transition somewhat smoother (possibly even real-analytic) if you drop your prejudices about "pure" versus "applied" mathematics.  Forget about the labels; just do the work.


Quantum complexity of maximum inner product search

I think the quantum complexity is right for $l=1$, if a quantum oracle $O$ that can compute the inner product of any two row vectors from $X$ and $Y$, namely, $O: |i\rangle|j\rangle|0\rangle \rightarrow |i\rangle|j\rangle|X_i\cdot X_j\rangle$, is provided. Computing the inner product of two $k$-length vectors requires time $\mathcal{O}(k)$. Based on this oracle, we can use the quantum algorithm for finding minimun to find maximum and the oracle complexity will scales as $\mathcal{O}(\sqrt{mn})$. Then the total time complexity will be $\mathcal{O}(k\sqrt{mn})$.

The above algorithm can be utilized to find $l$ largest entries of $XY^{T}$ in a successive manner. For example, finding the second largest entry is equivalent to finding the largest entry of the rest entries when we 'take' the true largest one away. Therefore, i think the quantum complexity for finding $l$ largest entries will be $\mathcal{O}(lk\sqrt{mn})$.


Online version of All pair shortest path when path weights are updated

I think adding the keywords decremental/incremental might help you find the relevant papers.

See e.g.
Camil Demetrescu, Giuseppe F. Italiano: Decremental All-Pairs Shortest Paths. Encyclopedia of Algorithms 2008 for an overview, Camil Demetrescu, Giuseppe F. Italiano: Fully dynamic all pairs shortest paths with real edge weights. J. Comput. Syst. Sci. 72(5): 813-837 (2006), and Camil Demetrescu, Giuseppe F. Italiano: A new approach to dynamic all pairs shortest paths. J. ACM 51(6): 968-992 (2004)

Approximate versions have been considered as well; the most recent result I know of is Monika Henzinger, Sebastian Krinninger, Danupon Nanongkai: Dynamic Approximate All-Pairs Shortest Paths: Breaking the O(mn) Barrier and Derandomization, FOCS 2013.
Table 1 in their paper has an overview of results.


In Definition 2.1 of Contextual Petri Nets, Asymmetric Event Structures, and Processes, Baldan, Corradini and Montanari are working in the setting of prime event structures, which consist of a set of events $E$ along with binary relations $\#$ and $\le$ on $E$, known as the conflict and causality relations, respectively. This is the close to what is going on in your your setting.

In this context, they state that the relation $\#$ is hereditary with respects to $\le$ whenever for all $e_0,e_1,e_2\in E$, if $e_0\#e_1$ and $e_1\le e_2$, then $e_0\#e_2$.

It does not make sense to say that a relation is hereditary on its own; it is always taken with respect to another relation.

In general, saying that a relation is the least hereditary relation is not equivalent to saying that it is the least hereditary, symmetry, irreflexive relation, as the definition of hereditary does not imply that the relation is symmetric.

In the specific case you mention, it does seem to be the case – after going into the details of the paper a little more – that one need not specify that the relation is symmetric or irreflexive, as these come for free from the context. Well spotted!!


Circuit Complexity Charaterization for DLogTime and NLogTime

I think it is far more interesting that the circuit complexity classes used by CS complexity theory make different predictions and use different metrics than those in the VLSI community.  From The VLSI complexity of Boolean functions:

  It is well-known that all Boolean functions of $n$ variables can be computed by a logic circuit with $O(2^n/n)$ gates (Lupanov's theorem) and that there exist Boolean functions of n variables which require logic circuits of this size (Shannon's theorem). We present corresponding results for Boolean functions computed by VLSI circuits, using Thompson's model of a VLSI chip. We prove that all Boolean functions of $n$ variables can be computed by a VLSI circuit of $O(2^n)$ area and period 1, and we prove that there exist Boolean functions of $n$ variables for which every (convex) VLSI chip must have $\Omega(2^n)$ area.

Interestingly, VLSI circuit complexity has a tendency to treat depth as "irrelevant" as there is one and only one "depth" that matters: the critical path.  For most practical purposes, an arbitrarily complex circuit can be treated as $O(1)$ with a latency of $n$.

In fact, I'm not even sure that the concept of $DLogTime$ / $NLogTime$ directly translates in to VLSI circuit complexity.  Even Shannons $2^n/n$ result does not readily translate: Shannons results is valid only for a boolean basis consisting of arity $\le2$ {AND, OR, NOT}.  This is not the only basis, and the number of "gates" needed drops dramatically as you allow more and more gate types.  The following are $area^2$ from a commercial VLSI standard cell library normalized to the size of a 2 input NAND gate:

        2    3    4    <- Arity
and    1.14 1.28 1.41
nand   1.00 1.14 1.28
or     1.14 1.41 1.41
nor    1.00 1.14 1.41
xor    1.62 2.44
xnor   1.62 2.44

buf    1.14
inv    0.80

aoi22  1.28
aoi222 1.62
aoi33  1.62
oai22  1.41
oai222 1.72
oai33  1.62

addf   2.64

Specifically, note the aoi / oai gates which are And Or Invert / Or And Invert consisting of arity sized first function feeding the second function, where the number of first function gates is equal to the number of times arity appears.  For example, aoi22 represents "Two 2 input AND gates feeding a NOR gate".

My point is: Taken separately, a oai222 function can be built using three 2 input OR gates and a 3 input NAND gate, for a total area of ~4.56, not including any area used for interconnect.  Yet this primitive can be realized in an area of just 1.72, which means a discrete manifestation of the same boolean function consumes 2.65 times more area.

Also note that the area for an $n$ input {AND, NAND, OR, NOR, XOR, XNOR} gate, where $n\ge2$, is much less than the area that it would take to build the same function using discrete 2 input gates.  Also note that while the area given for {XOR, XNOR} for this process is "large" relative to the other gates, there are other ways to build the same $n$ input gates using less area.

The propagation properties for the more complex primitives is also significantly better than what would be achieved using discrete gates.

Why is this important?  Because for me, at least, I've spent a simply enormous amount of time sifting through results from complexity theory that are built on a set of assumptions that has the effect of either rendering the result useless or wrong once the assumption is violated.  The following is from Steven Cooks $\mathcal{P}$ vs $\mathcal{NP}$:

  Thus to prove $\mathcal{P} \ne \mathcal{NP}$ it suffices to prove a super-polynomial lower bound on the size of any family of Boolean circuits solving some specific $\mathcal{NP}$-complete problem, such as 3-SAT. Back in 1949 Shannon proved that for almost all Boolean functions $f : \{0,1\}^n \to \{0,1\}$, any Boolean circuit computing $f$ requires at least $2^n/n$ gates. Unfortunately, his counting argument gives no clue as to how to prove lower bounds for problems in $\mathcal{NP}$.

I find Cooks reasoning curious.  Shannons result is valid for all $f : \{0,1\}^n \to \{0,1\}$, therefore if a $\mathcal{NP}$ problem can be described in $\{0,1\}^n$ bits, there must be a {AND, OR, NOT} basis circuit that can decide if it is satisfiable in ~$2^n/n$ gates (the actual paper gives a larger upper, but finite, bound for every possible function).  What this tells us is that anything that uses more than $n$ gates, where $n$ is the upper bound for the size of the $\mathcal{NP}$ problem, is using more gates than is required.  Using a larger, but complete, boolean basis only reduces the number of gates required.  Using a different circuit complexity model, i.e. VLSI, gives even "better" result bounds.  Curious.  But we know for a fact that any solution to a $\mathcal{NP}$ problem that uses more than ~$2^n/n$ "gates" (where gates is used loosely for steps / operations) is doing so in a sub-optimal fashion... and there's an infinite number of ways to find a solution in a sub-optimal fashion.

On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication shows that predicting circuit complexity using a OBDD model over-estimates the actual circuit complexity:

  Lower-bound results on Boolean-function complexity under two different models are discussed. The first is an abstraction of tradeoffs between chip area and speed in very-large-scale-integrated (VLSI) circuits. The second is the ordered binary decision diagram (OBDD) representation used as a data structure for symbolically representing and manipulating Boolean functions. The lower bounds demonstrate the fundamental limitations of VLSI as an implementation medium, and that of the OBDD as a data structure. It is shown that the same technique used to prove that any VLSI implementation of a single output Boolean function has area-time complexity $AT^2 = \Omega (n^2)$ also proves that any OBDD representation of the function has $\Omega(c^n)$ vertices for some $c<1$ but that the converse is not true. There are functions for which any OBDD representation is of exponential size, but there is a VLSI implementation of complexity $AT^2 = O(n^{1+c})$.

  An integer multiplier for word size $n$ with outputs numbered 0 (least significant) through $2n-1$ (most significant) is described. For the Boolean function representing either output $i-1$ or output $2n-i-1$, where $1\le i\le n$, the following lower bounds are proved: any VLSI implementation must have $AT^2 = \Omega(i^2)$ and any OBDD representation must have $\Omega(1.09^i)$ vertices.


My answer to the question is that I don't know of published work. However, I've recently been thinking a bit about formalizing what I believe is essentially your question, so I'll try to collect some thoughts in the following "extended comment", hoping that it will be interesting, useful, or spark productive discussion! (Maybe this is already well-known or studied, in which case I apologize.)
Consider the set of all languages on a fixed alphabet; call this the "universe". In analogy with a topology, we can define a sort of "computational space" as this universe together with a set of languages, i.e. a set of subsets of this universe. In particular $P$ is the set of languages decidable in polynomial time. I'll think of languages in $P$ as the analogues of open sets and polytime-computable functions (which will serve mainly as reductions) as the analogues of continuous functions.
Note that $P$ is closed under complement, finite union, and finite intersection, but not countable union or intersection (breaking the analogy).
Now in analogy with continuous functions, consider all polytime functions: functions $f: \Sigma^* \to \Sigma^*$ that are computable in polynomial time. You might also want to require that its input and output sizes are polynomially related (i.e. for some $p$, $|x| \leq p(|f(x)|)$). This choice could alter the sequel a little, so that's a caveat, but the whole discussion is sub-formal anyway.

We can see that the polytime functions satisfy the following property: $B \in P \implies f^{-1}(B) \in P$. We would like the following to be true: They are the only such "continuous" functions (note that output-size-messiness comes in when attempting to prove this converse). I don't know if it's true and it might even be equivalent to a very hard problem.

We can also see that a language $B$ is in NP if and only if it is the polytime image of a language in $P$, that is, there exists $A \in P$ and polytime $f$ with $f(A) = B$.
Sketch: If $A \in P$, then to decide the language $f(A)$ in nondeterministic polynomial time, given $y$, guess $x$ and accept iff $f(x)=y$. On the other hand, if $B$ is in NP, let $A = \{(x,w) : x \in B \text{ and $w$ is an NP certificate for $x$}\}$. $A$ is decidable in polynomial time and the polytime function $f$ that projects onto the first element of the pair satisfies $f(A) = B$.

Therefore, we can notice that $P = NP$ if and only if $P$ is closed under these polytime mappings, i.e. for all $A \in P$ and polytime $f$, $f(A) \in P$. The analogous statement in topology would be "all continuous mappings are open mappings".

We can see that an NP-complete set $B$ has the property that, for every $A \in P$, there exists a polytime $f$ with $f^{-1}(B) = A$. If $P \neq NP$, then an NP-intermediate set $C$ would therefore satisfy that there is some $A \in P$ with, for every polytime $f$, $f^{-1}(C) \neq A$; and also that it is not decidable in polynomial time, so there is no $A \in P$ and polytime $f$ with $f^{-1}(A) = C$.

There seem to be lots of sort-of interesting statements we can make, though their novelty/usefulness is probably dubious. For instance, I think something like this is true: "$P = NP$ if and only if every polytime mapping can be preimaged in polynomial time", (the analogy is that "every continuous function has a continuous inverse").
Similarly, you could probably translate lots of complexity statements into this framework but with again dubious utility. For instance, one-way functions (although I haven't thought about randomized algorithms...that could be quite interesting).
Final notes: I think the most interesting thing about this framework is that it seems not to relativize. One might of course think about other interesting complexity classes than $P$ and $NP$; one might also think of e.g. $DTIME(g(n))$ for a specific $g$; I'm not sure if that's interesting.


There is no sub-linear algorithm for it, assuming the array may have duplicates as in your example. The following shows that any algorithm must read all of $|A|$'s values.

Assume that there's sub linear algorithm $Alg$ that decides it.

Define an array $A$ by $A_k = k+1$.

Since $alg$ is sublinear, there has to be some cell of $A$ he didn't query. Denote such cell's index by $i$.

Define $B_k = \left\{
 \begin{array}{ll}
  k+1  & \mbox{if } k \neq i \\
  i & \mbox{if } k = i \\
 \end{array}
\right.$

Note since $Alg$ doesn't read cell $i$, it will answer the same for both $A$ and $B$, but obviously one of these answers is wrong..


These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called datasort refinements.

They were introduced by Tim Freeman and Frank Pfenning, in their 1991 PLDI paper, Refinement Types for ML.
Rowan Davies studied type inference for refinement types in his PhD thesis, Practical Refinement Type Checking. He also implemented it as an extension to SML, but I don't know if it is available online.
Joshua Dunfield studied how to combine datasort refinements with fancier lightweight type dependency in his thesis, A Unified System of Type Refinements. He also implemented it in his Stardust language, which is available online:

http://www.mpi-sws.org/~joshua/stardust/


Why not include private randomness in internal communication information definition?

I agree that the definition you suggest is more natural. However, this definition is equivalent to the definition without the private randomness, so I assume they omit the private randomness just to have a shorter notation.

To see the equivalence, observe that
\begin{eqnarray}
I(X; \Pi | Y, PR(Y) ) &=& I(X; \Pi, PR(Y) | Y ) - I(X; PR(Y) | Y ) \\
& = & I(X; \Pi, PR(Y) | Y ) \\
& = & I(X; \Pi | Y ) + I(X; PR(Y) | Y, \Pi ) \\
& = & I(X; \Pi | Y )
\end{eqnarray}
Here, the first and third equalities follow from the chain rule, the second equality follows since $X$ and $PR(Y)$ are independent even conditioned on $Y$, and the fourth equality follows $X$ and $PR(Y)$ are independent even conditioned on $Y$ and $\Pi$.

The last independence takes a bit of effort to verify, but it basically follows from the rectangle property of protocols (and one also needs to note that conditioning on $Y$ severs the possible dependence of $X$ and $PR(Y)$ given $\Pi$). A bit more specifically, observe that conditioned $\Pi$ and $Y$, the set of values of $X$ and $PR(Y)$ that are consistent with $\Pi$ and $Y$ form a rectangle. Since $X$ and $PR(Y)$ started as independent variables, conditioning them on being in this rectangle preserves their independence.


Who first proposed using $x^2+y^2 < 1$ Monte Carlo algorithm to calculate Pi?

The Monte-Carlo method is usually attributed to Metropolis and Ulam, the latter was a mathematician on the Manhattan project.

If my memory is good, Ulam published a paper where he computes pi using the algorithm.


Is there any time efficient way of achieving the result of FKS hashing lemma?

DGS prove a hashing lemma that bijectively hashes a sparse set to a set from a smaller universe (without involving a primality test). In particular see Lemma 3 in the paper that maps a set of size at most $(\log n)^{1/3}$ from the universe $[n]$ to a set  of size at most $v < \log{n}$ by using the hash function $((x \bmod{u})\bmod{v})$ where $u < n$.

I guess in your setting the set consists of elements from $n$-bit numbers and you can therefore plug in $2^n$ instead of $n$ in the DGS-lemma.


Is qsort linear when sorting only two values?

There is a large body of research on Quicksort for sorting multisets.
The talk Quicksort is optimal by Sedgewick gives a nice overview of this.
Basically with 3-way partitioning you get within a constant of the information theoretic minimum. The information theoretic minimum is: Suppose we are to sort $n$ keys, where there is only $m$ distinct keys, and the $i$th key occurs $n_i$ times. Then we need
$n \lg(n) - \sum_{i=1}^m n_i\lg n_i -n \lg e +O(\lg n)$ three way comparisons on the average. (See "Sorting multisets and vectors in-place", by Munro and Raman).


Describing a grammar and associated parser

if you don't count rembering the symbols of previous lines it's a regular language here's the regex as I see it (<char> is translated to [a-z])

[a-z]\s*,\s*([a-z]|None)\s*,\s*(R|L|P[a-z](R|L))\s*,\s*[a-z]\n

use capturing groups as necessary ;)


Graph transformation according to some utility function

I assume that the edge weights express how much the users interact to one another, rather than the amount of communication , i.e. the communication is always mutual and  not in risk of being just one-sided. This is more an issue of modeling and not of the problem itself.

The sets in general are not disjoint, as a cut would require them to be, unless you are referring to the subgraph of a certain person's friends (the adjacent vertices). In the social network graph, complex relations can be formed. For example, think of a triangle graph of 3 friends: You (A) might care for a friend B who also cares for your mutual friend C, however you ignore C. It is unclear in which subgraph C belongs. Experimenting with graphs allows you to find a lot of examples where the two sets are not disjoint.

Even if the subgraphs were disjoint and you wanted to know how communities, i.e.  groups of people that care for each other, appear in the graph, this is the min-k-cut problem , which is NP-complete, unless you know the number of communities (which in general you don't).

However, you can easily obtain the two subgraphs you want, by selecting a threshold and then on one graph include all edges (and their adjacent vertices) that pass that threshold, constructing the "who-cares_about-who"
 subgraph and in the other one include the edges that do not and also invert the weights, so that the bigger the weight, the higher the lack of interest between two friends. The problem with this approach is that deciding the value of the threshold is an optimization problem which seems to be reduced to the previous NP-complete problem. Still, you can use a number of techniques from statistics and experimental data to have a fixed threshold, perhaps associated with a level of confidence. Furthermore, you can use fuzzy logic so that the threshold is an interval instead of a fixed point, increasing the accuracy but risking false positives.


SERF-reducibility and subexponential algorithms

EDIT: As pointed out by Ryan in the comments, a problem may have a nonuniform algorithm with running time $O(2^{\epsilon n})$ for any constant $\epsilon > 0$ (the algorithm has access to $\epsilon$) but no uniform $2^{o(n)}$ time algorithm.

As a SERF reduction is a family of Turing reductions, one for each $\epsilon>0$, I conclude that they can only be used to obtain $O(2^{\epsilon n})$ time algorithms from $O(2^{\epsilon n})$ or $2^{o(n)}$ time algorithms.

The following Theorem is proved by Chen et al. [2009].

Theorem 2.4. Let $f(k)$ be a nondecreasing and unbounded function, and let $Q$ be a parameterized problem. Then the following statements are equivalent:
(1) $Q$ can be solved in time $O(2^{\delta f(k)}p(n))$ for any constant $\delta > 0$, where $p$ is a polynomial;
(2) $Q$ can be solved in time $2^{o(f(k))} q(n)$, where $q$ is a polynomial.

Taking $f(k)=n$ we obtain that a problem has a $O(2^{\epsilon n})$ time algorithm for every $\epsilon>0$ if and only if it has a $2^{o(n)}$ time algorithm.

It is mentioned in the paper by Chen et al. that this equivalence had been intuitively used before but that it was causing some confusion among researchers.


Does the Category of CPOs have omega^op limits?

Here's an attempt (please check!).

We have that $\bot_D = d$, where

$$
d_i = \bigsqcup^{D_i} \{\bot_i,f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),\ldots\}
$$

By construction (and monotonicity), the above is the supremum of an $\omega$-chain inside $D_i$, so $d_i$ is well defined.

It is an element of $D$ since, by continuity,

$$
\begin{array}{ll}
& f_i(d_{i+1}) \\
= & f_i(\bigsqcup^{D_{i+1}} \{\bot_{i+1},f_{i+1}(\bot_{i+2}),f_{i+1}(f_{i+2}(\bot_{i+3})),\ldots\}) \\
= & \bigsqcup^{D_{i}} \{f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\
= & \bigsqcup^{D_{i}} \{\bot_i, f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\
= & d_i
\end{array}
$$

To prove that $d$ is the bottom, we take any $x \in D$, and we observe

$$
\begin{array}{ll}
& d_i \sqsubseteq x_i \\
\Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq x_i \\
\Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq f_i \circ \cdots \circ f_k (x_{k+1})\\
\Leftarrow & \forall k\geq i.\ \bot_{k+1} \sqsubseteq x_{k+1}\\
\Leftarrow & {\sf true}
\end{array}
$$


This problem is PP-hard under Turing reductions when your weights are encoded in binary. The lower bound follows by a reduction from the $K$-th largest subset problem. Given a set $S\subseteq \{ s_1,\ldots,s_n \}\subseteq \mathbb{N}$ and $B, K\in \mathbb{N}$, this problem asks whether
\begin{align*}
\# \{ S'\subseteq S : \sum_{s\in S'} s \le B \} \ge K.
\end{align*}
It has recently been shown that this problem is PP-complete under polynomial-time Turing reductions. It's easily seen how to encode this problem into yours (and see Proposition 4 in here in case you need some inspiration).

If $k_1$ is given in unary then your problem is PP-complete. If $k_1$ is given in binary then your problem is in PEXP, I cannot say if it is PEXP-complete.

In general, you often see this kind of problems in the setting of quantitative verification of (stochastic) systems.


What's wrong with this proof that NP=Co-NP implies NP=PSPACE

A totally quantified boolean formula consists of an alternating sequence of quantifiers. This sequence is not of length 2, but arbitrarily long. That is the mistake you're making: an instance can be represented as a pair (P, phi) where phi is a propositional formula and L = (X_1, ..., X_k) is a partition of the set of variables occuring in phi, such that X_i are the variables in the i'th quantifier (which is an existential one if i is odd, and universal otherwise). You are assuming that this instance is equivalent to (L', phi), L' = (X_1', X_2') where X_1' is the union of the odd-indexed X_i, and X_2' is the union of the even-indexed X_i. Please verify for yourself that this is not necessarily true.


Does diagonalization captures the essence of class separation ?

Depends on how you formalize diagonalization. Kozen has a paper that shows any complexity class separation must be a diagonalization proof.


Easier and Harder instances of NP-complete problems?

If P=NP, then all NP-complete problems are equally difficult from the perspective of polynomial-time reductions.

On the other hand, if P!=NP, then we have ways to differentiate NP-complete problems, for example:

Approximable problems - NP-complete problems where we can find a polynomial-time algorithm that gives us almost the desired answer (within a constant factor).  For example, there is a trivial algorithm to produce a Vertex Cover within a factor of $2$ of optimal, although the optimal answer is NP-complete.
Somewhat approximable problems - NP-complete problems that can be approximated, but not within a constant factor.  The classic example is the set cover problem, which can be approximated within a fraction of roughly $ln n$ for $n$ sets, but cannot be approximated with a less than logarithmic fraction (unless P=NP).
Unapproximable problems - NP-complete problems for which (under accepted assumptions) no polynomial-time algorithm exists that approximates the solution within any polynomial factor.  An example is the max-clique problem.
Fixed-parameter tractable - problems that run in polynomial time if you fix one parameter.  The classic example again is vertex-cover, which can be computed in time $O(2^k n)$ for a vertex cover of size $k$ in a graph of size $n$.

In short, under accepted assumptions, there are varying difficulties of NP-complete problems.


There's also a recent work on low-rank semidefinite programming that, though not based directly on a quantum algorithm, still uses the same quantum-inspired techniques.


Writing a paper as a single author in 1st person singular

I am not a native English speaker, but I don't think this is important here. The appropriate thing is not what an English professor or a poet suggests, but what is standard in the particular field. And from my experience, "we" is the standard in theoretical computer science. As noted by usul in his comment, you can interpret the "we" as the author including the reader. I can think of several reasons why "we" is better than "I":

It sounds more natural and less egocentric.
A paper in theoretical computer science is not about your personal opinion, but you state and prove general facts. Replacing "we" with "I" in terms such as "we thus have" is therefore weird since what follows is generally true, not only for you.
Submissions are often anonymous. You don't want to reveal that the paper has been written by a single author in the submission (and you don't want to change "we" to "I" in the final version).

Edit: An exception are parts of the paper that are subjective, e.g., the acknowledgement section: I would like to thank András Salamon and Boaz Barak for pointing this out.


Chernoff-type inequality for random variable with 3 outcomes

You can get fairly good bounds by considering the random variable $Y_{ij}$ which is 1 if $X_i = j$ and zero otherwise (for $1 \le i \le n$ ranging over trials and $1 \le j \le 3$ ranging over categories). For any fixed $j$ the $Y_{ij}$ are independent and therefore $\sum_i Y_{ij}$ can be analyzed using Chernoff bounds. Then do a union bound over $j$.

If the above isn't enough I suggest that you look at the balls and bins model e.g. in Upfal and Mitzenmacher's textbook. That model is the same as yours except that some of your bins may be more likely than others to have balls land in them, right? There are some more sophisticated techniques involving Poisson approximations in that model that would likely be extendable to your setting with non-uniform bin probabilities.


Classes with oracles forcing the caller to immediately accept (or reject)?

The question is not entirely clear to me. However, concerning the example that is spelled out more precisely: if a language is recognizable by a poly-time machine with a SAT oracle which must accept whenever the oracle answers “yes”, it is in fact in NP. First, observe that regardless of the oracle answers, we can simulate in polynomial time the only possible run of the algorithm by pretending all answers are “no”. (In particular, we can compute the list of all oracle queries beforehand.) Then, the original algorithm accepts iff one of the oracle answers in the simulated run is actually “yes”, or the simulated algorithm accepts in the end. This is an NP property.

More generally, if we use an arbitrary oracle $A$ in the above scenario in place of SAT, a language can be computed in the indicated way iff it is poly-time dtt-reducible to $A$.


Algebraic formulation for packing problem

It is possible to prove the fixed-parameter tractability of various graph-theoretical problems (e.g., finding a path of length k or finding k disjoint triangles) using algebraic techniques by reducing the problem to questions about certain polynomials. See for example the following very readable paper by Ryan Williams:

http://arxiv.org/abs/0807.3026v3

and some other related papers:

http://www.cs.cmu.edu/~jkoutis/papers/MultilinearDetection.pdf

http://doi.ieeecomputersociety.org/10.1109/FOCS.2010.24

http://arxiv.org/abs/0912.2371

About your meta question: as the formulation of graph-theoretical problems is usually "combinatorial," it is not surprising to me that most of the natural approaches are "combinatorial" rather than "algebraic." The "algebraic" approaches work only if the problem has some unexpected connection with algebra, which is probably quite rare for natural "combinatorial" problems. In the above-mentioned papers, such a connection is discovered, allowing us to solve the problem using algebraic techniques. Interestingly, for these problems the algebraic algorithms are faster (have better bounds) than the combinatorial ones.


Complexity of iterative least squares regression

Linear regression

Yes.  For linear regression, you can do both updates in $O(1)$ time.

Recall that for ordinary least squares estimation, we estimate the parameter vector $\hat\beta$ using the equation

$$\hat{\beta} = (X^T X)^{-1} X^T y.$$

Here $X$ is a $n \times 2$ matrix and $y$ is a $n$-vector.  Adding a point amounts to adding a row to $X$ and $y$; deleting a point corresponds to deleting a row.

So, here is the technique.  When you do the initial estimate, remember the value of $X^T X$ (which is a $2 \times 2$ matrix) and of $X^T y$ (which is a $2$-vector).  This only requires $O(1)$ storage.

Now let's say you add a point.  This involves adding a row to $X,y$, to obtain new values, call them $X',y'$.  We now need to compute $(X'^T X')^{-1} X'^T y'$.  Fortunately, this can computed efficiently.  It is easy to compute $X'^T X'$ in $O(1)$ time, given the value of $X^T X$ and the row that was added to $X$.  It is also easy to compute $X'^T y'$ in $O(1)$, given the value of $X^T y$ and the row that was added to $X,y$.  Once you know the values of $X'^T X'$ and $X'^T y'$, you can simply multiply them (takes $O(1)$ time) and update the stored values.

A similar procedure can be used to remove a point, if you've stored all of the points and all of $X,y$.

Quadratic regression

The same techniques work for quadratic regression.  Now instead of a $n\times 2$ matrix, we have a $n \times 3$ matrix.  Basically, instead of the simple linear model $y \sim \beta_1 x + \beta_2$, we obtain the model $y \sim \beta_1 x^2 + \beta_2 x + \beta_3$, which has three parameters instead of two.  Everything else transfers over, and all updates can be done in $O(1)$ time.

Gradient descent

Finally, one last method.  Some variations on linear regression work by using gradient descent (or some other iterative mathematical optimization algorithm) to find the best model that maximizes some objective function (likelihood, or loss, or whatever).

Heuristically, if you update the set of points, you can often update the existing model much more efficiently than computing a new one from scratch.  In particular, you simply use grade descent with the new objective function -- but you use the old model as the starting point / initial point for the gradient descent.  Gradient descent is usually much faster when the starting point is close to the final optimum value, and when you make a small change (like adding or removing one point) we can expect this to be the case.

I don't think there are any complexity-theoretic guarantees with this approach, so it's entirely heuristic -- but it might work in practice if you are using gradient descent based methods for estimation instead of ordinary least squares.


What is the reverse of greedy algorithm for setcover?

The approximation guarantee will be significantly worse.

Assume you want to cover the set $U=\{1,\ldots,2n\}$.
For every $i=1,\ldots,n$ define a set with n+1 elements by $S_i=\{i,n+1,\ldots,2n\}$.
Assume we want to cover U with the sets
$C=\{S_1,\ldots,S_n,U\}$, where $c(U)=2, c(S_i)=1$.

We would now start with $C$ ans see that the effectivity of the sets $S_i$ is
$$\rho(S_i)=\frac{|S_i|}{c(S_i)}=\frac{n+1}{1}=n+1.$$

In contrast to this the effectivity of $U$ is
$$\rho(U)=\frac{|U|}{c(U)}=\frac{2n}{2}=n<n+1.$$

Thus the reverse greedy would throw out the less effective $U$ leaving us with a solution of cost $n$ while there is a solution of cost $2$.


Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

I think you'll find that the exact same proof of Lemma 3 in [1] (the proof itself appears in [2]) concerning $\rightarrow^\infty_\beta$ also holds for $\rightarrow^\infty_{\beta\bot}$: indeed, they are defined in the same way from $\rightarrow^*_\beta$ and $\rightarrow^*_{\beta\bot}$ respectively, which are transitive by definition!

The lemma holds for an arbitrary reflexive-transitive congruence relation in place of $\rightarrow^*_{\beta\bot}$, as you can verify in [2] without needing to go into the detail of the coinductive proofs. In particular, the proofs of lemmas 4.1-5 in [2] are unchanged (with extra induction cases in 4.4).


Bounds on the size of the solution of a quadratic program

In Quadratic Programming is in NP, it is shown that a slight variant of this problem (QPL) is in NP. The question can be formulated as follows: does there exist a point $x \in \mathbb{R}^n$ such that $ Ax \leq b $ and $x^T Q x \leq K$, where $K$ is a rational number. In the section 2 of this paper, they prove that, when the minimum exists, then there is a minimum $x^*$ with a polynomial number of digits. Their proof is independent from $K$, so it directly applies to your formulation.

The claim that $x^*$ has a polynomial number of digits is not enough, since you want the solution to be polynomial in $\varphi$ and $n$.

In their proof, they define $x^*$ as a particular global minimum with the maximum number of active inequalities, and then, they construct a nonsingular system of linear equations and show that $x^*$ (or a projection of $x^*$) is its unique solution. Thanks to a theorem by Edmonds they conclude that $x^*$ has a polynomial number of digits.

Since the system has a unique solution, $x^*$ is also the solution to a subsystem consisting of $n$ of the equations. At first sight, the projection of $x^*$ does not seem to be a problem, and all the coefficients of these equations can be kept integer and polynomial in $\varphi$.

So that should reduce your question to the following one:

For systems of linear equations $Cx=d$ (where $C$ is a $n\times n$ integer matrix, and the maximal entry in $C$ and $d$ is $\varphi$) with a unique solution $x^*$, is it true that $x^*$ is polynomial in $n$ and $\varphi$?

EDIT. As pointed out by Kristoffer Arnsfelt Hansen, it is of course useless to consider more than $n$ linear equations.